Metamath Proof Explorer

Theorem qusval

Description: Value of a quotient structure. (Contributed by Mario Carneiro, 23-Feb-2015)

Ref Expression
Hypotheses qusval.u 
|- ( ph -> U = ( R /s .~ ) )
qusval.v 
|- ( ph -> V = ( Base ` R ) )
qusval.f 
|- F = ( x e. V |-> [ x ] .~ )
qusval.e 
|- ( ph -> .~ e. W )
qusval.r 
|- ( ph -> R e. Z )
Assertion qusval 
|- ( ph -> U = ( F "s R ) )

Proof

Step Hyp Ref Expression
1 qusval.u 
 |-  ( ph -> U = ( R /s .~ ) )
2 qusval.v 
 |-  ( ph -> V = ( Base ` R ) )
3 qusval.f 
 |-  F = ( x e. V |-> [ x ] .~ )
4 qusval.e 
 |-  ( ph -> .~ e. W )
5 qusval.r 
 |-  ( ph -> R e. Z )
6 df-qus 
 |-  /s = ( r e. _V , e e. _V |-> ( ( x e. ( Base ` r ) |-> [ x ] e ) "s r ) )
7 6 a1i 
 |-  ( ph -> /s = ( r e. _V , e e. _V |-> ( ( x e. ( Base ` r ) |-> [ x ] e ) "s r ) ) )
8 simprl 
 |-  ( ( ph /\ ( r = R /\ e = .~ ) ) -> r = R )
9 8 fveq2d 
 |-  ( ( ph /\ ( r = R /\ e = .~ ) ) -> ( Base ` r ) = ( Base ` R ) )
10 2 adantr 
 |-  ( ( ph /\ ( r = R /\ e = .~ ) ) -> V = ( Base ` R ) )
11 9 10 eqtr4d 
 |-  ( ( ph /\ ( r = R /\ e = .~ ) ) -> ( Base ` r ) = V )
12 eceq2 
 |-  ( e = .~ -> [ x ] e = [ x ] .~ )
13 12 ad2antll 
 |-  ( ( ph /\ ( r = R /\ e = .~ ) ) -> [ x ] e = [ x ] .~ )
14 11 13 mpteq12dv 
 |-  ( ( ph /\ ( r = R /\ e = .~ ) ) -> ( x e. ( Base ` r ) |-> [ x ] e ) = ( x e. V |-> [ x ] .~ ) )
15 14 3 eqtr4di 
 |-  ( ( ph /\ ( r = R /\ e = .~ ) ) -> ( x e. ( Base ` r ) |-> [ x ] e ) = F )
16 15 8 oveq12d 
 |-  ( ( ph /\ ( r = R /\ e = .~ ) ) -> ( ( x e. ( Base ` r ) |-> [ x ] e ) "s r ) = ( F "s R ) )
17 5 elexd 
 |-  ( ph -> R e. _V )
18 4 elexd 
 |-  ( ph -> .~ e. _V )
19 ovexd 
 |-  ( ph -> ( F "s R ) e. _V )
20 7 16 17 18 19 ovmpod 
 |-  ( ph -> ( R /s .~ ) = ( F "s R ) )
21 1 20 eqtrd 
 |-  ( ph -> U = ( F "s R ) )