Metamath Proof Explorer

Theorem qusaddvallem

Description: Value of an operation defined on a quotient structure. (Contributed by Mario Carneiro, 24-Feb-2015)

Ref Expression
Hypotheses qusaddf.u 
|- ( ph -> U = ( R /s .~ ) )
qusaddf.v 
|- ( ph -> V = ( Base ` R ) )
qusaddf.r 
|- ( ph -> .~ Er V )
qusaddf.z 
|- ( ph -> R e. Z )
qusaddf.e 
|- ( ph -> ( ( a .~ p /\ b .~ q ) -> ( a .x. b ) .~ ( p .x. q ) ) )
qusaddf.c 
|- ( ( ph /\ ( p e. V /\ q e. V ) ) -> ( p .x. q ) e. V )
qusaddflem.f 
|- F = ( x e. V |-> [ x ] .~ )
qusaddflem.g 
|- ( ph -> .xb = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )
Assertion qusaddvallem 
|- ( ( ph /\ X e. V /\ Y e. V ) -> ( [ X ] .~ .xb [ Y ] .~ ) = [ ( X .x. Y ) ] .~ )

Proof

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 qusaddflem.f 
 |-  F = ( x e. V |-> [ x ] .~ )
8 qusaddflem.g 
 |-  ( ph -> .xb = U_ p e. V U_ q e. V { <. <. ( F ` p ) , ( F ` q ) >. , ( F ` ( p .x. q ) ) >. } )
9 fvex 
 |-  ( Base ` R ) e. _V
10 2 9 eqeltrdi 
 |-  ( ph -> V e. _V )
11 erex 
 |-  ( .~ Er V -> ( V e. _V -> .~ e. _V ) )
12 3 10 11 sylc 
 |-  ( ph -> .~ e. _V )
13 1 2 7 12 4 quslem 
 |-  ( ph -> F : V -onto-> ( V /. .~ ) )
14 3 10 7 6 5 ercpbl 
 |-  ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .x. b ) ) = ( F ` ( p .x. q ) ) ) )
15 13 14 8 imasaddvallem 
 |-  ( ( ph /\ X e. V /\ Y e. V ) -> ( ( F ` X ) .xb ( F ` Y ) ) = ( F ` ( X .x. Y ) ) )
16 3 3ad2ant1 
 |-  ( ( ph /\ X e. V /\ Y e. V ) -> .~ Er V )
17 10 3ad2ant1 
 |-  ( ( ph /\ X e. V /\ Y e. V ) -> V e. _V )
18 16 17 7 divsfval 
 |-  ( ( ph /\ X e. V /\ Y e. V ) -> ( F ` X ) = [ X ] .~ )
19 16 17 7 divsfval 
 |-  ( ( ph /\ X e. V /\ Y e. V ) -> ( F ` Y ) = [ Y ] .~ )
20 18 19 oveq12d 
 |-  ( ( ph /\ X e. V /\ Y e. V ) -> ( ( F ` X ) .xb ( F ` Y ) ) = ( [ X ] .~ .xb [ Y ] .~ ) )
21 16 17 7 divsfval 
 |-  ( ( ph /\ X e. V /\ Y e. V ) -> ( F ` ( X .x. Y ) ) = [ ( X .x. Y ) ] .~ )
22 15 20 21 3eqtr3d 
 |-  ( ( ph /\ X e. V /\ Y e. V ) -> ( [ X ] .~ .xb [ Y ] .~ ) = [ ( X .x. Y ) ] .~ )