Metamath Proof Explorer

Theorem erov

Description: The value of an operation defined on equivalence classes. (Contributed by Jeff Madsen, 10-Jun-2010) (Revised by Mario Carneiro, 30-Dec-2014)

Ref Expression
Hypotheses eropr.1 
|- J = ( A /. R )
eropr.2 
|- K = ( B /. S )
eropr.3 
|- ( ph -> T e. Z )
eropr.4 
|- ( ph -> R Er U )
eropr.5 
|- ( ph -> S Er V )
eropr.6 
|- ( ph -> T Er W )
eropr.7 
|- ( ph -> A C_ U )
eropr.8 
|- ( ph -> B C_ V )
eropr.9 
|- ( ph -> C C_ W )
eropr.10 
|- ( ph -> .+ : ( A X. B ) --> C )
eropr.11 
|- ( ( ph /\ ( ( r e. A /\ s e. A ) /\ ( t e. B /\ u e. B ) ) ) -> ( ( r R s /\ t S u ) -> ( r .+ t ) T ( s .+ u ) ) )
eropr.12 
|- .+^ = { <. <. x , y >. , z >. | E. p e. A E. q e. B ( ( x = [ p ] R /\ y = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) }
eropr.13 
|- ( ph -> R e. X )
eropr.14 
|- ( ph -> S e. Y )
Assertion erov 
|- ( ( ph /\ P e. A /\ Q e. B ) -> ( [ P ] R .+^ [ Q ] S ) = [ ( P .+ Q ) ] T )

Proof

Step Hyp Ref Expression
1 eropr.1 
 |-  J = ( A /. R )
2 eropr.2 
 |-  K = ( B /. S )
3 eropr.3 
 |-  ( ph -> T e. Z )
4 eropr.4 
 |-  ( ph -> R Er U )
5 eropr.5 
 |-  ( ph -> S Er V )
6 eropr.6 
 |-  ( ph -> T Er W )
7 eropr.7 
 |-  ( ph -> A C_ U )
8 eropr.8 
 |-  ( ph -> B C_ V )
9 eropr.9 
 |-  ( ph -> C C_ W )
10 eropr.10 
 |-  ( ph -> .+ : ( A X. B ) --> C )
11 eropr.11 
 |-  ( ( ph /\ ( ( r e. A /\ s e. A ) /\ ( t e. B /\ u e. B ) ) ) -> ( ( r R s /\ t S u ) -> ( r .+ t ) T ( s .+ u ) ) )
12 eropr.12 
 |-  .+^ = { <. <. x , y >. , z >. | E. p e. A E. q e. B ( ( x = [ p ] R /\ y = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) }
13 eropr.13 
 |-  ( ph -> R e. X )
14 eropr.14 
 |-  ( ph -> S e. Y )
15 1 2 3 4 5 6 7 8 9 10 11 12 erovlem 
 |-  ( ph -> .+^ = ( x e. J , y e. K |-> ( iota z E. p e. A E. q e. B ( ( x = [ p ] R /\ y = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) ) ) )
16 15 3ad2ant1 
 |-  ( ( ph /\ P e. A /\ Q e. B ) -> .+^ = ( x e. J , y e. K |-> ( iota z E. p e. A E. q e. B ( ( x = [ p ] R /\ y = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) ) ) )
17 simprl 
 |-  ( ( ( ph /\ P e. A /\ Q e. B ) /\ ( x = [ P ] R /\ y = [ Q ] S ) ) -> x = [ P ] R )
18 17 eqeq1d 
 |-  ( ( ( ph /\ P e. A /\ Q e. B ) /\ ( x = [ P ] R /\ y = [ Q ] S ) ) -> ( x = [ p ] R <-> [ P ] R = [ p ] R ) )
19 simprr 
 |-  ( ( ( ph /\ P e. A /\ Q e. B ) /\ ( x = [ P ] R /\ y = [ Q ] S ) ) -> y = [ Q ] S )
20 19 eqeq1d 
 |-  ( ( ( ph /\ P e. A /\ Q e. B ) /\ ( x = [ P ] R /\ y = [ Q ] S ) ) -> ( y = [ q ] S <-> [ Q ] S = [ q ] S ) )
21 18 20 anbi12d 
 |-  ( ( ( ph /\ P e. A /\ Q e. B ) /\ ( x = [ P ] R /\ y = [ Q ] S ) ) -> ( ( x = [ p ] R /\ y = [ q ] S ) <-> ( [ P ] R = [ p ] R /\ [ Q ] S = [ q ] S ) ) )
22 21 anbi1d 
 |-  ( ( ( ph /\ P e. A /\ Q e. B ) /\ ( x = [ P ] R /\ y = [ Q ] S ) ) -> ( ( ( x = [ p ] R /\ y = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) <-> ( ( [ P ] R = [ p ] R /\ [ Q ] S = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) ) )
23 22 2rexbidv 
 |-  ( ( ( ph /\ P e. A /\ Q e. B ) /\ ( x = [ P ] R /\ y = [ Q ] S ) ) -> ( E. p e. A E. q e. B ( ( x = [ p ] R /\ y = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) <-> E. p e. A E. q e. B ( ( [ P ] R = [ p ] R /\ [ Q ] S = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) ) )
24 23 iotabidv 
 |-  ( ( ( ph /\ P e. A /\ Q e. B ) /\ ( x = [ P ] R /\ y = [ Q ] S ) ) -> ( iota z E. p e. A E. q e. B ( ( x = [ p ] R /\ y = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) ) = ( iota z E. p e. A E. q e. B ( ( [ P ] R = [ p ] R /\ [ Q ] S = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) ) )
25 ecelqsg 
 |-  ( ( R e. X /\ P e. A ) -> [ P ] R e. ( A /. R ) )
26 25 1 eleqtrrdi 
 |-  ( ( R e. X /\ P e. A ) -> [ P ] R e. J )
27 13 26 sylan 
 |-  ( ( ph /\ P e. A ) -> [ P ] R e. J )
28 27 3adant3 
 |-  ( ( ph /\ P e. A /\ Q e. B ) -> [ P ] R e. J )
29 ecelqsg 
 |-  ( ( S e. Y /\ Q e. B ) -> [ Q ] S e. ( B /. S ) )
30 29 2 eleqtrrdi 
 |-  ( ( S e. Y /\ Q e. B ) -> [ Q ] S e. K )
31 14 30 sylan 
 |-  ( ( ph /\ Q e. B ) -> [ Q ] S e. K )
32 31 3adant2 
 |-  ( ( ph /\ P e. A /\ Q e. B ) -> [ Q ] S e. K )
33 iotaex 
 |-  ( iota z E. p e. A E. q e. B ( ( [ P ] R = [ p ] R /\ [ Q ] S = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) ) e. _V
34 33 a1i 
 |-  ( ( ph /\ P e. A /\ Q e. B ) -> ( iota z E. p e. A E. q e. B ( ( [ P ] R = [ p ] R /\ [ Q ] S = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) ) e. _V )
35 16 24 28 32 34 ovmpod 
 |-  ( ( ph /\ P e. A /\ Q e. B ) -> ( [ P ] R .+^ [ Q ] S ) = ( iota z E. p e. A E. q e. B ( ( [ P ] R = [ p ] R /\ [ Q ] S = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) ) )
36 eqid 
 |-  [ P ] R = [ P ] R
37 eqid 
 |-  [ Q ] S = [ Q ] S
38 36 37 pm3.2i 
 |-  ( [ P ] R = [ P ] R /\ [ Q ] S = [ Q ] S )
39 eqid 
 |-  [ ( P .+ Q ) ] T = [ ( P .+ Q ) ] T
40 38 39 pm3.2i 
 |-  ( ( [ P ] R = [ P ] R /\ [ Q ] S = [ Q ] S ) /\ [ ( P .+ Q ) ] T = [ ( P .+ Q ) ] T )
41 eceq1 
 |-  ( p = P -> [ p ] R = [ P ] R )
42 41 eqeq2d 
 |-  ( p = P -> ( [ P ] R = [ p ] R <-> [ P ] R = [ P ] R ) )
43 42 anbi1d 
 |-  ( p = P -> ( ( [ P ] R = [ p ] R /\ [ Q ] S = [ q ] S ) <-> ( [ P ] R = [ P ] R /\ [ Q ] S = [ q ] S ) ) )
44 oveq1 
 |-  ( p = P -> ( p .+ q ) = ( P .+ q ) )
45 44 eceq1d 
 |-  ( p = P -> [ ( p .+ q ) ] T = [ ( P .+ q ) ] T )
46 45 eqeq2d 
 |-  ( p = P -> ( [ ( P .+ Q ) ] T = [ ( p .+ q ) ] T <-> [ ( P .+ Q ) ] T = [ ( P .+ q ) ] T ) )
47 43 46 anbi12d 
 |-  ( p = P -> ( ( ( [ P ] R = [ p ] R /\ [ Q ] S = [ q ] S ) /\ [ ( P .+ Q ) ] T = [ ( p .+ q ) ] T ) <-> ( ( [ P ] R = [ P ] R /\ [ Q ] S = [ q ] S ) /\ [ ( P .+ Q ) ] T = [ ( P .+ q ) ] T ) ) )
48 eceq1 
 |-  ( q = Q -> [ q ] S = [ Q ] S )
49 48 eqeq2d 
 |-  ( q = Q -> ( [ Q ] S = [ q ] S <-> [ Q ] S = [ Q ] S ) )
50 49 anbi2d 
 |-  ( q = Q -> ( ( [ P ] R = [ P ] R /\ [ Q ] S = [ q ] S ) <-> ( [ P ] R = [ P ] R /\ [ Q ] S = [ Q ] S ) ) )
51 oveq2 
 |-  ( q = Q -> ( P .+ q ) = ( P .+ Q ) )
52 51 eceq1d 
 |-  ( q = Q -> [ ( P .+ q ) ] T = [ ( P .+ Q ) ] T )
53 52 eqeq2d 
 |-  ( q = Q -> ( [ ( P .+ Q ) ] T = [ ( P .+ q ) ] T <-> [ ( P .+ Q ) ] T = [ ( P .+ Q ) ] T ) )
54 50 53 anbi12d 
 |-  ( q = Q -> ( ( ( [ P ] R = [ P ] R /\ [ Q ] S = [ q ] S ) /\ [ ( P .+ Q ) ] T = [ ( P .+ q ) ] T ) <-> ( ( [ P ] R = [ P ] R /\ [ Q ] S = [ Q ] S ) /\ [ ( P .+ Q ) ] T = [ ( P .+ Q ) ] T ) ) )
55 47 54 rspc2ev 
 |-  ( ( P e. A /\ Q e. B /\ ( ( [ P ] R = [ P ] R /\ [ Q ] S = [ Q ] S ) /\ [ ( P .+ Q ) ] T = [ ( P .+ Q ) ] T ) ) -> E. p e. A E. q e. B ( ( [ P ] R = [ p ] R /\ [ Q ] S = [ q ] S ) /\ [ ( P .+ Q ) ] T = [ ( p .+ q ) ] T ) )
56 40 55 mp3an3 
 |-  ( ( P e. A /\ Q e. B ) -> E. p e. A E. q e. B ( ( [ P ] R = [ p ] R /\ [ Q ] S = [ q ] S ) /\ [ ( P .+ Q ) ] T = [ ( p .+ q ) ] T ) )
57 56 3adant1 
 |-  ( ( ph /\ P e. A /\ Q e. B ) -> E. p e. A E. q e. B ( ( [ P ] R = [ p ] R /\ [ Q ] S = [ q ] S ) /\ [ ( P .+ Q ) ] T = [ ( p .+ q ) ] T ) )
58 ecexg 
 |-  ( T e. Z -> [ ( P .+ Q ) ] T e. _V )
59 3 58 syl 
 |-  ( ph -> [ ( P .+ Q ) ] T e. _V )
60 59 3ad2ant1 
 |-  ( ( ph /\ P e. A /\ Q e. B ) -> [ ( P .+ Q ) ] T e. _V )
61 simp1 
 |-  ( ( ph /\ P e. A /\ Q e. B ) -> ph )
62 1 2 3 4 5 6 7 8 9 10 11 eroveu 
 |-  ( ( ph /\ ( [ P ] R e. J /\ [ Q ] S e. K ) ) -> E! z E. p e. A E. q e. B ( ( [ P ] R = [ p ] R /\ [ Q ] S = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) )
63 61 28 32 62 syl12anc 
 |-  ( ( ph /\ P e. A /\ Q e. B ) -> E! z E. p e. A E. q e. B ( ( [ P ] R = [ p ] R /\ [ Q ] S = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) )
64 simpr 
 |-  ( ( ( ph /\ P e. A /\ Q e. B ) /\ z = [ ( P .+ Q ) ] T ) -> z = [ ( P .+ Q ) ] T )
65 64 eqeq1d 
 |-  ( ( ( ph /\ P e. A /\ Q e. B ) /\ z = [ ( P .+ Q ) ] T ) -> ( z = [ ( p .+ q ) ] T <-> [ ( P .+ Q ) ] T = [ ( p .+ q ) ] T ) )
66 65 anbi2d 
 |-  ( ( ( ph /\ P e. A /\ Q e. B ) /\ z = [ ( P .+ Q ) ] T ) -> ( ( ( [ P ] R = [ p ] R /\ [ Q ] S = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) <-> ( ( [ P ] R = [ p ] R /\ [ Q ] S = [ q ] S ) /\ [ ( P .+ Q ) ] T = [ ( p .+ q ) ] T ) ) )
67 66 2rexbidv 
 |-  ( ( ( ph /\ P e. A /\ Q e. B ) /\ z = [ ( P .+ Q ) ] T ) -> ( E. p e. A E. q e. B ( ( [ P ] R = [ p ] R /\ [ Q ] S = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) <-> E. p e. A E. q e. B ( ( [ P ] R = [ p ] R /\ [ Q ] S = [ q ] S ) /\ [ ( P .+ Q ) ] T = [ ( p .+ q ) ] T ) ) )
68 60 63 67 iota2d 
 |-  ( ( ph /\ P e. A /\ Q e. B ) -> ( E. p e. A E. q e. B ( ( [ P ] R = [ p ] R /\ [ Q ] S = [ q ] S ) /\ [ ( P .+ Q ) ] T = [ ( p .+ q ) ] T ) <-> ( iota z E. p e. A E. q e. B ( ( [ P ] R = [ p ] R /\ [ Q ] S = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) ) = [ ( P .+ Q ) ] T ) )
69 57 68 mpbid 
 |-  ( ( ph /\ P e. A /\ Q e. B ) -> ( iota z E. p e. A E. q e. B ( ( [ P ] R = [ p ] R /\ [ Q ] S = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) ) = [ ( P .+ Q ) ] T )
70 35 69 eqtrd 
 |-  ( ( ph /\ P e. A /\ Q e. B ) -> ( [ P ] R .+^ [ Q ] S ) = [ ( P .+ Q ) ] T )