Metamath Proof Explorer

Theorem pzriprnglem4

Description: Lemma 4 for pzriprng : I is a subgroup of R . (Contributed by AV, 18-Mar-2025)

Ref Expression
Hypotheses pzriprng.r ⊢ 𝑅 = ( ℤring ×s ℤring )
pzriprng.i ⊢ 𝐼 = ( ℤ × { 0 } )
Assertion pzriprnglem4 𝐼 ∈ ( SubGrp ‘ 𝑅 )

Proof

Step Hyp Ref Expression
1 pzriprng.r ⊢ 𝑅 = ( ℤring ×s ℤring )
2 pzriprng.i ⊢ 𝐼 = ( ℤ × { 0 } )
3 0z ⊢ 0 ∈ ℤ
4 c0ex ⊢ 0 ∈ V
5 4 snss ⊢ ( 0 ∈ ℤ ↔ { 0 } ⊆ ℤ )
6 3 5 mpbi ⊢ { 0 } ⊆ ℤ
7 xpss2 ⊢ ( { 0 } ⊆ ℤ → ( ℤ × { 0 } ) ⊆ ( ℤ × ℤ ) )
8 6 7 ax-mp ⊢ ( ℤ × { 0 } ) ⊆ ( ℤ × ℤ )
9 1 pzriprnglem2 ⊢ ( Base ‘ 𝑅 ) = ( ℤ × ℤ )
10 8 2 9 3sstr4i ⊢ 𝐼 ⊆ ( Base ‘ 𝑅 )
11 3 ne0ii ⊢ ℤ ≠ ∅
12 4 snnz ⊢ { 0 } ≠ ∅
13 11 12 pm3.2i ⊢ ( ℤ ≠ ∅ ∧ { 0 } ≠ ∅ )
14 xpnz ⊢ ( ( ℤ ≠ ∅ ∧ { 0 } ≠ ∅ ) ↔ ( ℤ × { 0 } ) ≠ ∅ )
15 13 14 mpbi ⊢ ( ℤ × { 0 } ) ≠ ∅
16 2 15 eqnetri ⊢ 𝐼 ≠ ∅
17 1 2 pzriprnglem3 ⊢ ( 𝑥 ∈ 𝐼 ↔ ∃ 𝑎 ∈ ℤ 𝑥 = ⟨ 𝑎 , 0 ⟩ )
18 1 2 pzriprnglem3 ⊢ ( 𝑦 ∈ 𝐼 ↔ ∃ 𝑏 ∈ ℤ 𝑦 = ⟨ 𝑏 , 0 ⟩ )
19 simpr ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑥 = ⟨ 𝑎 , 0 ⟩ ) → 𝑥 = ⟨ 𝑎 , 0 ⟩ )
20 19 adantr ⊢ ( ( ( 𝑎 ∈ ℤ ∧ 𝑥 = ⟨ 𝑎 , 0 ⟩ ) ∧ 𝑏 ∈ ℤ ) → 𝑥 = ⟨ 𝑎 , 0 ⟩ )
21 id ⊢ ( 𝑦 = ⟨ 𝑏 , 0 ⟩ → 𝑦 = ⟨ 𝑏 , 0 ⟩ )
22 20 21 oveqan12d ⊢ ( ( ( ( 𝑎 ∈ ℤ ∧ 𝑥 = ⟨ 𝑎 , 0 ⟩ ) ∧ 𝑏 ∈ ℤ ) ∧ 𝑦 = ⟨ 𝑏 , 0 ⟩ ) → ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) = ( ⟨ 𝑎 , 0 ⟩ ( +g ‘ 𝑅 ) ⟨ 𝑏 , 0 ⟩ ) )
23 zringbas ⊢ ℤ = ( Base ‘ ℤring )
24 zringring ⊢ ℤring ∈ Ring
25 24 a1i ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ℤring ∈ Ring )
26 simpl ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → 𝑎 ∈ ℤ )
27 3 a1i ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → 0 ∈ ℤ )
28 simpr ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → 𝑏 ∈ ℤ )
29 zaddcl ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( 𝑎 + 𝑏 ) ∈ ℤ )
30 00id ⊢ ( 0 + 0 ) = 0
31 30 3 eqeltri ⊢ ( 0 + 0 ) ∈ ℤ
32 31 a1i ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( 0 + 0 ) ∈ ℤ )
33 zringplusg ⊢ + = ( +g ‘ ℤring )
34 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
35 1 23 23 25 25 26 27 28 27 29 32 33 33 34 xpsadd ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( ⟨ 𝑎 , 0 ⟩ ( +g ‘ 𝑅 ) ⟨ 𝑏 , 0 ⟩ ) = ⟨ ( 𝑎 + 𝑏 ) , ( 0 + 0 ) ⟩ )
36 4 snid ⊢ 0 ∈ { 0 }
37 30 36 eqeltri ⊢ ( 0 + 0 ) ∈ { 0 }
38 2 eleq2i ⊢ ( ⟨ ( 𝑎 + 𝑏 ) , ( 0 + 0 ) ⟩ ∈ 𝐼 ↔ ⟨ ( 𝑎 + 𝑏 ) , ( 0 + 0 ) ⟩ ∈ ( ℤ × { 0 } ) )
39 opelxp ⊢ ( ⟨ ( 𝑎 + 𝑏 ) , ( 0 + 0 ) ⟩ ∈ ( ℤ × { 0 } ) ↔ ( ( 𝑎 + 𝑏 ) ∈ ℤ ∧ ( 0 + 0 ) ∈ { 0 } ) )
40 38 39 bitri ⊢ ( ⟨ ( 𝑎 + 𝑏 ) , ( 0 + 0 ) ⟩ ∈ 𝐼 ↔ ( ( 𝑎 + 𝑏 ) ∈ ℤ ∧ ( 0 + 0 ) ∈ { 0 } ) )
41 29 37 40 sylanblrc ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ⟨ ( 𝑎 + 𝑏 ) , ( 0 + 0 ) ⟩ ∈ 𝐼 )
42 35 41 eqeltrd ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( ⟨ 𝑎 , 0 ⟩ ( +g ‘ 𝑅 ) ⟨ 𝑏 , 0 ⟩ ) ∈ 𝐼 )
43 42 ad4ant13 ⊢ ( ( ( ( 𝑎 ∈ ℤ ∧ 𝑥 = ⟨ 𝑎 , 0 ⟩ ) ∧ 𝑏 ∈ ℤ ) ∧ 𝑦 = ⟨ 𝑏 , 0 ⟩ ) → ( ⟨ 𝑎 , 0 ⟩ ( +g ‘ 𝑅 ) ⟨ 𝑏 , 0 ⟩ ) ∈ 𝐼 )
44 22 43 eqeltrd ⊢ ( ( ( ( 𝑎 ∈ ℤ ∧ 𝑥 = ⟨ 𝑎 , 0 ⟩ ) ∧ 𝑏 ∈ ℤ ) ∧ 𝑦 = ⟨ 𝑏 , 0 ⟩ ) → ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 )
45 44 rexlimdva2 ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑥 = ⟨ 𝑎 , 0 ⟩ ) → ( ∃ 𝑏 ∈ ℤ 𝑦 = ⟨ 𝑏 , 0 ⟩ → ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 ) )
46 18 45 biimtrid ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑥 = ⟨ 𝑎 , 0 ⟩ ) → ( 𝑦 ∈ 𝐼 → ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 ) )
47 46 ralrimiv ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑥 = ⟨ 𝑎 , 0 ⟩ ) → ∀ 𝑦 ∈ 𝐼 ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 )
48 zringgrp ⊢ ℤring ∈ Grp
49 48 a1i ⊢ ( 𝑎 ∈ ℤ → ℤring ∈ Grp )
50 id ⊢ ( 𝑎 ∈ ℤ → 𝑎 ∈ ℤ )
51 3 a1i ⊢ ( 𝑎 ∈ ℤ → 0 ∈ ℤ )
52 eqid ⊢ ( invg ‘ ℤring ) = ( invg ‘ ℤring )
53 eqid ⊢ ( invg ‘ 𝑅 ) = ( invg ‘ 𝑅 )
54 1 23 23 49 49 50 51 52 52 53 xpsinv ⊢ ( 𝑎 ∈ ℤ → ( ( invg ‘ 𝑅 ) ‘ ⟨ 𝑎 , 0 ⟩ ) = ⟨ ( ( invg ‘ ℤring ) ‘ 𝑎 ) , ( ( invg ‘ ℤring ) ‘ 0 ) ⟩ )
55 zringinvg ⊢ ( 𝑎 ∈ ℤ → - 𝑎 = ( ( invg ‘ ℤring ) ‘ 𝑎 ) )
56 znegcl ⊢ ( 𝑎 ∈ ℤ → - 𝑎 ∈ ℤ )
57 55 56 eqeltrrd ⊢ ( 𝑎 ∈ ℤ → ( ( invg ‘ ℤring ) ‘ 𝑎 ) ∈ ℤ )
58 neg0 ⊢ - 0 = 0
59 58 36 eqeltri ⊢ - 0 ∈ { 0 }
60 zringinvg ⊢ ( 0 ∈ ℤ → - 0 = ( ( invg ‘ ℤring ) ‘ 0 ) )
61 60 eleq1d ⊢ ( 0 ∈ ℤ → ( - 0 ∈ { 0 } ↔ ( ( invg ‘ ℤring ) ‘ 0 ) ∈ { 0 } ) )
62 3 61 mp1i ⊢ ( 𝑎 ∈ ℤ → ( - 0 ∈ { 0 } ↔ ( ( invg ‘ ℤring ) ‘ 0 ) ∈ { 0 } ) )
63 59 62 mpbii ⊢ ( 𝑎 ∈ ℤ → ( ( invg ‘ ℤring ) ‘ 0 ) ∈ { 0 } )
64 57 63 opelxpd ⊢ ( 𝑎 ∈ ℤ → ⟨ ( ( invg ‘ ℤring ) ‘ 𝑎 ) , ( ( invg ‘ ℤring ) ‘ 0 ) ⟩ ∈ ( ℤ × { 0 } ) )
65 54 64 eqeltrd ⊢ ( 𝑎 ∈ ℤ → ( ( invg ‘ 𝑅 ) ‘ ⟨ 𝑎 , 0 ⟩ ) ∈ ( ℤ × { 0 } ) )
66 65 adantr ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑥 = ⟨ 𝑎 , 0 ⟩ ) → ( ( invg ‘ 𝑅 ) ‘ ⟨ 𝑎 , 0 ⟩ ) ∈ ( ℤ × { 0 } ) )
67 fveq2 ⊢ ( 𝑥 = ⟨ 𝑎 , 0 ⟩ → ( ( invg ‘ 𝑅 ) ‘ 𝑥 ) = ( ( invg ‘ 𝑅 ) ‘ ⟨ 𝑎 , 0 ⟩ ) )
68 67 adantl ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑥 = ⟨ 𝑎 , 0 ⟩ ) → ( ( invg ‘ 𝑅 ) ‘ 𝑥 ) = ( ( invg ‘ 𝑅 ) ‘ ⟨ 𝑎 , 0 ⟩ ) )
69 2 a1i ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑥 = ⟨ 𝑎 , 0 ⟩ ) → 𝐼 = ( ℤ × { 0 } ) )
70 66 68 69 3eltr4d ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑥 = ⟨ 𝑎 , 0 ⟩ ) → ( ( invg ‘ 𝑅 ) ‘ 𝑥 ) ∈ 𝐼 )
71 47 70 jca ⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑥 = ⟨ 𝑎 , 0 ⟩ ) → ( ∀ 𝑦 ∈ 𝐼 ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 ∧ ( ( invg ‘ 𝑅 ) ‘ 𝑥 ) ∈ 𝐼 ) )
72 71 rexlimiva ⊢ ( ∃ 𝑎 ∈ ℤ 𝑥 = ⟨ 𝑎 , 0 ⟩ → ( ∀ 𝑦 ∈ 𝐼 ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 ∧ ( ( invg ‘ 𝑅 ) ‘ 𝑥 ) ∈ 𝐼 ) )
73 17 72 sylbi ⊢ ( 𝑥 ∈ 𝐼 → ( ∀ 𝑦 ∈ 𝐼 ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 ∧ ( ( invg ‘ 𝑅 ) ‘ 𝑥 ) ∈ 𝐼 ) )
74 73 rgen ⊢ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ 𝐼 ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 ∧ ( ( invg ‘ 𝑅 ) ‘ 𝑥 ) ∈ 𝐼 )
75 1 pzriprnglem1 ⊢ 𝑅 ∈ Rng
76 rnggrp ⊢ ( 𝑅 ∈ Rng → 𝑅 ∈ Grp )
77 75 76 ax-mp ⊢ 𝑅 ∈ Grp
78 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
79 78 34 53 issubg2 ⊢ ( 𝑅 ∈ Grp → ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ↔ ( 𝐼 ⊆ ( Base ‘ 𝑅 ) ∧ 𝐼 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ 𝐼 ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 ∧ ( ( invg ‘ 𝑅 ) ‘ 𝑥 ) ∈ 𝐼 ) ) ) )
80 77 79 ax-mp ⊢ ( 𝐼 ∈ ( SubGrp ‘ 𝑅 ) ↔ ( 𝐼 ⊆ ( Base ‘ 𝑅 ) ∧ 𝐼 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝐼 ( ∀ 𝑦 ∈ 𝐼 ( 𝑥 ( +g ‘ 𝑅 ) 𝑦 ) ∈ 𝐼 ∧ ( ( invg ‘ 𝑅 ) ‘ 𝑥 ) ∈ 𝐼 ) ) )
81 10 16 74 80 mpbir3an ⊢ 𝐼 ∈ ( SubGrp ‘ 𝑅 )