Metamath Proof Explorer

Theorem pzriprnglem6

Description: Lemma 6 for pzriprng : J has a ring unity. (Contributed by AV, 19-Mar-2025)

Ref Expression
Hypotheses pzriprng.r ⊢ 𝑅 = ( ℤring ×s ℤring )
pzriprng.i ⊢ 𝐼 = ( ℤ × { 0 } )
pzriprng.j ⊢ 𝐽 = ( 𝑅 ↾s 𝐼 )
Assertion pzriprnglem6 ( 𝑋 ∈ 𝐼 → ( ( ⟨ 1 , 0 ⟩ ( .r ‘ 𝐽 ) 𝑋 ) = 𝑋 ∧ ( 𝑋 ( .r ‘ 𝐽 ) ⟨ 1 , 0 ⟩ ) = 𝑋 ) )

Proof

Step Hyp Ref Expression
1 pzriprng.r ⊢ 𝑅 = ( ℤring ×s ℤring )
2 pzriprng.i ⊢ 𝐼 = ( ℤ × { 0 } )
3 pzriprng.j ⊢ 𝐽 = ( 𝑅 ↾s 𝐼 )
4 1 2 pzriprnglem3 ⊢ ( 𝑋 ∈ 𝐼 ↔ ∃ 𝑎 ∈ ℤ 𝑋 = ⟨ 𝑎 , 0 ⟩ )
5 1 2 pzriprnglem5 ⊢ 𝐼 ∈ ( SubRng ‘ 𝑅 )
6 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
7 3 6 ressmulr ⊢ ( 𝐼 ∈ ( SubRng ‘ 𝑅 ) → ( .r ‘ 𝑅 ) = ( .r ‘ 𝐽 ) )
8 7 eqcomd ⊢ ( 𝐼 ∈ ( SubRng ‘ 𝑅 ) → ( .r ‘ 𝐽 ) = ( .r ‘ 𝑅 ) )
9 5 8 ax-mp ⊢ ( .r ‘ 𝐽 ) = ( .r ‘ 𝑅 )
10 9 oveqi ⊢ ( ⟨ 1 , 0 ⟩ ( .r ‘ 𝐽 ) ⟨ 𝑎 , 0 ⟩ ) = ( ⟨ 1 , 0 ⟩ ( .r ‘ 𝑅 ) ⟨ 𝑎 , 0 ⟩ )
11 10 a1i ⊢ ( 𝑎 ∈ ℤ → ( ⟨ 1 , 0 ⟩ ( .r ‘ 𝐽 ) ⟨ 𝑎 , 0 ⟩ ) = ( ⟨ 1 , 0 ⟩ ( .r ‘ 𝑅 ) ⟨ 𝑎 , 0 ⟩ ) )
12 zringbas ⊢ ℤ = ( Base ‘ ℤring )
13 zringring ⊢ ℤring ∈ Ring
14 13 a1i ⊢ ( 𝑎 ∈ ℤ → ℤring ∈ Ring )
15 1zzd ⊢ ( 𝑎 ∈ ℤ → 1 ∈ ℤ )
16 0z ⊢ 0 ∈ ℤ
17 16 a1i ⊢ ( 𝑎 ∈ ℤ → 0 ∈ ℤ )
18 id ⊢ ( 𝑎 ∈ ℤ → 𝑎 ∈ ℤ )
19 zringmulr ⊢ · = ( .r ‘ ℤring )
20 19 oveqi ⊢ ( 1 · 𝑎 ) = ( 1 ( .r ‘ ℤring ) 𝑎 )
21 15 18 zmulcld ⊢ ( 𝑎 ∈ ℤ → ( 1 · 𝑎 ) ∈ ℤ )
22 20 21 eqeltrrid ⊢ ( 𝑎 ∈ ℤ → ( 1 ( .r ‘ ℤring ) 𝑎 ) ∈ ℤ )
23 19 eqcomi ⊢ ( .r ‘ ℤring ) = ·
24 23 oveqi ⊢ ( 0 ( .r ‘ ℤring ) 0 ) = ( 0 · 0 )
25 id ⊢ ( 0 ∈ ℤ → 0 ∈ ℤ )
26 25 25 zmulcld ⊢ ( 0 ∈ ℤ → ( 0 · 0 ) ∈ ℤ )
27 16 26 ax-mp ⊢ ( 0 · 0 ) ∈ ℤ
28 24 27 eqeltri ⊢ ( 0 ( .r ‘ ℤring ) 0 ) ∈ ℤ
29 28 a1i ⊢ ( 𝑎 ∈ ℤ → ( 0 ( .r ‘ ℤring ) 0 ) ∈ ℤ )
30 eqid ⊢ ( .r ‘ ℤring ) = ( .r ‘ ℤring )
31 1 12 12 14 14 15 17 18 17 22 29 30 30 6 xpsmul ⊢ ( 𝑎 ∈ ℤ → ( ⟨ 1 , 0 ⟩ ( .r ‘ 𝑅 ) ⟨ 𝑎 , 0 ⟩ ) = ⟨ ( 1 ( .r ‘ ℤring ) 𝑎 ) , ( 0 ( .r ‘ ℤring ) 0 ) ⟩ )
32 zcn ⊢ ( 𝑎 ∈ ℤ → 𝑎 ∈ ℂ )
33 32 mullidd ⊢ ( 𝑎 ∈ ℤ → ( 1 · 𝑎 ) = 𝑎 )
34 20 33 eqtr3id ⊢ ( 𝑎 ∈ ℤ → ( 1 ( .r ‘ ℤring ) 𝑎 ) = 𝑎 )
35 0cn ⊢ 0 ∈ ℂ
36 35 mul02i ⊢ ( 0 · 0 ) = 0
37 24 36 eqtri ⊢ ( 0 ( .r ‘ ℤring ) 0 ) = 0
38 37 a1i ⊢ ( 𝑎 ∈ ℤ → ( 0 ( .r ‘ ℤring ) 0 ) = 0 )
39 34 38 opeq12d ⊢ ( 𝑎 ∈ ℤ → ⟨ ( 1 ( .r ‘ ℤring ) 𝑎 ) , ( 0 ( .r ‘ ℤring ) 0 ) ⟩ = ⟨ 𝑎 , 0 ⟩ )
40 11 31 39 3eqtrd ⊢ ( 𝑎 ∈ ℤ → ( ⟨ 1 , 0 ⟩ ( .r ‘ 𝐽 ) ⟨ 𝑎 , 0 ⟩ ) = ⟨ 𝑎 , 0 ⟩ )
41 9 oveqi ⊢ ( ⟨ 𝑎 , 0 ⟩ ( .r ‘ 𝐽 ) ⟨ 1 , 0 ⟩ ) = ( ⟨ 𝑎 , 0 ⟩ ( .r ‘ 𝑅 ) ⟨ 1 , 0 ⟩ )
42 41 a1i ⊢ ( 𝑎 ∈ ℤ → ( ⟨ 𝑎 , 0 ⟩ ( .r ‘ 𝐽 ) ⟨ 1 , 0 ⟩ ) = ( ⟨ 𝑎 , 0 ⟩ ( .r ‘ 𝑅 ) ⟨ 1 , 0 ⟩ ) )
43 19 oveqi ⊢ ( 𝑎 · 1 ) = ( 𝑎 ( .r ‘ ℤring ) 1 )
44 18 15 zmulcld ⊢ ( 𝑎 ∈ ℤ → ( 𝑎 · 1 ) ∈ ℤ )
45 43 44 eqeltrrid ⊢ ( 𝑎 ∈ ℤ → ( 𝑎 ( .r ‘ ℤring ) 1 ) ∈ ℤ )
46 1 12 12 14 14 18 17 15 17 45 29 30 30 6 xpsmul ⊢ ( 𝑎 ∈ ℤ → ( ⟨ 𝑎 , 0 ⟩ ( .r ‘ 𝑅 ) ⟨ 1 , 0 ⟩ ) = ⟨ ( 𝑎 ( .r ‘ ℤring ) 1 ) , ( 0 ( .r ‘ ℤring ) 0 ) ⟩ )
47 23 oveqi ⊢ ( 𝑎 ( .r ‘ ℤring ) 1 ) = ( 𝑎 · 1 )
48 32 mulridd ⊢ ( 𝑎 ∈ ℤ → ( 𝑎 · 1 ) = 𝑎 )
49 47 48 eqtrid ⊢ ( 𝑎 ∈ ℤ → ( 𝑎 ( .r ‘ ℤring ) 1 ) = 𝑎 )
50 49 38 opeq12d ⊢ ( 𝑎 ∈ ℤ → ⟨ ( 𝑎 ( .r ‘ ℤring ) 1 ) , ( 0 ( .r ‘ ℤring ) 0 ) ⟩ = ⟨ 𝑎 , 0 ⟩ )
51 42 46 50 3eqtrd ⊢ ( 𝑎 ∈ ℤ → ( ⟨ 𝑎 , 0 ⟩ ( .r ‘ 𝐽 ) ⟨ 1 , 0 ⟩ ) = ⟨ 𝑎 , 0 ⟩ )
52 40 51 jca ⊢ ( 𝑎 ∈ ℤ → ( ( ⟨ 1 , 0 ⟩ ( .r ‘ 𝐽 ) ⟨ 𝑎 , 0 ⟩ ) = ⟨ 𝑎 , 0 ⟩ ∧ ( ⟨ 𝑎 , 0 ⟩ ( .r ‘ 𝐽 ) ⟨ 1 , 0 ⟩ ) = ⟨ 𝑎 , 0 ⟩ ) )
53 oveq2 ⊢ ( 𝑋 = ⟨ 𝑎 , 0 ⟩ → ( ⟨ 1 , 0 ⟩ ( .r ‘ 𝐽 ) 𝑋 ) = ( ⟨ 1 , 0 ⟩ ( .r ‘ 𝐽 ) ⟨ 𝑎 , 0 ⟩ ) )
54 id ⊢ ( 𝑋 = ⟨ 𝑎 , 0 ⟩ → 𝑋 = ⟨ 𝑎 , 0 ⟩ )
55 53 54 eqeq12d ⊢ ( 𝑋 = ⟨ 𝑎 , 0 ⟩ → ( ( ⟨ 1 , 0 ⟩ ( .r ‘ 𝐽 ) 𝑋 ) = 𝑋 ↔ ( ⟨ 1 , 0 ⟩ ( .r ‘ 𝐽 ) ⟨ 𝑎 , 0 ⟩ ) = ⟨ 𝑎 , 0 ⟩ ) )
56 oveq1 ⊢ ( 𝑋 = ⟨ 𝑎 , 0 ⟩ → ( 𝑋 ( .r ‘ 𝐽 ) ⟨ 1 , 0 ⟩ ) = ( ⟨ 𝑎 , 0 ⟩ ( .r ‘ 𝐽 ) ⟨ 1 , 0 ⟩ ) )
57 56 54 eqeq12d ⊢ ( 𝑋 = ⟨ 𝑎 , 0 ⟩ → ( ( 𝑋 ( .r ‘ 𝐽 ) ⟨ 1 , 0 ⟩ ) = 𝑋 ↔ ( ⟨ 𝑎 , 0 ⟩ ( .r ‘ 𝐽 ) ⟨ 1 , 0 ⟩ ) = ⟨ 𝑎 , 0 ⟩ ) )
58 55 57 anbi12d ⊢ ( 𝑋 = ⟨ 𝑎 , 0 ⟩ → ( ( ( ⟨ 1 , 0 ⟩ ( .r ‘ 𝐽 ) 𝑋 ) = 𝑋 ∧ ( 𝑋 ( .r ‘ 𝐽 ) ⟨ 1 , 0 ⟩ ) = 𝑋 ) ↔ ( ( ⟨ 1 , 0 ⟩ ( .r ‘ 𝐽 ) ⟨ 𝑎 , 0 ⟩ ) = ⟨ 𝑎 , 0 ⟩ ∧ ( ⟨ 𝑎 , 0 ⟩ ( .r ‘ 𝐽 ) ⟨ 1 , 0 ⟩ ) = ⟨ 𝑎 , 0 ⟩ ) ) )
59 52 58 syl5ibrcom ⊢ ( 𝑎 ∈ ℤ → ( 𝑋 = ⟨ 𝑎 , 0 ⟩ → ( ( ⟨ 1 , 0 ⟩ ( .r ‘ 𝐽 ) 𝑋 ) = 𝑋 ∧ ( 𝑋 ( .r ‘ 𝐽 ) ⟨ 1 , 0 ⟩ ) = 𝑋 ) ) )
60 59 rexlimiv ⊢ ( ∃ 𝑎 ∈ ℤ 𝑋 = ⟨ 𝑎 , 0 ⟩ → ( ( ⟨ 1 , 0 ⟩ ( .r ‘ 𝐽 ) 𝑋 ) = 𝑋 ∧ ( 𝑋 ( .r ‘ 𝐽 ) ⟨ 1 , 0 ⟩ ) = 𝑋 ) )
61 4 60 sylbi ⊢ ( 𝑋 ∈ 𝐼 → ( ( ⟨ 1 , 0 ⟩ ( .r ‘ 𝐽 ) 𝑋 ) = 𝑋 ∧ ( 𝑋 ( .r ‘ 𝐽 ) ⟨ 1 , 0 ⟩ ) = 𝑋 ) )