---

Step * 2 of Lemma omral_bilinear


1. g : OCMon
2. a : CDRng
⊢ ∀a1,x,y:|omral(g;a)|.  ((a1 ** (x ++ y)) = ((a1 ** x) ++ (a1 ** y)) ∈ |omral(g;a)|)
BY
{ ((RenameBVars [`a1',`ps';`x',`qs';`y',`rs'] 0 
THENM RepD 
THENM BLemma `omral_lookups_same_a` 
THENM D 0) THENA Auto) 
 }

1
1. g : OCMon
2. a : CDRng
3. ps : |omral(g;a)|
4. qs : |omral(g;a)|
5. rs : |omral(g;a)|
6. u : |g|
⊢ ((ps ** (qs ++ rs))[u]) = (((ps ** qs) ++ (ps ** rs))[u]) ∈ |a|

---

Latex:

---

Latex:

1.  g  :  OCMon
2.  a  :  CDRng
\mvdash{}  \mforall{}a1,x,y:|omral(g;a)|.    ((a1  **  (x  ++  y))  =  ((a1  **  x)  ++  (a1  **  y)))


By

---

Latex:
((RenameBVars  [`a1',`ps';`x',`qs';`y',`rs']  0 
THENM  RepD 
THENM  BLemma  `omral\_lookups\_same\_a` 
THENM  D  0)  THENA  Auto) 

---

Home Index