Step |
Hyp |
Ref |
Expression |
1 |
|
qusaddf.u |
|- ( ph -> U = ( R /s .~ ) ) |
2 |
|
qusaddf.v |
|- ( ph -> V = ( Base ` R ) ) |
3 |
|
qusaddf.r |
|- ( ph -> .~ Er V ) |
4 |
|
qusaddf.z |
|- ( ph -> R e. Z ) |
5 |
|
qusaddf.e |
|- ( ph -> ( ( a .~ p /\ b .~ q ) -> ( a .x. b ) .~ ( p .x. q ) ) ) |
6 |
|
qusaddf.c |
|- ( ( ph /\ ( p e. V /\ q e. V ) ) -> ( p .x. q ) e. V ) |
7 |
|
qusaddf.p |
|- .x. = ( +g ` R ) |
8 |
|
qusaddf.a |
|- .xb = ( +g ` U ) |
9 |
|
eqid |
|- ( x e. V |-> [ x ] .~ ) = ( x e. V |-> [ x ] .~ ) |
10 |
|
fvex |
|- ( Base ` R ) e. _V |
11 |
2 10
|
eqeltrdi |
|- ( ph -> V e. _V ) |
12 |
|
erex |
|- ( .~ Er V -> ( V e. _V -> .~ e. _V ) ) |
13 |
3 11 12
|
sylc |
|- ( ph -> .~ e. _V ) |
14 |
1 2 9 13 4
|
qusval |
|- ( ph -> U = ( ( x e. V |-> [ x ] .~ ) "s R ) ) |
15 |
1 2 9 13 4
|
quslem |
|- ( ph -> ( x e. V |-> [ x ] .~ ) : V -onto-> ( V /. .~ ) ) |
16 |
14 2 15 4 7 8
|
imasplusg |
|- ( ph -> .xb = U_ p e. V U_ q e. V { <. <. ( ( x e. V |-> [ x ] .~ ) ` p ) , ( ( x e. V |-> [ x ] .~ ) ` q ) >. , ( ( x e. V |-> [ x ] .~ ) ` ( p .x. q ) ) >. } ) |
17 |
1 2 3 4 5 6 9 16
|
qusaddflem |
|- ( ph -> .xb : ( ( V /. .~ ) X. ( V /. .~ ) ) --> ( V /. .~ ) ) |