Metamath Proof Explorer

Theorem pzriprnglem12

Description: Lemma 12 for pzriprng : Q has a ring unity. (Contributed by AV, 23-Mar-2025)

Ref Expression
Hypotheses pzriprng.r ⊢ 𝑅 = ( ℤring ×s ℤring )
pzriprng.i ⊢ 𝐼 = ( ℤ × { 0 } )
pzriprng.j ⊢ 𝐽 = ( 𝑅 ↾s 𝐼 )
pzriprng.1 ⊢ 1 = ( 1r ‘ 𝐽 )
pzriprng.g ⊢ ∼ = ( 𝑅 ~QG 𝐼 )
pzriprng.q ⊢ 𝑄 = ( 𝑅 /s ∼ )
Assertion pzriprnglem12 ( 𝑋 ∈ ( Base ‘ 𝑄 ) → ( ( ( ℤ × { 1 } ) ( .r ‘ 𝑄 ) 𝑋 ) = 𝑋 ∧ ( 𝑋 ( .r ‘ 𝑄 ) ( ℤ × { 1 } ) ) = 𝑋 ) )

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 pzriprng.q ⊢ 𝑄 = ( 𝑅 /s ∼ )
7 1 2 3 4 5 6 pzriprnglem11 ⊢ ( Base ‘ 𝑄 ) = ∪ 𝑦 ∈ ℤ { ( ℤ × { 𝑦 } ) }
8 7 eleq2i ⊢ ( 𝑋 ∈ ( Base ‘ 𝑄 ) ↔ 𝑋 ∈ ∪ 𝑦 ∈ ℤ { ( ℤ × { 𝑦 } ) } )
9 eliun ⊢ ( 𝑋 ∈ ∪ 𝑦 ∈ ℤ { ( ℤ × { 𝑦 } ) } ↔ ∃ 𝑦 ∈ ℤ 𝑋 ∈ { ( ℤ × { 𝑦 } ) } )
10 8 9 bitri ⊢ ( 𝑋 ∈ ( Base ‘ 𝑄 ) ↔ ∃ 𝑦 ∈ ℤ 𝑋 ∈ { ( ℤ × { 𝑦 } ) } )
11 elsni ⊢ ( 𝑋 ∈ { ( ℤ × { 𝑦 } ) } → 𝑋 = ( ℤ × { 𝑦 } ) )
12 1z ⊢ 1 ∈ ℤ
13 1 2 3 4 5 pzriprnglem10 ⊢ ( ( 1 ∈ ℤ ∧ 𝑦 ∈ ℤ ) → [ ⟨ 1 , 𝑦 ⟩ ] ∼ = ( ℤ × { 𝑦 } ) )
14 12 13 mpan ⊢ ( 𝑦 ∈ ℤ → [ ⟨ 1 , 𝑦 ⟩ ] ∼ = ( ℤ × { 𝑦 } ) )
15 14 eqcomd ⊢ ( 𝑦 ∈ ℤ → ( ℤ × { 𝑦 } ) = [ ⟨ 1 , 𝑦 ⟩ ] ∼ )
16 15 eqeq2d ⊢ ( 𝑦 ∈ ℤ → ( 𝑋 = ( ℤ × { 𝑦 } ) ↔ 𝑋 = [ ⟨ 1 , 𝑦 ⟩ ] ∼ ) )
17 1 pzriprnglem1 ⊢ 𝑅 ∈ Rng
18 17 a1i ⊢ ( 𝑦 ∈ ℤ → 𝑅 ∈ Rng )
19 1 2 3 pzriprnglem8 ⊢ 𝐼 ∈ ( 2Ideal ‘ 𝑅 )
20 19 a1i ⊢ ( 𝑦 ∈ ℤ → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
21 1 2 pzriprnglem4 ⊢ 𝐼 ∈ ( SubGrp ‘ 𝑅 )
22 21 a1i ⊢ ( 𝑦 ∈ ℤ → 𝐼 ∈ ( SubGrp ‘ 𝑅 ) )
23 12 a1i ⊢ ( 𝑦 ∈ ℤ → 1 ∈ ℤ )
24 23 23 opelxpd ⊢ ( 𝑦 ∈ ℤ → ⟨ 1 , 1 ⟩ ∈ ( ℤ × ℤ ) )
25 id ⊢ ( 𝑦 ∈ ℤ → 𝑦 ∈ ℤ )
26 23 25 opelxpd ⊢ ( 𝑦 ∈ ℤ → ⟨ 1 , 𝑦 ⟩ ∈ ( ℤ × ℤ ) )
27 1 pzriprnglem2 ⊢ ( Base ‘ 𝑅 ) = ( ℤ × ℤ )
28 27 eqcomi ⊢ ( ℤ × ℤ ) = ( Base ‘ 𝑅 )
29 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
30 eqid ⊢ ( .r ‘ 𝑄 ) = ( .r ‘ 𝑄 )
31 5 6 28 29 30 qusmulrng ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( ⟨ 1 , 1 ⟩ ∈ ( ℤ × ℤ ) ∧ ⟨ 1 , 𝑦 ⟩ ∈ ( ℤ × ℤ ) ) ) → ( [ ⟨ 1 , 1 ⟩ ] ∼ ( .r ‘ 𝑄 ) [ ⟨ 1 , 𝑦 ⟩ ] ∼ ) = [ ( ⟨ 1 , 1 ⟩ ( .r ‘ 𝑅 ) ⟨ 1 , 𝑦 ⟩ ) ] ∼ )
32 18 20 22 24 26 31 syl32anc ⊢ ( 𝑦 ∈ ℤ → ( [ ⟨ 1 , 1 ⟩ ] ∼ ( .r ‘ 𝑄 ) [ ⟨ 1 , 𝑦 ⟩ ] ∼ ) = [ ( ⟨ 1 , 1 ⟩ ( .r ‘ 𝑅 ) ⟨ 1 , 𝑦 ⟩ ) ] ∼ )
33 zringbas ⊢ ℤ = ( Base ‘ ℤring )
34 zringring ⊢ ℤring ∈ Ring
35 34 a1i ⊢ ( 𝑦 ∈ ℤ → ℤring ∈ Ring )
36 23 23 zmulcld ⊢ ( 𝑦 ∈ ℤ → ( 1 · 1 ) ∈ ℤ )
37 23 25 zmulcld ⊢ ( 𝑦 ∈ ℤ → ( 1 · 𝑦 ) ∈ ℤ )
38 zringmulr ⊢ · = ( .r ‘ ℤring )
39 1 33 33 35 35 23 23 23 25 36 37 38 38 29 xpsmul ⊢ ( 𝑦 ∈ ℤ → ( ⟨ 1 , 1 ⟩ ( .r ‘ 𝑅 ) ⟨ 1 , 𝑦 ⟩ ) = ⟨ ( 1 · 1 ) , ( 1 · 𝑦 ) ⟩ )
40 1cnd ⊢ ( 𝑦 ∈ ℤ → 1 ∈ ℂ )
41 40 mulridd ⊢ ( 𝑦 ∈ ℤ → ( 1 · 1 ) = 1 )
42 zcn ⊢ ( 𝑦 ∈ ℤ → 𝑦 ∈ ℂ )
43 42 mullidd ⊢ ( 𝑦 ∈ ℤ → ( 1 · 𝑦 ) = 𝑦 )
44 41 43 opeq12d ⊢ ( 𝑦 ∈ ℤ → ⟨ ( 1 · 1 ) , ( 1 · 𝑦 ) ⟩ = ⟨ 1 , 𝑦 ⟩ )
45 39 44 eqtrd ⊢ ( 𝑦 ∈ ℤ → ( ⟨ 1 , 1 ⟩ ( .r ‘ 𝑅 ) ⟨ 1 , 𝑦 ⟩ ) = ⟨ 1 , 𝑦 ⟩ )
46 45 eceq1d ⊢ ( 𝑦 ∈ ℤ → [ ( ⟨ 1 , 1 ⟩ ( .r ‘ 𝑅 ) ⟨ 1 , 𝑦 ⟩ ) ] ∼ = [ ⟨ 1 , 𝑦 ⟩ ] ∼ )
47 32 46 eqtrd ⊢ ( 𝑦 ∈ ℤ → ( [ ⟨ 1 , 1 ⟩ ] ∼ ( .r ‘ 𝑄 ) [ ⟨ 1 , 𝑦 ⟩ ] ∼ ) = [ ⟨ 1 , 𝑦 ⟩ ] ∼ )
48 5 6 28 29 30 qusmulrng ⊢ ( ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) ∧ ( ⟨ 1 , 𝑦 ⟩ ∈ ( ℤ × ℤ ) ∧ ⟨ 1 , 1 ⟩ ∈ ( ℤ × ℤ ) ) ) → ( [ ⟨ 1 , 𝑦 ⟩ ] ∼ ( .r ‘ 𝑄 ) [ ⟨ 1 , 1 ⟩ ] ∼ ) = [ ( ⟨ 1 , 𝑦 ⟩ ( .r ‘ 𝑅 ) ⟨ 1 , 1 ⟩ ) ] ∼ )
49 18 20 22 26 24 48 syl32anc ⊢ ( 𝑦 ∈ ℤ → ( [ ⟨ 1 , 𝑦 ⟩ ] ∼ ( .r ‘ 𝑄 ) [ ⟨ 1 , 1 ⟩ ] ∼ ) = [ ( ⟨ 1 , 𝑦 ⟩ ( .r ‘ 𝑅 ) ⟨ 1 , 1 ⟩ ) ] ∼ )
50 25 23 zmulcld ⊢ ( 𝑦 ∈ ℤ → ( 𝑦 · 1 ) ∈ ℤ )
51 1 33 33 35 35 23 25 23 23 36 50 38 38 29 xpsmul ⊢ ( 𝑦 ∈ ℤ → ( ⟨ 1 , 𝑦 ⟩ ( .r ‘ 𝑅 ) ⟨ 1 , 1 ⟩ ) = ⟨ ( 1 · 1 ) , ( 𝑦 · 1 ) ⟩ )
52 42 mulridd ⊢ ( 𝑦 ∈ ℤ → ( 𝑦 · 1 ) = 𝑦 )
53 41 52 opeq12d ⊢ ( 𝑦 ∈ ℤ → ⟨ ( 1 · 1 ) , ( 𝑦 · 1 ) ⟩ = ⟨ 1 , 𝑦 ⟩ )
54 51 53 eqtrd ⊢ ( 𝑦 ∈ ℤ → ( ⟨ 1 , 𝑦 ⟩ ( .r ‘ 𝑅 ) ⟨ 1 , 1 ⟩ ) = ⟨ 1 , 𝑦 ⟩ )
55 54 eceq1d ⊢ ( 𝑦 ∈ ℤ → [ ( ⟨ 1 , 𝑦 ⟩ ( .r ‘ 𝑅 ) ⟨ 1 , 1 ⟩ ) ] ∼ = [ ⟨ 1 , 𝑦 ⟩ ] ∼ )
56 49 55 eqtrd ⊢ ( 𝑦 ∈ ℤ → ( [ ⟨ 1 , 𝑦 ⟩ ] ∼ ( .r ‘ 𝑄 ) [ ⟨ 1 , 1 ⟩ ] ∼ ) = [ ⟨ 1 , 𝑦 ⟩ ] ∼ )
57 47 56 jca ⊢ ( 𝑦 ∈ ℤ → ( ( [ ⟨ 1 , 1 ⟩ ] ∼ ( .r ‘ 𝑄 ) [ ⟨ 1 , 𝑦 ⟩ ] ∼ ) = [ ⟨ 1 , 𝑦 ⟩ ] ∼ ∧ ( [ ⟨ 1 , 𝑦 ⟩ ] ∼ ( .r ‘ 𝑄 ) [ ⟨ 1 , 1 ⟩ ] ∼ ) = [ ⟨ 1 , 𝑦 ⟩ ] ∼ ) )
58 1 2 3 4 5 pzriprnglem10 ⊢ ( ( 1 ∈ ℤ ∧ 1 ∈ ℤ ) → [ ⟨ 1 , 1 ⟩ ] ∼ = ( ℤ × { 1 } ) )
59 12 12 58 mp2an ⊢ [ ⟨ 1 , 1 ⟩ ] ∼ = ( ℤ × { 1 } )
60 59 eqcomi ⊢ ( ℤ × { 1 } ) = [ ⟨ 1 , 1 ⟩ ] ∼
61 60 a1i ⊢ ( 𝑋 = [ ⟨ 1 , 𝑦 ⟩ ] ∼ → ( ℤ × { 1 } ) = [ ⟨ 1 , 1 ⟩ ] ∼ )
62 id ⊢ ( 𝑋 = [ ⟨ 1 , 𝑦 ⟩ ] ∼ → 𝑋 = [ ⟨ 1 , 𝑦 ⟩ ] ∼ )
63 61 62 oveq12d ⊢ ( 𝑋 = [ ⟨ 1 , 𝑦 ⟩ ] ∼ → ( ( ℤ × { 1 } ) ( .r ‘ 𝑄 ) 𝑋 ) = ( [ ⟨ 1 , 1 ⟩ ] ∼ ( .r ‘ 𝑄 ) [ ⟨ 1 , 𝑦 ⟩ ] ∼ ) )
64 63 62 eqeq12d ⊢ ( 𝑋 = [ ⟨ 1 , 𝑦 ⟩ ] ∼ → ( ( ( ℤ × { 1 } ) ( .r ‘ 𝑄 ) 𝑋 ) = 𝑋 ↔ ( [ ⟨ 1 , 1 ⟩ ] ∼ ( .r ‘ 𝑄 ) [ ⟨ 1 , 𝑦 ⟩ ] ∼ ) = [ ⟨ 1 , 𝑦 ⟩ ] ∼ ) )
65 62 61 oveq12d ⊢ ( 𝑋 = [ ⟨ 1 , 𝑦 ⟩ ] ∼ → ( 𝑋 ( .r ‘ 𝑄 ) ( ℤ × { 1 } ) ) = ( [ ⟨ 1 , 𝑦 ⟩ ] ∼ ( .r ‘ 𝑄 ) [ ⟨ 1 , 1 ⟩ ] ∼ ) )
66 65 62 eqeq12d ⊢ ( 𝑋 = [ ⟨ 1 , 𝑦 ⟩ ] ∼ → ( ( 𝑋 ( .r ‘ 𝑄 ) ( ℤ × { 1 } ) ) = 𝑋 ↔ ( [ ⟨ 1 , 𝑦 ⟩ ] ∼ ( .r ‘ 𝑄 ) [ ⟨ 1 , 1 ⟩ ] ∼ ) = [ ⟨ 1 , 𝑦 ⟩ ] ∼ ) )
67 64 66 anbi12d ⊢ ( 𝑋 = [ ⟨ 1 , 𝑦 ⟩ ] ∼ → ( ( ( ( ℤ × { 1 } ) ( .r ‘ 𝑄 ) 𝑋 ) = 𝑋 ∧ ( 𝑋 ( .r ‘ 𝑄 ) ( ℤ × { 1 } ) ) = 𝑋 ) ↔ ( ( [ ⟨ 1 , 1 ⟩ ] ∼ ( .r ‘ 𝑄 ) [ ⟨ 1 , 𝑦 ⟩ ] ∼ ) = [ ⟨ 1 , 𝑦 ⟩ ] ∼ ∧ ( [ ⟨ 1 , 𝑦 ⟩ ] ∼ ( .r ‘ 𝑄 ) [ ⟨ 1 , 1 ⟩ ] ∼ ) = [ ⟨ 1 , 𝑦 ⟩ ] ∼ ) ) )
68 57 67 syl5ibrcom ⊢ ( 𝑦 ∈ ℤ → ( 𝑋 = [ ⟨ 1 , 𝑦 ⟩ ] ∼ → ( ( ( ℤ × { 1 } ) ( .r ‘ 𝑄 ) 𝑋 ) = 𝑋 ∧ ( 𝑋 ( .r ‘ 𝑄 ) ( ℤ × { 1 } ) ) = 𝑋 ) ) )
69 16 68 sylbid ⊢ ( 𝑦 ∈ ℤ → ( 𝑋 = ( ℤ × { 𝑦 } ) → ( ( ( ℤ × { 1 } ) ( .r ‘ 𝑄 ) 𝑋 ) = 𝑋 ∧ ( 𝑋 ( .r ‘ 𝑄 ) ( ℤ × { 1 } ) ) = 𝑋 ) ) )
70 11 69 syl5 ⊢ ( 𝑦 ∈ ℤ → ( 𝑋 ∈ { ( ℤ × { 𝑦 } ) } → ( ( ( ℤ × { 1 } ) ( .r ‘ 𝑄 ) 𝑋 ) = 𝑋 ∧ ( 𝑋 ( .r ‘ 𝑄 ) ( ℤ × { 1 } ) ) = 𝑋 ) ) )
71 70 rexlimiv ⊢ ( ∃ 𝑦 ∈ ℤ 𝑋 ∈ { ( ℤ × { 𝑦 } ) } → ( ( ( ℤ × { 1 } ) ( .r ‘ 𝑄 ) 𝑋 ) = 𝑋 ∧ ( 𝑋 ( .r ‘ 𝑄 ) ( ℤ × { 1 } ) ) = 𝑋 ) )
72 10 71 sylbi ⊢ ( 𝑋 ∈ ( Base ‘ 𝑄 ) → ( ( ( ℤ × { 1 } ) ( .r ‘ 𝑄 ) 𝑋 ) = 𝑋 ∧ ( 𝑋 ( .r ‘ 𝑄 ) ( ℤ × { 1 } ) ) = 𝑋 ) )