Metamath Proof Explorer


Theorem erov2

Description: The value of an operation defined on equivalence classes. (Contributed by Jeff Madsen, 10-Jun-2010)

Ref Expression
Hypotheses eropr2.1
|- J = ( A /. .~ )
eropr2.2
|- .+^ = { <. <. x , y >. , z >. | E. p e. A E. q e. A ( ( x = [ p ] .~ /\ y = [ q ] .~ ) /\ z = [ ( p .+ q ) ] .~ ) }
eropr2.3
|- ( ph -> .~ e. X )
eropr2.4
|- ( ph -> .~ Er U )
eropr2.5
|- ( ph -> A C_ U )
eropr2.6
|- ( ph -> .+ : ( A X. A ) --> A )
eropr2.7
|- ( ( ph /\ ( ( r e. A /\ s e. A ) /\ ( t e. A /\ u e. A ) ) ) -> ( ( r .~ s /\ t .~ u ) -> ( r .+ t ) .~ ( s .+ u ) ) )
Assertion erov2
|- ( ( ph /\ P e. A /\ Q e. A ) -> ( [ P ] .~ .+^ [ Q ] .~ ) = [ ( P .+ Q ) ] .~ )

Proof

Step Hyp Ref Expression
1 eropr2.1
 |-  J = ( A /. .~ )
2 eropr2.2
 |-  .+^ = { <. <. x , y >. , z >. | E. p e. A E. q e. A ( ( x = [ p ] .~ /\ y = [ q ] .~ ) /\ z = [ ( p .+ q ) ] .~ ) }
3 eropr2.3
 |-  ( ph -> .~ e. X )
4 eropr2.4
 |-  ( ph -> .~ Er U )
5 eropr2.5
 |-  ( ph -> A C_ U )
6 eropr2.6
 |-  ( ph -> .+ : ( A X. A ) --> A )
7 eropr2.7
 |-  ( ( ph /\ ( ( r e. A /\ s e. A ) /\ ( t e. A /\ u e. A ) ) ) -> ( ( r .~ s /\ t .~ u ) -> ( r .+ t ) .~ ( s .+ u ) ) )
8 1 1 3 4 4 4 5 5 5 6 7 2 3 3 erov
 |-  ( ( ph /\ P e. A /\ Q e. A ) -> ( [ P ] .~ .+^ [ Q ] .~ ) = [ ( P .+ Q ) ] .~ )