Metamath Proof Explorer

Theorem eroprf

Description: Functionality 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 )
eropr.15 
|- L = ( C /. T )
Assertion eroprf 
|- ( ph -> .+^ : ( J X. K ) --> L )

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 eropr.15 
 |-  L = ( C /. T )
16 3 ad2antrr 
 |-  ( ( ( ph /\ ( x e. J /\ y e. K ) ) /\ ( p e. A /\ q e. B ) ) -> T e. Z )
17 10 adantr 
 |-  ( ( ph /\ ( x e. J /\ y e. K ) ) -> .+ : ( A X. B ) --> C )
18 17 fovcdmda 
 |-  ( ( ( ph /\ ( x e. J /\ y e. K ) ) /\ ( p e. A /\ q e. B ) ) -> ( p .+ q ) e. C )
19 ecelqsg 
 |-  ( ( T e. Z /\ ( p .+ q ) e. C ) -> [ ( p .+ q ) ] T e. ( C /. T ) )
20 16 18 19 syl2anc 
 |-  ( ( ( ph /\ ( x e. J /\ y e. K ) ) /\ ( p e. A /\ q e. B ) ) -> [ ( p .+ q ) ] T e. ( C /. T ) )
21 20 15 eleqtrrdi 
 |-  ( ( ( ph /\ ( x e. J /\ y e. K ) ) /\ ( p e. A /\ q e. B ) ) -> [ ( p .+ q ) ] T e. L )
22 eleq1a 
 |-  ( [ ( p .+ q ) ] T e. L -> ( z = [ ( p .+ q ) ] T -> z e. L ) )
23 21 22 syl 
 |-  ( ( ( ph /\ ( x e. J /\ y e. K ) ) /\ ( p e. A /\ q e. B ) ) -> ( z = [ ( p .+ q ) ] T -> z e. L ) )
24 23 adantld 
 |-  ( ( ( ph /\ ( x e. J /\ y e. K ) ) /\ ( p e. A /\ q e. B ) ) -> ( ( ( x = [ p ] R /\ y = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) -> z e. L ) )
25 24 rexlimdvva 
 |-  ( ( ph /\ ( x e. J /\ y e. K ) ) -> ( E. p e. A E. q e. B ( ( x = [ p ] R /\ y = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) -> z e. L ) )
26 25 abssdv 
 |-  ( ( ph /\ ( x e. J /\ y e. K ) ) -> { z | E. p e. A E. q e. B ( ( x = [ p ] R /\ y = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) } C_ L )
27 1 2 3 4 5 6 7 8 9 10 11 eroveu 
 |-  ( ( ph /\ ( x e. J /\ y e. K ) ) -> E! z E. p e. A E. q e. B ( ( x = [ p ] R /\ y = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) )
28 iotacl 
 |-  ( E! 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 ( ( x = [ p ] R /\ y = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) ) e. { z | E. p e. A E. q e. B ( ( x = [ p ] R /\ y = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) } )
29 27 28 syl 
 |-  ( ( 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 ) ) e. { z | E. p e. A E. q e. B ( ( x = [ p ] R /\ y = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) } )
30 26 29 sseldd 
 |-  ( ( 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 ) ) e. L )
31 30 ralrimivva 
 |-  ( ph -> A. x e. J A. y e. K ( iota z E. p e. A E. q e. B ( ( x = [ p ] R /\ y = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) ) e. L )
32 eqid 
 |-  ( 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 ) ) ) = ( 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 ) ) )
33 32 fmpo 
 |-  ( A. x e. J A. y e. K ( iota z E. p e. A E. q e. B ( ( x = [ p ] R /\ y = [ q ] S ) /\ z = [ ( p .+ q ) ] T ) ) e. L <-> ( 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 ) ) ) : ( J X. K ) --> L )
34 31 33 sylib 
 |-  ( 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 ) ) ) : ( J X. K ) --> L )
35 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 ) ) ) )
36 35 feq1d 
 |-  ( ph -> ( .+^ : ( J X. K ) --> L <-> ( 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 ) ) ) : ( J X. K ) --> L ) )
37 34 36 mpbird 
 |-  ( ph -> .+^ : ( J X. K ) --> L )