Metamath Proof Explorer

Theorem pzriprnglem10

Description: Lemma 10 for pzriprng : The equivalence classes of R modulo J . (Contributed by AV, 22-Mar-2025)

Ref Expression
Hypotheses pzriprng.r 
|- R = ( ZZring Xs. ZZring )
pzriprng.i 
|- I = ( ZZ X. { 0 } )
pzriprng.j 
|- J = ( R |`s I )
pzriprng.1 
|- .1. = ( 1r ` J )
pzriprng.g 
|- .~ = ( R ~QG I )
Assertion pzriprnglem10 
|- ( ( X e. ZZ /\ Y e. ZZ ) -> [ <. X , Y >. ] .~ = ( ZZ X. { Y } ) )

Proof

Step Hyp Ref Expression
1 pzriprng.r 
 |-  R = ( ZZring Xs. ZZring )
2 pzriprng.i 
 |-  I = ( ZZ X. { 0 } )
3 pzriprng.j 
 |-  J = ( R |`s I )
4 pzriprng.1 
 |-  .1. = ( 1r ` J )
5 pzriprng.g 
 |-  .~ = ( R ~QG I )
6 1 pzriprnglem1 
 |-  R e. Rng
7 rnggrp 
 |-  ( R e. Rng -> R e. Grp )
8 6 7 ax-mp 
 |-  R e. Grp
9 0z 
 |-  0 e. ZZ
10 snssi 
 |-  ( 0 e. ZZ -> { 0 } C_ ZZ )
11 xpss2 
 |-  ( { 0 } C_ ZZ -> ( ZZ X. { 0 } ) C_ ( ZZ X. ZZ ) )
12 9 10 11 mp2b 
 |-  ( ZZ X. { 0 } ) C_ ( ZZ X. ZZ )
13 2 12 eqsstri 
 |-  I C_ ( ZZ X. ZZ )
14 13 a1i 
 |-  ( ( X e. ZZ /\ Y e. ZZ ) -> I C_ ( ZZ X. ZZ ) )
15 opelxpi 
 |-  ( ( X e. ZZ /\ Y e. ZZ ) -> <. X , Y >. e. ( ZZ X. ZZ ) )
16 1 pzriprnglem2 
 |-  ( Base ` R ) = ( ZZ X. ZZ )
17 16 eqcomi 
 |-  ( ZZ X. ZZ ) = ( Base ` R )
18 eqid 
 |-  ( +g ` R ) = ( +g ` R )
