Metamath Proof Explorer

Theorem pzriprnglem8

Description: Lemma 8 for pzriprng : I resp. J is a two-sided ideal of the non-unital ring R . (Contributed by AV, 21-Mar-2025)

Ref Expression
Hypotheses pzriprng.r ⊢ 𝑅 = ( ℤring ×s ℤring )
pzriprng.i ⊢ 𝐼 = ( ℤ × { 0 } )
pzriprng.j ⊢ 𝐽 = ( 𝑅 ↾s 𝐼 )
Assertion pzriprnglem8 𝐼 ∈ ( 2Ideal ‘ 𝑅 )

Proof

Step Hyp Ref Expression
1 pzriprng.r ⊢ 𝑅 = ( ℤring ×s ℤring )
2 pzriprng.i ⊢ 𝐼 = ( ℤ × { 0 } )
3 pzriprng.j ⊢ 𝐽 = ( 𝑅 ↾s 𝐼 )
4 1 pzriprnglem2 ⊢ ( Base ‘ 𝑅 ) = ( ℤ × ℤ )
5 4 eleq2i ⊢ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↔ 𝑥 ∈ ( ℤ × ℤ ) )
6 elxp2 ⊢ ( 𝑥 ∈ ( ℤ × ℤ ) ↔ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ )
7 5 6 bitri ⊢ ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↔ ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ )
8 1 2 pzriprnglem3 ⊢ ( 𝑦 ∈ 𝐼 ↔ ∃ 𝑐 ∈ ℤ 𝑦 = ⟨ 𝑐 , 0 ⟩ )
9 simpll ⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ 𝑐 ∈ ℤ ) → 𝑎 ∈ ℤ )
10 simpr ⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ 𝑐 ∈ ℤ ) → 𝑐 ∈ ℤ )
11 9 10 zmulcld ⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ 𝑐 ∈ ℤ ) → ( 𝑎 · 𝑐 ) ∈ ℤ )
12 zcn ⊢ ( 𝑏 ∈ ℤ → 𝑏 ∈ ℂ )
13 12 adantl ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → 𝑏 ∈ ℂ )
14 13 adantr ⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ 𝑐 ∈ ℤ ) → 𝑏 ∈ ℂ )
15 14 mul01d ⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ 𝑐 ∈ ℤ ) → ( 𝑏 · 0 ) = 0 )
16 ovex ⊢ ( 𝑏 · 0 ) ∈ V
17 16 elsn ⊢ ( ( 𝑏 · 0 ) ∈ { 0 } ↔ ( 𝑏 · 0 ) = 0 )
18 15 17 sylibr ⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ 𝑐 ∈ ℤ ) → ( 𝑏 · 0 ) ∈ { 0 } )
19 11 18 opelxpd ⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ 𝑐 ∈ ℤ ) → ⟨ ( 𝑎 · 𝑐 ) , ( 𝑏 · 0 ) ⟩ ∈ ( ℤ × { 0 } ) )
20 10 9 zmulcld ⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ 𝑐 ∈ ℤ ) → ( 𝑐 · 𝑎 ) ∈ ℤ )
21 14 mul02d ⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ 𝑐 ∈ ℤ ) → ( 0 · 𝑏 ) = 0 )
22 ovex ⊢ ( 0 · 𝑏 ) ∈ V
23 22 elsn ⊢ ( ( 0 · 𝑏 ) ∈ { 0 } ↔ ( 0 · 𝑏 ) = 0 )
24 21 23 sylibr ⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ 𝑐 ∈ ℤ ) → ( 0 · 𝑏 ) ∈ { 0 } )
25 20 24 opelxpd ⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ 𝑐 ∈ ℤ ) → ⟨ ( 𝑐 · 𝑎 ) , ( 0 · 𝑏 ) ⟩ ∈ ( ℤ × { 0 } ) )
26 zringbas ⊢ ℤ = ( Base ‘ ℤring )
27 zringring ⊢ ℤring ∈ Ring
28 27 a1i ⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ 𝑐 ∈ ℤ ) → ℤring ∈ Ring )
29 simplr ⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ 𝑐 ∈ ℤ ) → 𝑏 ∈ ℤ )
30 0zd ⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ 𝑐 ∈ ℤ ) → 0 ∈ ℤ )
31 29 30 zmulcld ⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ 𝑐 ∈ ℤ ) → ( 𝑏 · 0 ) ∈ ℤ )
32 zringmulr ⊢ · = ( .r ‘ ℤring )
33 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
34 1 26 26 28 28 9 29 10 30 11 31 32 32 33 xpsmul ⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ 𝑐 ∈ ℤ ) → ( ⟨ 𝑎 , 𝑏 ⟩ ( .r ‘ 𝑅 ) ⟨ 𝑐 , 0 ⟩ ) = ⟨ ( 𝑎 · 𝑐 ) , ( 𝑏 · 0 ) ⟩ )
35 34 eleq1d ⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ 𝑐 ∈ ℤ ) → ( ( ⟨ 𝑎 , 𝑏 ⟩ ( .r ‘ 𝑅 ) ⟨ 𝑐 , 0 ⟩ ) ∈ ( ℤ × { 0 } ) ↔ ⟨ ( 𝑎 · 𝑐 ) , ( 𝑏 · 0 ) ⟩ ∈ ( ℤ × { 0 } ) ) )
36 simpl ⊢ ( ( 𝑐 ∈ ℤ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑐 ∈ ℤ )
37 simprl ⊢ ( ( 𝑐 ∈ ℤ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑎 ∈ ℤ )
38 36 37 zmulcld ⊢ ( ( 𝑐 ∈ ℤ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 𝑐 · 𝑎 ) ∈ ℤ )
39 38 ancoms ⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ 𝑐 ∈ ℤ ) → ( 𝑐 · 𝑎 ) ∈ ℤ )
40 0zd ⊢ ( ( 𝑐 ∈ ℤ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 0 ∈ ℤ )
41 simprr ⊢ ( ( 𝑐 ∈ ℤ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → 𝑏 ∈ ℤ )
42 40 41 zmulcld ⊢ ( ( 𝑐 ∈ ℤ ∧ ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ) → ( 0 · 𝑏 ) ∈ ℤ )
43 42 ancoms ⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ 𝑐 ∈ ℤ ) → ( 0 · 𝑏 ) ∈ ℤ )
44 1 26 26 28 28 10 30 9 29 39 43 32 32 33 xpsmul ⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ 𝑐 ∈ ℤ ) → ( ⟨ 𝑐 , 0 ⟩ ( .r ‘ 𝑅 ) ⟨ 𝑎 , 𝑏 ⟩ ) = ⟨ ( 𝑐 · 𝑎 ) , ( 0 · 𝑏 ) ⟩ )
45 44 eleq1d ⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ 𝑐 ∈ ℤ ) → ( ( ⟨ 𝑐 , 0 ⟩ ( .r ‘ 𝑅 ) ⟨ 𝑎 , 𝑏 ⟩ ) ∈ ( ℤ × { 0 } ) ↔ ⟨ ( 𝑐 · 𝑎 ) , ( 0 · 𝑏 ) ⟩ ∈ ( ℤ × { 0 } ) ) )
46 35 45 anbi12d ⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ 𝑐 ∈ ℤ ) → ( ( ( ⟨ 𝑎 , 𝑏 ⟩ ( .r ‘ 𝑅 ) ⟨ 𝑐 , 0 ⟩ ) ∈ ( ℤ × { 0 } ) ∧ ( ⟨ 𝑐 , 0 ⟩ ( .r ‘ 𝑅 ) ⟨ 𝑎 , 𝑏 ⟩ ) ∈ ( ℤ × { 0 } ) ) ↔ ( ⟨ ( 𝑎 · 𝑐 ) , ( 𝑏 · 0 ) ⟩ ∈ ( ℤ × { 0 } ) ∧ ⟨ ( 𝑐 · 𝑎 ) , ( 0 · 𝑏 ) ⟩ ∈ ( ℤ × { 0 } ) ) ) )
47 19 25 46 mpbir2and ⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ 𝑐 ∈ ℤ ) → ( ( ⟨ 𝑎 , 𝑏 ⟩ ( .r ‘ 𝑅 ) ⟨ 𝑐 , 0 ⟩ ) ∈ ( ℤ × { 0 } ) ∧ ( ⟨ 𝑐 , 0 ⟩ ( .r ‘ 𝑅 ) ⟨ 𝑎 , 𝑏 ⟩ ) ∈ ( ℤ × { 0 } ) ) )
48 47 adantr ⊢ ( ( ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ 𝑐 ∈ ℤ ) ∧ ( 𝑦 = ⟨ 𝑐 , 0 ⟩ ∧ 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ) ) → ( ( ⟨ 𝑎 , 𝑏 ⟩ ( .r ‘ 𝑅 ) ⟨ 𝑐 , 0 ⟩ ) ∈ ( ℤ × { 0 } ) ∧ ( ⟨ 𝑐 , 0 ⟩ ( .r ‘ 𝑅 ) ⟨ 𝑎 , 𝑏 ⟩ ) ∈ ( ℤ × { 0 } ) ) )
49 oveq12 ⊢ ( ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ 𝑦 = ⟨ 𝑐 , 0 ⟩ ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = ( ⟨ 𝑎 , 𝑏 ⟩ ( .r ‘ 𝑅 ) ⟨ 𝑐 , 0 ⟩ ) )
50 49 ancoms ⊢ ( ( 𝑦 = ⟨ 𝑐 , 0 ⟩ ∧ 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = ( ⟨ 𝑎 , 𝑏 ⟩ ( .r ‘ 𝑅 ) ⟨ 𝑐 , 0 ⟩ ) )
51 50 adantl ⊢ ( ( ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ 𝑐 ∈ ℤ ) ∧ ( 𝑦 = ⟨ 𝑐 , 0 ⟩ ∧ 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ) ) → ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) = ( ⟨ 𝑎 , 𝑏 ⟩ ( .r ‘ 𝑅 ) ⟨ 𝑐 , 0 ⟩ ) )
52 2 a1i ⊢ ( ( ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ 𝑐 ∈ ℤ ) ∧ ( 𝑦 = ⟨ 𝑐 , 0 ⟩ ∧ 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ) ) → 𝐼 = ( ℤ × { 0 } ) )
53 51 52 eleq12d ⊢ ( ( ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ 𝑐 ∈ ℤ ) ∧ ( 𝑦 = ⟨ 𝑐 , 0 ⟩ ∧ 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 ↔ ( ⟨ 𝑎 , 𝑏 ⟩ ( .r ‘ 𝑅 ) ⟨ 𝑐 , 0 ⟩ ) ∈ ( ℤ × { 0 } ) ) )
54 oveq12 ⊢ ( ( 𝑦 = ⟨ 𝑐 , 0 ⟩ ∧ 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ) → ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( ⟨ 𝑐 , 0 ⟩ ( .r ‘ 𝑅 ) ⟨ 𝑎 , 𝑏 ⟩ ) )
55 54 adantl ⊢ ( ( ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ 𝑐 ∈ ℤ ) ∧ ( 𝑦 = ⟨ 𝑐 , 0 ⟩ ∧ 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ) ) → ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) = ( ⟨ 𝑐 , 0 ⟩ ( .r ‘ 𝑅 ) ⟨ 𝑎 , 𝑏 ⟩ ) )
56 55 52 eleq12d ⊢ ( ( ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ 𝑐 ∈ ℤ ) ∧ ( 𝑦 = ⟨ 𝑐 , 0 ⟩ ∧ 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ) ) → ( ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ∈ 𝐼 ↔ ( ⟨ 𝑐 , 0 ⟩ ( .r ‘ 𝑅 ) ⟨ 𝑎 , 𝑏 ⟩ ) ∈ ( ℤ × { 0 } ) ) )
57 53 56 anbi12d ⊢ ( ( ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ 𝑐 ∈ ℤ ) ∧ ( 𝑦 = ⟨ 𝑐 , 0 ⟩ ∧ 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ) ) → ( ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ∈ 𝐼 ) ↔ ( ( ⟨ 𝑎 , 𝑏 ⟩ ( .r ‘ 𝑅 ) ⟨ 𝑐 , 0 ⟩ ) ∈ ( ℤ × { 0 } ) ∧ ( ⟨ 𝑐 , 0 ⟩ ( .r ‘ 𝑅 ) ⟨ 𝑎 , 𝑏 ⟩ ) ∈ ( ℤ × { 0 } ) ) ) )
58 48 57 mpbird ⊢ ( ( ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ 𝑐 ∈ ℤ ) ∧ ( 𝑦 = ⟨ 𝑐 , 0 ⟩ ∧ 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ) ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ∈ 𝐼 ) )
59 58 exp32 ⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) ∧ 𝑐 ∈ ℤ ) → ( 𝑦 = ⟨ 𝑐 , 0 ⟩ → ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ∈ 𝐼 ) ) ) )
60 59 rexlimdva ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( ∃ 𝑐 ∈ ℤ 𝑦 = ⟨ 𝑐 , 0 ⟩ → ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ∈ 𝐼 ) ) ) )
61 60 com23 ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → ( ∃ 𝑐 ∈ ℤ 𝑦 = ⟨ 𝑐 , 0 ⟩ → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ∈ 𝐼 ) ) ) )
62 61 rexlimivv ⊢ ( ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ → ( ∃ 𝑐 ∈ ℤ 𝑦 = ⟨ 𝑐 , 0 ⟩ → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ∈ 𝐼 ) ) )
63 62 imp ⊢ ( ( ∃ 𝑎 ∈ ℤ ∃ 𝑏 ∈ ℤ 𝑥 = ⟨ 𝑎 , 𝑏 ⟩ ∧ ∃ 𝑐 ∈ ℤ 𝑦 = ⟨ 𝑐 , 0 ⟩ ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ∈ 𝐼 ) )
64 7 8 63 syl2anb ⊢ ( ( 𝑥 ∈ ( Base ‘ 𝑅 ) ∧ 𝑦 ∈ 𝐼 ) → ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ∈ 𝐼 ) )
65 64 rgen2 ⊢ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ 𝐼 ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ∈ 𝐼 )
66 1 pzriprnglem1 ⊢ 𝑅 ∈ Rng
67 1 2 pzriprnglem4 ⊢ 𝐼 ∈ ( SubGrp ‘ 𝑅 )
68 eqid ⊢ ( 2Ideal ‘ 𝑅 ) = ( 2Ideal ‘ 𝑅 )
69 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
70 68 69 33 df2idl2rng ⊢ ( ( 𝑅 ∈ Rng ∧ 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ) → ( 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ 𝐼 ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ∈ 𝐼 ) ) )
71 66 67 70 mp2an ⊢ ( 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) ↔ ∀ 𝑥 ∈ ( Base ‘ 𝑅 ) ∀ 𝑦 ∈ 𝐼 ( ( 𝑥 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 ∧ ( 𝑦 ( .r ‘ 𝑅 ) 𝑥 ) ∈ 𝐼 ) )
72 65 71 mpbir ⊢ 𝐼 ∈ ( 2Ideal ‘ 𝑅 )