---

Step * of Lemma bilinear_comm_elim

∀[T:Type]. ∀[pl,tm:T ⟶ T ⟶ T].
  (BiLinear(T;pl;tm)) supposing ((∀a,x,y:T.  ((a tm (x pl y)) = ((a tm x) pl (a tm y)) ∈ T)) and Comm(T;tm))
BY
{ ((Unfolds ``comm bilinear`` 0 
THEN GenRepD) THENA Auto) }

1
1. T : Type
2. pl : T ⟶ T ⟶ T
3. tm : T ⟶ T ⟶ T
4. ∀[x,y:T].  ((x tm y) = (y tm x) ∈ T)
5. ∀a,x,y:T.  ((a tm (x pl y)) = ((a tm x) pl (a tm y)) ∈ T)
6. a : T
7. x : T
8. y : T
⊢ (a tm (x pl y)) = ((a tm x) pl (a tm y)) ∈ T

2
1. T : Type
2. pl : T ⟶ T ⟶ T
3. tm : T ⟶ T ⟶ T
4. ∀[x,y:T].  ((x tm y) = (y tm x) ∈ T)
5. ∀a,x,y:T.  ((a tm (x pl y)) = ((a tm x) pl (a tm y)) ∈ T)
6. a : T
7. x : T
8. y : T
⊢ ((x pl y) tm a) = ((x tm a) pl (y tm a)) ∈ T

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[pl,tm:T  {}\mrightarrow{}  T  {}\mrightarrow{}  T].
    (BiLinear(T;pl;tm))  supposing 
          ((\mforall{}a,x,y:T.    ((a  tm  (x  pl  y))  =  ((a  tm  x)  pl  (a  tm  y))))  and 
          Comm(T;tm))


By

---

Latex:
((Unfolds  ``comm  bilinear``  0 
THEN  GenRepD)  THENA  Auto)

---

Home Index