19 17 5 18 eqglact 
 |-  ( ( R e. Grp /\ I C_ ( ZZ X. ZZ ) /\ <. X , Y >. e. ( ZZ X. ZZ ) ) -> [ <. X , Y >. ] .~ = ( ( x e. ( ZZ X. ZZ ) |-> ( <. X , Y >. ( +g ` R ) x ) ) " I ) )
20 8 14 15 19 mp3an2i 
 |-  ( ( X e. ZZ /\ Y e. ZZ ) -> [ <. X , Y >. ] .~ = ( ( x e. ( ZZ X. ZZ ) |-> ( <. X , Y >. ( +g ` R ) x ) ) " I ) )
21 14 mptimass 
 |-  ( ( X e. ZZ /\ Y e. ZZ ) -> ( ( x e. ( ZZ X. ZZ ) |-> ( <. X , Y >. ( +g ` R ) x ) ) " I ) = ran ( x e. I |-> ( <. X , Y >. ( +g ` R ) x ) ) )
22 eqid 
 |-  ( x e. I |-> ( <. X , Y >. ( +g ` R ) x ) ) = ( x e. I |-> ( <. X , Y >. ( +g ` R ) x ) )
23 22 rnmpt 
 |-  ran ( x e. I |-> ( <. X , Y >. ( +g ` R ) x ) ) = { e | E. x e. I e = ( <. X , Y >. ( +g ` R ) x ) }
24 23 a1i 
 |-  ( ( X e. ZZ /\ Y e. ZZ ) -> ran ( x e. I |-> ( <. X , Y >. ( +g ` R ) x ) ) = { e | E. x e. I e = ( <. X , Y >. ( +g ` R ) x ) } )
25 2 rexeqi 
 |-  ( E. x e. I e = ( <. X , Y >. ( +g ` R ) x ) <-> E. x e. ( ZZ X. { 0 } ) e = ( <. X , Y >. ( +g ` R ) x ) )
26 oveq2 
 |-  ( x = <. a , b >. -> ( <. X , Y >. ( +g ` R ) x ) = ( <. X , Y >. ( +g ` R ) <. a , b >. ) )
27 26 eqeq2d 
 |-  ( x = <. a , b >. -> ( e = ( <. X , Y >. ( +g ` R ) x ) <-> e = ( <. X , Y >. ( +g ` R ) <. a , b >. ) ) )
28 27 rexxp 
 |-  ( E. x e. ( ZZ X. { 0 } ) e = ( <. X , Y >. ( +g ` R ) x ) <-> E. a e. ZZ E. b e. { 0 } e = ( <. X , Y >. ( +g ` R ) <. a , b >. ) )
29 25 28 bitri 
 |-  ( E. x e. I e = ( <. X , Y >. ( +g ` R ) x ) <-> E. a e. ZZ E. b e. { 0 } e = ( <. X , Y >. ( +g ` R ) <. a , b >. ) )
30 29 a1i 
 |-  ( ( X e. ZZ /\ Y e. ZZ ) -> ( E. x e. I e = ( <. X , Y >. ( +g ` R ) x ) <-> E. a e. ZZ E. b e. { 0 } e = ( <. X , Y >. ( +g ` R ) <. a , b >. ) ) )
31 30 abbidv 
 |-  ( ( X e. ZZ /\ Y e. ZZ ) -> { e | E. x e. I e = ( <. X , Y >. ( +g ` R ) x ) } = { e | E. a e. ZZ E. b e. { 0 } e = ( <. X , Y >. ( +g ` R ) <. a , b >. ) } )
32 c0ex 
 |-  0 e. _V
33 opeq2 
 |-  ( b = 0 -> <. a , b >. = <. a , 0 >. )
34 33 oveq2d 
 |-  ( b = 0 -> ( <. X , Y >. ( +g ` R ) <. a , b >. ) = ( <. X , Y >. ( +g ` R ) <. a , 0 >. ) )
35 34 eqeq2d 
 |-  ( b = 0 -> ( e = ( <. X , Y >. ( +g ` R ) <. a , b >. ) <-> e = ( <. X , Y >. ( +g ` R ) <. a , 0 >. ) ) )
36 32 35 rexsn 
 |-  ( E. b e. { 0 } e = ( <. X , Y >. ( +g ` R ) <. a , b >. ) <-> e = ( <. X , Y >. ( +g ` R ) <. a , 0 >. ) )
37 zringbas 
 |-  ZZ = ( Base ` ZZring )
38 zringring 
 |-  ZZring e. Ring
39 38 a1i 
 |-  ( ( ( X e. ZZ /\ Y e. ZZ ) /\ a e. ZZ ) -> ZZring e. Ring )
40 simpll 
 |-  ( ( ( X e. ZZ /\ Y e. ZZ ) /\ a e. ZZ ) -> X e. ZZ )
41 simplr 
 |-  ( ( ( X e. ZZ /\ Y e. ZZ ) /\ a e. ZZ ) -> Y e. ZZ )
42 simpr 
 |-  ( ( ( X e. ZZ /\ Y e. ZZ ) /\ a e. ZZ ) -> a e. ZZ )
43 0zd 
 |-  ( ( ( X e. ZZ /\ Y e. ZZ ) /\ a e. ZZ ) -> 0 e. ZZ )
44 40 42 zaddcld 
 |-  ( ( ( X e. ZZ /\ Y e. ZZ ) /\ a e. ZZ ) -> ( X + a ) e. ZZ )
45 simpr 
 |-  ( ( X e. ZZ /\ Y e. ZZ ) -> Y e. ZZ )
46 0zd 
 |-  ( ( X e. ZZ /\ Y e. ZZ ) -> 0 e. ZZ )
47 45 46 zaddcld 
 |-  ( ( X e. ZZ /\ Y e. ZZ ) -> ( Y + 0 ) e. ZZ )
48 47 adantr 
 |-  ( ( ( X e. ZZ /\ Y e. ZZ ) /\ a e. ZZ ) -> ( Y + 0 ) e. ZZ )
49 zringplusg 
 |-  + = ( +g ` ZZring )
50 1 37 37 39 39 40 41 42 43 44 48 49 49 18 xpsadd 
 |-  ( ( ( X e. ZZ /\ Y e. ZZ ) /\ a e. ZZ ) -> ( <. X , Y >. ( +g ` R ) <. a , 0 >. ) = <. ( X + a ) , ( Y + 0 ) >. )
51 50 eqeq2d 
 |-  ( ( ( X e. ZZ /\ Y e. ZZ ) /\ a e. ZZ ) -> ( e = ( <. X , Y >. ( +g ` R ) <. a , 0 >. ) <-> e = <. ( X + a ) , ( Y + 0 ) >. ) )
52 36 51 bitrid 
 |-  ( ( ( X e. ZZ /\ Y e. ZZ ) /\ a e. ZZ ) -> ( E. b e. { 0 } e = ( <. X , Y >. ( +g ` R ) <. a , b >. ) <-> e = <. ( X + a ) , ( Y + 0 ) >. ) )
53 52 rexbidva 
 |-  ( ( X e. ZZ /\ Y e. ZZ ) -> ( E. a e. ZZ E. b e. { 0 } e = ( <. X , Y >. ( +g ` R ) <. a , b >. ) <-> E. a e. ZZ e = <. ( X + a ) , ( Y + 0 ) >. ) )
54 53 abbidv 
 |-  ( ( X e. ZZ /\ Y e. ZZ ) -> { e | E. a e. ZZ E. b e. { 0 } e = ( <. X , Y >. ( +g ` R ) <. a , b >. ) } = { e | E. a e. ZZ e = <. ( X + a ) , ( Y + 0 ) >. } )
55 iunab 
 |-  U_ a e. ZZ { e | e = <. ( X + a ) , ( Y + 0 ) >. } = { e | E. a e. ZZ e = <. ( X + a ) , ( Y + 0 ) >. }
56 55 eqcomi 
 |-  { e | E. a e. ZZ e = <. ( X + a ) , ( Y + 0 ) >. } = U_ a e. ZZ { e | e = <. ( X + a ) , ( Y + 0 ) >. }
57 56 a1i 
 |-  ( ( X e. ZZ /\ Y e. ZZ ) -> { e | E. a e. ZZ e = <. ( X + a ) , ( Y + 0 ) >. } = U_ a e. ZZ { e | e = <. ( X + a ) , ( Y + 0 ) >. } )
58 zcn 
 |-  ( Y e. ZZ -> Y e. CC )
59 58 adantl 
 |-  ( ( X e. ZZ /\ Y e. ZZ ) -> Y e. CC )
60 59 addridd 
 |-  ( ( X e. ZZ /\ Y e. ZZ ) -> ( Y + 0 ) = Y )
61 60 opeq2d 
 |-  ( ( X e. ZZ /\ Y e. ZZ ) -> <. ( X + a ) , ( Y + 0 ) >. = <. ( X + a ) , Y >. )
62 61 eqeq2d 
 |-  ( ( X e. ZZ /\ Y e. ZZ ) -> ( e = <. ( X + a ) , ( Y + 0 ) >. <-> e = <. ( X + a ) , Y >. ) )
63 62 abbidv 
 |-  ( ( X e. ZZ /\ Y e. ZZ ) -> { e | e = <. ( X + a ) , ( Y + 0 ) >. } = { e | e = <. ( X + a ) , Y >. } )
64 63 iuneq2d 
 |-  ( ( X e. ZZ /\ Y e. ZZ ) -> U_ a e. ZZ { e | e = <. ( X + a ) , ( Y + 0 ) >. } = U_ a e. ZZ { e | e = <. ( X + a ) , Y >. } )
65 df-sn 
 |-  { <. ( X + a ) , Y >. } = { e | e = <. ( X + a ) , Y >. }
66 65 eqcomi 
 |-  { e | e = <. ( X + a ) , Y >. } = { <. ( X + a ) , Y >. }
67 66 a1i 
 |-  ( a e. ZZ -> { e | e = <. ( X + a ) , Y >. } = { <. ( X + a ) , Y >. } )
68 67 iuneq2i 
 |-  U_ a e. ZZ { e | e = <. ( X + a ) , Y >. } = U_ a e. ZZ { <. ( X + a ) , Y >. }
69 68 a1i 
 |-  ( ( X e. ZZ /\ Y e. ZZ ) -> U_ a e. ZZ { e | e = <. ( X + a ) , Y >. } = U_ a e. ZZ { <. ( X + a ) , Y >. } )
70 velsn 
 |-  ( y e. { <. ( X + a ) , Y >. } <-> y = <. ( X + a ) , Y >. )
71 70 rexbii 
 |-  ( E. a e. ZZ y e. { <. ( X + a ) , Y >. } <-> E. a e. ZZ y = <. ( X + a ) , Y >. )
72 44 adantr 
 |-  ( ( ( ( X e. ZZ /\ Y e. ZZ ) /\ a e. ZZ ) /\ y = <. ( X + a ) , Y >. ) -> ( X + a ) e. ZZ )
73 simplr 
 |-  ( ( ( ( ( X e. ZZ /\ Y e. ZZ ) /\ a e. ZZ ) /\ y = <. ( X + a ) , Y >. ) /\ b = ( X + a ) ) -> y = <. ( X + a ) , Y >. )
74 opeq1 
 |-  ( b = ( X + a ) -> <. b , Y >. = <. ( X + a ) , Y >. )
75 74 adantl 
 |-  ( ( ( ( ( X e. ZZ /\ Y e. ZZ ) /\ a e. ZZ ) /\ y = <. ( X + a ) , Y >. ) /\ b = ( X + a ) ) -> <. b , Y >. = <. ( X + a ) , Y >. )
76 73 75 eqeq12d 
 |-  ( ( ( ( ( X e. ZZ /\ Y e. ZZ ) /\ a e. ZZ ) /\ y = <. ( X + a ) , Y >. ) /\ b = ( X + a ) ) -> ( y = <. b , Y >. <-> <. ( X + a ) , Y >. = <. ( X + a ) , Y >. ) )
77 eqidd 
 |-  ( ( ( ( X e. ZZ /\ Y e. ZZ ) /\ a e. ZZ ) /\ y = <. ( X + a ) , Y >. ) -> <. ( X + a ) , Y >. = <. ( X + a ) , Y >. )
78 72 76 77 rspcedvd 
 |-  ( ( ( ( X e. ZZ /\ Y e. ZZ ) /\ a e. ZZ ) /\ y = <. ( X + a ) , Y >. ) -> E. b e. ZZ y = <. b , Y >. )
79 78 ex 
 |-  ( ( ( X e. ZZ /\ Y e. ZZ ) /\ a e. ZZ ) -> ( y = <. ( X + a ) , Y >. -> E. b e. ZZ y = <. b , Y >. ) )
80 79 rexlimdva 
 |-  ( ( X e. ZZ /\ Y e. ZZ ) -> ( E. a e. ZZ y = <. ( X + a ) , Y >. -> E. b e. ZZ y = <. b , Y >. ) )
81 simpr 
 |-  ( ( ( X e. ZZ /\ Y e. ZZ ) /\ b e. ZZ ) -> b e. ZZ )
82 simpll 
 |-  ( ( ( X e. ZZ /\ Y e. ZZ ) /\ b e. ZZ ) -> X e. ZZ )
83 81 82 zsubcld 
 |-  ( ( ( X e. ZZ /\ Y e. ZZ ) /\ b e. ZZ ) -> ( b - X ) e. ZZ )
84 83 adantr 
 |-  ( ( ( ( X e. ZZ /\ Y e. ZZ ) /\ b e. ZZ ) /\ y = <. b , Y >. ) -> ( b - X ) e. ZZ )
85 simplr 
 |-  ( ( ( ( ( X e. ZZ /\ Y e. ZZ ) /\ b e. ZZ ) /\ y = <. b , Y >. ) /\ a = ( b - X ) ) -> y = <. b , Y >. )
86 oveq2 
 |-  ( a = ( b - X ) -> ( X + a ) = ( X + ( b - X ) ) )
87 86 adantl 
 |-  ( ( ( ( ( X e. ZZ /\ Y e. ZZ ) /\ b e. ZZ ) /\ y = <. b , Y >. ) /\ a = ( b - X ) ) -> ( X + a ) = ( X + ( b - X ) ) )
88 87 opeq1d 
 |-  ( ( ( ( ( X e. ZZ /\ Y e. ZZ ) /\ b e. ZZ ) /\ y = <. b , Y >. ) /\ a = ( b - X ) ) -> <. ( X + a ) , Y >. = <. ( X + ( b - X ) ) , Y >. )
89 85 88 eqeq12d 
 |-  ( ( ( ( ( X e. ZZ /\ Y e. ZZ ) /\ b e. ZZ ) /\ y = <. b , Y >. ) /\ a = ( b - X ) ) -> ( y = <. ( X + a ) , Y >. <-> <. b , Y >. = <. ( X + ( b - X ) ) , Y >. ) )
90 zcn 
 |-  ( X e. ZZ -> X e. CC )
91 90 adantr 
 |-  ( ( X e. ZZ /\ Y e. ZZ ) -> X e. CC )
92 91 adantr 
 |-  ( ( ( X e. ZZ /\ Y e. ZZ ) /\ b e. ZZ ) -> X e. CC )
93 zcn 
 |-  ( b e. ZZ -> b e. CC )
94 93 adantl 
 |-  ( ( ( X e. ZZ /\ Y e. ZZ ) /\ b e. ZZ ) -> b e. CC )
95 92 94 pncan3d 
 |-  ( ( ( X e. ZZ /\ Y e. ZZ ) /\ b e. ZZ ) -> ( X + ( b - X ) ) = b )
96 95 eqcomd 
 |-  ( ( ( X e. ZZ /\ Y e. ZZ ) /\ b e. ZZ ) -> b = ( X + ( b - X ) ) )
97 96 adantr 
 |-  ( ( ( ( X e. ZZ /\ Y e. ZZ ) /\ b e. ZZ ) /\ y = <. b , Y >. ) -> b = ( X + ( b - X ) ) )
98 97 opeq1d 
 |-  ( ( ( ( X e. ZZ /\ Y e. ZZ ) /\ b e. ZZ ) /\ y = <. b , Y >. ) -> <. b , Y >. = <. ( X + ( b - X ) ) , Y >. )
99 84 89 98 rspcedvd 
 |-  ( ( ( ( X e. ZZ /\ Y e. ZZ ) /\ b e. ZZ ) /\ y = <. b , Y >. ) -> E. a e. ZZ y = <. ( X + a ) , Y >. )
100 99 ex 
 |-  ( ( ( X e. ZZ /\ Y e. ZZ ) /\ b e. ZZ ) -> ( y = <. b , Y >. -> E. a e. ZZ y = <. ( X + a ) , Y >. ) )
101 100 rexlimdva 
 |-  ( ( X e. ZZ /\ Y e. ZZ ) -> ( E. b e. ZZ y = <. b , Y >. -> E. a e. ZZ y = <. ( X + a ) , Y >. ) )
102 80 101 impbid 
 |-  ( ( X e. ZZ /\ Y e. ZZ ) -> ( E. a e. ZZ y = <. ( X + a ) , Y >. <-> E. b e. ZZ y = <. b , Y >. ) )
103 71 102 bitrid 
 |-  ( ( X e. ZZ /\ Y e. ZZ ) -> ( E. a e. ZZ y e. { <. ( X + a ) , Y >. } <-> E. b e. ZZ y = <. b , Y >. ) )
104 opeq2 
 |-  ( c = Y -> <. b , c >. = <. b , Y >. )
105 104 eqeq2d 
 |-  ( c = Y -> ( y = <. b , c >. <-> y = <. b , Y >. ) )
106 105 rexsng 
 |-  ( Y e. ZZ -> ( E. c e. { Y } y = <. b , c >. <-> y = <. b , Y >. ) )
107 106 adantl 
 |-  ( ( X e. ZZ /\ Y e. ZZ ) -> ( E. c e. { Y } y = <. b , c >. <-> y = <. b , Y >. ) )
108 107 bicomd 
 |-  ( ( X e. ZZ /\ Y e. ZZ ) -> ( y = <. b , Y >. <-> E. c e. { Y } y = <. b , c >. ) )
109 108 rexbidv 
 |-  ( ( X e. ZZ /\ Y e. ZZ ) -> ( E. b e. ZZ y = <. b , Y >. <-> E. b e. ZZ E. c e. { Y } y = <. b , c >. ) )
110 103 109 bitrd 
 |-  ( ( X e. ZZ /\ Y e. ZZ ) -> ( E. a e. ZZ y e. { <. ( X + a ) , Y >. } <-> E. b e. ZZ E. c e. { Y } y = <. b , c >. ) )
111 eliun 
 |-  ( y e. U_ a e. ZZ { <. ( X + a ) , Y >. } <-> E. a e. ZZ y e. { <. ( X + a ) , Y >. } )
112 elxp2 
 |-  ( y e. ( ZZ X. { Y } ) <-> E. b e. ZZ E. c e. { Y } y = <. b , c >. )
113 110 111 112 3bitr4g 
 |-  ( ( X e. ZZ /\ Y e. ZZ ) -> ( y e. U_ a e. ZZ { <. ( X + a ) , Y >. } <-> y e. ( ZZ X. { Y } ) ) )
114 113 eqrdv 
 |-  ( ( X e. ZZ /\ Y e. ZZ ) -> U_ a e. ZZ { <. ( X + a ) , Y >. } = ( ZZ X. { Y } ) )
115 64 69 114 3eqtrd 
 |-  ( ( X e. ZZ /\ Y e. ZZ ) -> U_ a e. ZZ { e | e = <. ( X + a ) , ( Y + 0 ) >. } = ( ZZ X. { Y } ) )
116 54 57 115 3eqtrd 
 |-  ( ( X e. ZZ /\ Y e. ZZ ) -> { e | E. a e. ZZ E. b e. { 0 } e = ( <. X , Y >. ( +g ` R ) <. a , b >. ) } = ( ZZ X. { Y } ) )
117 24 31 116 3eqtrd 
 |-  ( ( X e. ZZ /\ Y e. ZZ ) -> ran ( x e. I |-> ( <. X , Y >. ( +g ` R ) x ) ) = ( ZZ X. { Y } ) )
118 20 21 117 3eqtrd 
 |-  ( ( X e. ZZ /\ Y e. ZZ ) -> [ <. X , Y >. ] .~ = ( ZZ X. { Y } ) )