This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem qusmulval

Description: The multiplication in 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 )
qusmulf.p 
|- .x. = ( .r ` R )
qusmulf.a 
|- .xb = ( .r ` U )
Assertion qusmulval 
|- ( ( 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 qusmulf.p 
 |-  .x. = ( .r ` R )
8 qusmulf.a 
 |-  .xb = ( .r ` 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 imasmulr 
 |-  ( 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 qusaddvallem 
 |-  ( ( ph /\ X e. V /\ Y e. V ) -> ( [ X ] .~ .xb [ Y ] .~ ) = [ ( X .x. Y ) ] .~ )