Metamath Proof Explorer


Theorem qusmulf

Description: The base set of an image 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 qusmulf
|- ( ph -> .xb : ( ( V /. .~ ) X. ( V /. .~ ) ) --> ( V /. .~ ) )

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 qusaddflem
 |-  ( ph -> .xb : ( ( V /. .~ ) X. ( V /. .~ ) ) --> ( V /. .~ ) )