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 ) ] .~ )