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 ⊢ 𝑅 = ( ℤring ×s ℤring )
pzriprng.i ⊢ 𝐼 = ( ℤ × { 0 } )
pzriprng.j ⊢ 𝐽 = ( 𝑅 ↾s 𝐼 )
pzriprng.1 ⊢ 1 = ( 1r ‘ 𝐽 )
pzriprng.g ⊢ ∼ = ( 𝑅 ~QG 𝐼 )
Assertion pzriprnglem10 ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → [ ⟨ 𝑋 , 𝑌 ⟩ ] ∼ = ( ℤ × { 𝑌 } ) )

Proof

Step Hyp Ref Expression
1 pzriprng.r ⊢ 𝑅 = ( ℤring ×s ℤring )
2 pzriprng.i ⊢ 𝐼 = ( ℤ × { 0 } )
3 pzriprng.j ⊢ 𝐽 = ( 𝑅 ↾s 𝐼 )
4 pzriprng.1 ⊢ 1 = ( 1r ‘ 𝐽 )
5 pzriprng.g ⊢ ∼ = ( 𝑅 ~QG 𝐼 )
6 1 pzriprnglem1 ⊢ 𝑅 ∈ Rng
7 rnggrp ⊢ ( 𝑅 ∈ Rng → 𝑅 ∈ Grp )
8 6 7 ax-mp ⊢ 𝑅 ∈ Grp
9 0z ⊢ 0 ∈ ℤ
10 snssi ⊢ ( 0 ∈ ℤ → { 0 } ⊆ ℤ )
11 xpss2 ⊢ ( { 0 } ⊆ ℤ → ( ℤ × { 0 } ) ⊆ ( ℤ × ℤ ) )
12 9 10 11 mp2b ⊢ ( ℤ × { 0 } ) ⊆ ( ℤ × ℤ )
13 2 12 eqsstri ⊢ 𝐼 ⊆ ( ℤ × ℤ )
14 13 a1i ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → 𝐼 ⊆ ( ℤ × ℤ ) )
15 opelxpi ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → ⟨ 𝑋 , 𝑌 ⟩ ∈ ( ℤ × ℤ ) )
16 1 pzriprnglem2 ⊢ ( Base ‘ 𝑅 ) = ( ℤ × ℤ )
17 16 eqcomi ⊢ ( ℤ × ℤ ) = ( Base ‘ 𝑅 )
18 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
19 17 5 18 eqglact ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐼 ⊆ ( ℤ × ℤ ) ∧ ⟨ 𝑋 , 𝑌 ⟩ ∈ ( ℤ × ℤ ) ) → [ ⟨ 𝑋 , 𝑌 ⟩ ] ∼ = ( ( 𝑥 ∈ ( ℤ × ℤ ) ↦ ( ⟨ 𝑋 , 𝑌 ⟩ ( +g ‘ 𝑅 ) 𝑥 ) ) “ 𝐼 ) )
20 8 14 15 19 mp3an2i ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → [ ⟨ 𝑋 , 𝑌 ⟩ ] ∼ = ( ( 𝑥 ∈ ( ℤ × ℤ ) ↦ ( ⟨ 𝑋 , 𝑌 ⟩ ( +g ‘ 𝑅 ) 𝑥 ) ) “ 𝐼 ) )
21 14 mptimass ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → ( ( 𝑥 ∈ ( ℤ × ℤ ) ↦ ( ⟨ 𝑋 , 𝑌 ⟩ ( +g ‘ 𝑅 ) 𝑥 ) ) “ 𝐼 ) = ran ( 𝑥 ∈ 𝐼 ↦ ( ⟨ 𝑋 , 𝑌 ⟩ ( +g ‘ 𝑅 ) 𝑥 ) ) )
22 eqid ⊢ ( 𝑥 ∈ 𝐼 ↦ ( ⟨ 𝑋 , 𝑌 ⟩ ( +g ‘ 𝑅 ) 𝑥 ) ) = ( 𝑥 ∈ 𝐼 ↦ ( ⟨ 𝑋 , 𝑌 ⟩ ( +g ‘ 𝑅 ) 𝑥 ) )
23 22 rnmpt ⊢ ran ( 𝑥 ∈ 𝐼 ↦ ( ⟨ 𝑋 , 𝑌 ⟩ ( +g ‘ 𝑅 ) 𝑥 ) ) = { 𝑒 ∣ ∃ 𝑥 ∈ 𝐼 𝑒 = ( ⟨ 𝑋 , 𝑌 ⟩ ( +g ‘ 𝑅 ) 𝑥 ) }
24 23 a1i ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → ran ( 𝑥 ∈ 𝐼 ↦ ( ⟨ 𝑋 , 𝑌 ⟩ ( +g ‘ 𝑅 ) 𝑥 ) ) = { 𝑒 ∣ ∃ 𝑥 ∈ 𝐼 𝑒 = ( ⟨ 𝑋 , 𝑌 ⟩ ( +g ‘ 𝑅 ) 𝑥 ) } )
25 2 rexeqi ⊢ ( ∃ 𝑥 ∈ 𝐼 𝑒 = ( ⟨ 𝑋 , 𝑌 ⟩ ( +g ‘ 𝑅 ) 𝑥 ) ↔ ∃ 𝑥 ∈ ( ℤ × { 0 } ) 𝑒 = ( ⟨ 𝑋 , 𝑌 ⟩ ( +g ‘ 𝑅 ) 𝑥 ) )
26 oveq2 ⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → ( ⟨ 𝑋 , 𝑌 ⟩ ( +g ‘ 𝑅 ) 𝑥 ) = ( ⟨ 𝑋 , 𝑌 ⟩ ( +g ‘ 𝑅 ) ⟨ 𝑎 , 𝑏 ⟩ ) )
27 26 eqeq2d ⊢ ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → ( 𝑒 = ( ⟨ 𝑋 , 𝑌 ⟩ ( +g ‘ 𝑅 ) 𝑥 ) ↔ 𝑒 = ( ⟨ 𝑋 , 𝑌 ⟩ ( +g ‘ 𝑅 ) ⟨ 𝑎 , 𝑏 ⟩ ) ) )
28 27 rexxp ⊢ ( ∃ 𝑥 ∈ ( ℤ × { 0 } ) 𝑒 = ( ⟨ 𝑋 , 𝑌 ⟩ ( +g ‘ 𝑅 ) 𝑥 ) ↔ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ { 0 } 𝑒 = ( ⟨ 𝑋 , 𝑌 ⟩ ( +g ‘ 𝑅 ) ⟨ 𝑎 , 𝑏 ⟩ ) )
29 25 28 bitri ⊢ ( ∃ 𝑥 ∈ 𝐼 𝑒 = ( ⟨ 𝑋 , 𝑌 ⟩ ( +g ‘ 𝑅 ) 𝑥 ) ↔ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ { 0 } 𝑒 = ( ⟨ 𝑋 , 𝑌 ⟩ ( +g ‘ 𝑅 ) ⟨ 𝑎 , 𝑏 ⟩ ) )
30 29 a1i ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → ( ∃ 𝑥 ∈ 𝐼 𝑒 = ( ⟨ 𝑋 , 𝑌 ⟩ ( +g ‘ 𝑅 ) 𝑥 ) ↔ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ { 0 } 𝑒 = ( ⟨ 𝑋 , 𝑌 ⟩ ( +g ‘ 𝑅 ) ⟨ 𝑎 , 𝑏 ⟩ ) ) )
31 30 abbidv ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → { 𝑒 ∣ ∃ 𝑥 ∈ 𝐼 𝑒 = ( ⟨ 𝑋 , 𝑌 ⟩ ( +g ‘ 𝑅 ) 𝑥 ) } = { 𝑒 ∣ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ { 0 } 𝑒 = ( ⟨ 𝑋 , 𝑌 ⟩ ( +g ‘ 𝑅 ) ⟨ 𝑎 , 𝑏 ⟩ ) } )
32 c0ex ⊢ 0 ∈ V
33 opeq2 ⊢ ( 𝑏 = 0 → ⟨ 𝑎 , 𝑏 ⟩ = ⟨ 𝑎 , 0 ⟩ )
34 33 oveq2d ⊢ ( 𝑏 = 0 → ( ⟨ 𝑋 , 𝑌 ⟩ ( +g ‘ 𝑅 ) ⟨ 𝑎 , 𝑏 ⟩ ) = ( ⟨ 𝑋 , 𝑌 ⟩ ( +g ‘ 𝑅 ) ⟨ 𝑎 , 0 ⟩ ) )
35 34 eqeq2d ⊢ ( 𝑏 = 0 → ( 𝑒 = ( ⟨ 𝑋 , 𝑌 ⟩ ( +g ‘ 𝑅 ) ⟨ 𝑎 , 𝑏 ⟩ ) ↔ 𝑒 = ( ⟨ 𝑋 , 𝑌 ⟩ ( +g ‘ 𝑅 ) ⟨ 𝑎 , 0 ⟩ ) ) )
36 32 35 rexsn ⊢ ( ∃ 𝑏 ∈ { 0 } 𝑒 = ( ⟨ 𝑋 , 𝑌 ⟩ ( +g ‘ 𝑅 ) ⟨ 𝑎 , 𝑏 ⟩ ) ↔ 𝑒 = ( ⟨ 𝑋 , 𝑌 ⟩ ( +g ‘ 𝑅 ) ⟨ 𝑎 , 0 ⟩ ) )
37 zringbas ⊢ ℤ = ( Base ‘ ℤring )
38 zringring ⊢ ℤring ∈ Ring
39 38 a1i ⊢ ( ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ∧ 𝑎 ∈ ℤ ) → ℤring ∈ Ring )
40 simpll ⊢ ( ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ∧ 𝑎 ∈ ℤ ) → 𝑋 ∈ ℤ )
41 simplr ⊢ ( ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ∧ 𝑎 ∈ ℤ ) → 𝑌 ∈ ℤ )
42 simpr ⊢ ( ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ∧ 𝑎 ∈ ℤ ) → 𝑎 ∈ ℤ )
43 0zd ⊢ ( ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ∧ 𝑎 ∈ ℤ ) → 0 ∈ ℤ )
44 40 42 zaddcld ⊢ ( ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ∧ 𝑎 ∈ ℤ ) → ( 𝑋 + 𝑎 ) ∈ ℤ )
45 simpr ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → 𝑌 ∈ ℤ )
46 0zd ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → 0 ∈ ℤ )
47 45 46 zaddcld ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → ( 𝑌 + 0 ) ∈ ℤ )
48 47 adantr ⊢ ( ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ∧ 𝑎 ∈ ℤ ) → ( 𝑌 + 0 ) ∈ ℤ )
49 zringplusg ⊢ + = ( +g ‘ ℤring )
50 1 37 37 39 39 40 41 42 43 44 48 49 49 18 xpsadd ⊢ ( ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ∧ 𝑎 ∈ ℤ ) → ( ⟨ 𝑋 , 𝑌 ⟩ ( +g ‘ 𝑅 ) ⟨ 𝑎 , 0 ⟩ ) = ⟨ ( 𝑋 + 𝑎 ) , ( 𝑌 + 0 ) ⟩ )
51 50 eqeq2d ⊢ ( ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ∧ 𝑎 ∈ ℤ ) → ( 𝑒 = ( ⟨ 𝑋 , 𝑌 ⟩ ( +g ‘ 𝑅 ) ⟨ 𝑎 , 0 ⟩ ) ↔ 𝑒 = ⟨ ( 𝑋 + 𝑎 ) , ( 𝑌 + 0 ) ⟩ ) )
52 36 51 bitrid ⊢ ( ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ∧ 𝑎 ∈ ℤ ) → ( ∃ 𝑏 ∈ { 0 } 𝑒 = ( ⟨ 𝑋 , 𝑌 ⟩ ( +g ‘ 𝑅 ) ⟨ 𝑎 , 𝑏 ⟩ ) ↔ 𝑒 = ⟨ ( 𝑋 + 𝑎 ) , ( 𝑌 + 0 ) ⟩ ) )
53 52 rexbidva ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → ( ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ { 0 } 𝑒 = ( ⟨ 𝑋 , 𝑌 ⟩ ( +g ‘ 𝑅 ) ⟨ 𝑎 , 𝑏 ⟩ ) ↔ ∃ 𝑎 ∈ ℤ 𝑒 = ⟨ ( 𝑋 + 𝑎 ) , ( 𝑌 + 0 ) ⟩ ) )
54 53 abbidv ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → { 𝑒 ∣ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ { 0 } 𝑒 = ( ⟨ 𝑋 , 𝑌 ⟩ ( +g ‘ 𝑅 ) ⟨ 𝑎 , 𝑏 ⟩ ) } = { 𝑒 ∣ ∃ 𝑎 ∈ ℤ 𝑒 = ⟨ ( 𝑋 + 𝑎 ) , ( 𝑌 + 0 ) ⟩ } )
55 iunab ⊢ ∪ 𝑎 ∈ ℤ { 𝑒 ∣ 𝑒 = ⟨ ( 𝑋 + 𝑎 ) , ( 𝑌 + 0 ) ⟩ } = { 𝑒 ∣ ∃ 𝑎 ∈ ℤ 𝑒 = ⟨ ( 𝑋 + 𝑎 ) , ( 𝑌 + 0 ) ⟩ }
56 55 eqcomi ⊢ { 𝑒 ∣ ∃ 𝑎 ∈ ℤ 𝑒 = ⟨ ( 𝑋 + 𝑎 ) , ( 𝑌 + 0 ) ⟩ } = ∪ 𝑎 ∈ ℤ { 𝑒 ∣ 𝑒 = ⟨ ( 𝑋 + 𝑎 ) , ( 𝑌 + 0 ) ⟩ }
57 56 a1i ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → { 𝑒 ∣ ∃ 𝑎 ∈ ℤ 𝑒 = ⟨ ( 𝑋 + 𝑎 ) , ( 𝑌 + 0 ) ⟩ } = ∪ 𝑎 ∈ ℤ { 𝑒 ∣ 𝑒 = ⟨ ( 𝑋 + 𝑎 ) , ( 𝑌 + 0 ) ⟩ } )
58 zcn ⊢ ( 𝑌 ∈ ℤ → 𝑌 ∈ ℂ )
59 58 adantl ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → 𝑌 ∈ ℂ )
60 59 addridd ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → ( 𝑌 + 0 ) = 𝑌 )
61 60 opeq2d ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → ⟨ ( 𝑋 + 𝑎 ) , ( 𝑌 + 0 ) ⟩ = ⟨ ( 𝑋 + 𝑎 ) , 𝑌 ⟩ )
62 61 eqeq2d ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → ( 𝑒 = ⟨ ( 𝑋 + 𝑎 ) , ( 𝑌 + 0 ) ⟩ ↔ 𝑒 = ⟨ ( 𝑋 + 𝑎 ) , 𝑌 ⟩ ) )
63 62 abbidv ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → { 𝑒 ∣ 𝑒 = ⟨ ( 𝑋 + 𝑎 ) , ( 𝑌 + 0 ) ⟩ } = { 𝑒 ∣ 𝑒 = ⟨ ( 𝑋 + 𝑎 ) , 𝑌 ⟩ } )
64 63 iuneq2d ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → ∪ 𝑎 ∈ ℤ { 𝑒 ∣ 𝑒 = ⟨ ( 𝑋 + 𝑎 ) , ( 𝑌 + 0 ) ⟩ } = ∪ 𝑎 ∈ ℤ { 𝑒 ∣ 𝑒 = ⟨ ( 𝑋 + 𝑎 ) , 𝑌 ⟩ } )
65 df-sn ⊢ { ⟨ ( 𝑋 + 𝑎 ) , 𝑌 ⟩ } = { 𝑒 ∣ 𝑒 = ⟨ ( 𝑋 + 𝑎 ) , 𝑌 ⟩ }
66 65 eqcomi ⊢ { 𝑒 ∣ 𝑒 = ⟨ ( 𝑋 + 𝑎 ) , 𝑌 ⟩ } = { ⟨ ( 𝑋 + 𝑎 ) , 𝑌 ⟩ }
67 66 a1i ⊢ ( 𝑎 ∈ ℤ → { 𝑒 ∣ 𝑒 = ⟨ ( 𝑋 + 𝑎 ) , 𝑌 ⟩ } = { ⟨ ( 𝑋 + 𝑎 ) , 𝑌 ⟩ } )
68 67 iuneq2i ⊢ ∪ 𝑎 ∈ ℤ { 𝑒 ∣ 𝑒 = ⟨ ( 𝑋 + 𝑎 ) , 𝑌 ⟩ } = ∪ 𝑎 ∈ ℤ { ⟨ ( 𝑋 + 𝑎 ) , 𝑌 ⟩ }
69 68 a1i ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → ∪ 𝑎 ∈ ℤ { 𝑒 ∣ 𝑒 = ⟨ ( 𝑋 + 𝑎 ) , 𝑌 ⟩ } = ∪ 𝑎 ∈ ℤ { ⟨ ( 𝑋 + 𝑎 ) , 𝑌 ⟩ } )
70 velsn ⊢ ( 𝑦 ∈ { ⟨ ( 𝑋 + 𝑎 ) , 𝑌 ⟩ } ↔ 𝑦 = ⟨ ( 𝑋 + 𝑎 ) , 𝑌 ⟩ )
71 70 rexbii ⊢ ( ∃ 𝑎 ∈ ℤ 𝑦 ∈ { ⟨ ( 𝑋 + 𝑎 ) , 𝑌 ⟩ } ↔ ∃ 𝑎 ∈ ℤ 𝑦 = ⟨ ( 𝑋 + 𝑎 ) , 𝑌 ⟩ )
72 44 adantr ⊢ ( ( ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑦 = ⟨ ( 𝑋 + 𝑎 ) , 𝑌 ⟩ ) → ( 𝑋 + 𝑎 ) ∈ ℤ )
73 simplr ⊢ ( ( ( ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑦 = ⟨ ( 𝑋 + 𝑎 ) , 𝑌 ⟩ ) ∧ 𝑏 = ( 𝑋 + 𝑎 ) ) → 𝑦 = ⟨ ( 𝑋 + 𝑎 ) , 𝑌 ⟩ )
74 opeq1 ⊢ ( 𝑏 = ( 𝑋 + 𝑎 ) → ⟨ 𝑏 , 𝑌 ⟩ = ⟨ ( 𝑋 + 𝑎 ) , 𝑌 ⟩ )
75 74 adantl ⊢ ( ( ( ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑦 = ⟨ ( 𝑋 + 𝑎 ) , 𝑌 ⟩ ) ∧ 𝑏 = ( 𝑋 + 𝑎 ) ) → ⟨ 𝑏 , 𝑌 ⟩ = ⟨ ( 𝑋 + 𝑎 ) , 𝑌 ⟩ )
76 73 75 eqeq12d ⊢ ( ( ( ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑦 = ⟨ ( 𝑋 + 𝑎 ) , 𝑌 ⟩ ) ∧ 𝑏 = ( 𝑋 + 𝑎 ) ) → ( 𝑦 = ⟨ 𝑏 , 𝑌 ⟩ ↔ ⟨ ( 𝑋 + 𝑎 ) , 𝑌 ⟩ = ⟨ ( 𝑋 + 𝑎 ) , 𝑌 ⟩ ) )
77 eqidd ⊢ ( ( ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑦 = ⟨ ( 𝑋 + 𝑎 ) , 𝑌 ⟩ ) → ⟨ ( 𝑋 + 𝑎 ) , 𝑌 ⟩ = ⟨ ( 𝑋 + 𝑎 ) , 𝑌 ⟩ )
78 72 76 77 rspcedvd ⊢ ( ( ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ∧ 𝑎 ∈ ℤ ) ∧ 𝑦 = ⟨ ( 𝑋 + 𝑎 ) , 𝑌 ⟩ ) → ∃ 𝑏 ∈ ℤ 𝑦 = ⟨ 𝑏 , 𝑌 ⟩ )
79 78 ex ⊢ ( ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ∧ 𝑎 ∈ ℤ ) → ( 𝑦 = ⟨ ( 𝑋 + 𝑎 ) , 𝑌 ⟩ → ∃ 𝑏 ∈ ℤ 𝑦 = ⟨ 𝑏 , 𝑌 ⟩ ) )
80 79 rexlimdva ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → ( ∃ 𝑎 ∈ ℤ 𝑦 = ⟨ ( 𝑋 + 𝑎 ) , 𝑌 ⟩ → ∃ 𝑏 ∈ ℤ 𝑦 = ⟨ 𝑏 , 𝑌 ⟩ ) )
81 simpr ⊢ ( ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ∧ 𝑏 ∈ ℤ ) → 𝑏 ∈ ℤ )
82 simpll ⊢ ( ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ∧ 𝑏 ∈ ℤ ) → 𝑋 ∈ ℤ )
83 81 82 zsubcld ⊢ ( ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ∧ 𝑏 ∈ ℤ ) → ( 𝑏 − 𝑋 ) ∈ ℤ )
84 83 adantr ⊢ ( ( ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ∧ 𝑏 ∈ ℤ ) ∧ 𝑦 = ⟨ 𝑏 , 𝑌 ⟩ ) → ( 𝑏 − 𝑋 ) ∈ ℤ )
85 simplr ⊢ ( ( ( ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ∧ 𝑏 ∈ ℤ ) ∧ 𝑦 = ⟨ 𝑏 , 𝑌 ⟩ ) ∧ 𝑎 = ( 𝑏 − 𝑋 ) ) → 𝑦 = ⟨ 𝑏 , 𝑌 ⟩ )
86 oveq2 ⊢ ( 𝑎 = ( 𝑏 − 𝑋 ) → ( 𝑋 + 𝑎 ) = ( 𝑋 + ( 𝑏 − 𝑋 ) ) )
87 86 adantl ⊢ ( ( ( ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ∧ 𝑏 ∈ ℤ ) ∧ 𝑦 = ⟨ 𝑏 , 𝑌 ⟩ ) ∧ 𝑎 = ( 𝑏 − 𝑋 ) ) → ( 𝑋 + 𝑎 ) = ( 𝑋 + ( 𝑏 − 𝑋 ) ) )
88 87 opeq1d ⊢ ( ( ( ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ∧ 𝑏 ∈ ℤ ) ∧ 𝑦 = ⟨ 𝑏 , 𝑌 ⟩ ) ∧ 𝑎 = ( 𝑏 − 𝑋 ) ) → ⟨ ( 𝑋 + 𝑎 ) , 𝑌 ⟩ = ⟨ ( 𝑋 + ( 𝑏 − 𝑋 ) ) , 𝑌 ⟩ )
89 85 88 eqeq12d ⊢ ( ( ( ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ∧ 𝑏 ∈ ℤ ) ∧ 𝑦 = ⟨ 𝑏 , 𝑌 ⟩ ) ∧ 𝑎 = ( 𝑏 − 𝑋 ) ) → ( 𝑦 = ⟨ ( 𝑋 + 𝑎 ) , 𝑌 ⟩ ↔ ⟨ 𝑏 , 𝑌 ⟩ = ⟨ ( 𝑋 + ( 𝑏 − 𝑋 ) ) , 𝑌 ⟩ ) )
90 zcn ⊢ ( 𝑋 ∈ ℤ → 𝑋 ∈ ℂ )
91 90 adantr ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → 𝑋 ∈ ℂ )
92 91 adantr ⊢ ( ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ∧ 𝑏 ∈ ℤ ) → 𝑋 ∈ ℂ )
93 zcn ⊢ ( 𝑏 ∈ ℤ → 𝑏 ∈ ℂ )
94 93 adantl ⊢ ( ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ∧ 𝑏 ∈ ℤ ) → 𝑏 ∈ ℂ )
95 92 94 pncan3d ⊢ ( ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ∧ 𝑏 ∈ ℤ ) → ( 𝑋 + ( 𝑏 − 𝑋 ) ) = 𝑏 )
96 95 eqcomd ⊢ ( ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ∧ 𝑏 ∈ ℤ ) → 𝑏 = ( 𝑋 + ( 𝑏 − 𝑋 ) ) )
97 96 adantr ⊢ ( ( ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ∧ 𝑏 ∈ ℤ ) ∧ 𝑦 = ⟨ 𝑏 , 𝑌 ⟩ ) → 𝑏 = ( 𝑋 + ( 𝑏 − 𝑋 ) ) )
98 97 opeq1d ⊢ ( ( ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ∧ 𝑏 ∈ ℤ ) ∧ 𝑦 = ⟨ 𝑏 , 𝑌 ⟩ ) → ⟨ 𝑏 , 𝑌 ⟩ = ⟨ ( 𝑋 + ( 𝑏 − 𝑋 ) ) , 𝑌 ⟩ )
99 84 89 98 rspcedvd ⊢ ( ( ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ∧ 𝑏 ∈ ℤ ) ∧ 𝑦 = ⟨ 𝑏 , 𝑌 ⟩ ) → ∃ 𝑎 ∈ ℤ 𝑦 = ⟨ ( 𝑋 + 𝑎 ) , 𝑌 ⟩ )
100 99 ex ⊢ ( ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) ∧ 𝑏 ∈ ℤ ) → ( 𝑦 = ⟨ 𝑏 , 𝑌 ⟩ → ∃ 𝑎 ∈ ℤ 𝑦 = ⟨ ( 𝑋 + 𝑎 ) , 𝑌 ⟩ ) )
101 100 rexlimdva ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → ( ∃ 𝑏 ∈ ℤ 𝑦 = ⟨ 𝑏 , 𝑌 ⟩ → ∃ 𝑎 ∈ ℤ 𝑦 = ⟨ ( 𝑋 + 𝑎 ) , 𝑌 ⟩ ) )
102 80 101 impbid ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → ( ∃ 𝑎 ∈ ℤ 𝑦 = ⟨ ( 𝑋 + 𝑎 ) , 𝑌 ⟩ ↔ ∃ 𝑏 ∈ ℤ 𝑦 = ⟨ 𝑏 , 𝑌 ⟩ ) )
103 71 102 bitrid ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → ( ∃ 𝑎 ∈ ℤ 𝑦 ∈ { ⟨ ( 𝑋 + 𝑎 ) , 𝑌 ⟩ } ↔ ∃ 𝑏 ∈ ℤ 𝑦 = ⟨ 𝑏 , 𝑌 ⟩ ) )
104 opeq2 ⊢ ( 𝑐 = 𝑌 → ⟨ 𝑏 , 𝑐 ⟩ = ⟨ 𝑏 , 𝑌 ⟩ )
105 104 eqeq2d ⊢ ( 𝑐 = 𝑌 → ( 𝑦 = ⟨ 𝑏 , 𝑐 ⟩ ↔ 𝑦 = ⟨ 𝑏 , 𝑌 ⟩ ) )
106 105 rexsng ⊢ ( 𝑌 ∈ ℤ → ( ∃ 𝑐 ∈ { 𝑌 } 𝑦 = ⟨ 𝑏 , 𝑐 ⟩ ↔ 𝑦 = ⟨ 𝑏 , 𝑌 ⟩ ) )
107 106 adantl ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → ( ∃ 𝑐 ∈ { 𝑌 } 𝑦 = ⟨ 𝑏 , 𝑐 ⟩ ↔ 𝑦 = ⟨ 𝑏 , 𝑌 ⟩ ) )
108 107 bicomd ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → ( 𝑦 = ⟨ 𝑏 , 𝑌 ⟩ ↔ ∃ 𝑐 ∈ { 𝑌 } 𝑦 = ⟨ 𝑏 , 𝑐 ⟩ ) )
109 108 rexbidv ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → ( ∃ 𝑏 ∈ ℤ 𝑦 = ⟨ 𝑏 , 𝑌 ⟩ ↔ ∃ 𝑏 ∈ ℤ ∃ 𝑐 ∈ { 𝑌 } 𝑦 = ⟨ 𝑏 , 𝑐 ⟩ ) )
110 103 109 bitrd ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → ( ∃ 𝑎 ∈ ℤ 𝑦 ∈ { ⟨ ( 𝑋 + 𝑎 ) , 𝑌 ⟩ } ↔ ∃ 𝑏 ∈ ℤ ∃ 𝑐 ∈ { 𝑌 } 𝑦 = ⟨ 𝑏 , 𝑐 ⟩ ) )
111 eliun ⊢ ( 𝑦 ∈ ∪ 𝑎 ∈ ℤ { ⟨ ( 𝑋 + 𝑎 ) , 𝑌 ⟩ } ↔ ∃ 𝑎 ∈ ℤ 𝑦 ∈ { ⟨ ( 𝑋 + 𝑎 ) , 𝑌 ⟩ } )
112 elxp2 ⊢ ( 𝑦 ∈ ( ℤ × { 𝑌 } ) ↔ ∃ 𝑏 ∈ ℤ ∃ 𝑐 ∈ { 𝑌 } 𝑦 = ⟨ 𝑏 , 𝑐 ⟩ )
113 110 111 112 3bitr4g ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → ( 𝑦 ∈ ∪ 𝑎 ∈ ℤ { ⟨ ( 𝑋 + 𝑎 ) , 𝑌 ⟩ } ↔ 𝑦 ∈ ( ℤ × { 𝑌 } ) ) )
114 113 eqrdv ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → ∪ 𝑎 ∈ ℤ { ⟨ ( 𝑋 + 𝑎 ) , 𝑌 ⟩ } = ( ℤ × { 𝑌 } ) )
115 64 69 114 3eqtrd ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → ∪ 𝑎 ∈ ℤ { 𝑒 ∣ 𝑒 = ⟨ ( 𝑋 + 𝑎 ) , ( 𝑌 + 0 ) ⟩ } = ( ℤ × { 𝑌 } ) )
116 54 57 115 3eqtrd ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → { 𝑒 ∣ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ { 0 } 𝑒 = ( ⟨ 𝑋 , 𝑌 ⟩ ( +g ‘ 𝑅 ) ⟨ 𝑎 , 𝑏 ⟩ ) } = ( ℤ × { 𝑌 } ) )
117 24 31 116 3eqtrd ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → ran ( 𝑥 ∈ 𝐼 ↦ ( ⟨ 𝑋 , 𝑌 ⟩ ( +g ‘ 𝑅 ) 𝑥 ) ) = ( ℤ × { 𝑌 } ) )
118 20 21 117 3eqtrd ⊢ ( ( 𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ ) → [ ⟨ 𝑋 , 𝑌 ⟩ ] ∼ = ( ℤ × { 𝑌 } ) )