pzriprnglem4

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

	Ref	Expression
Hypotheses	pzriprng.r	$⊢ R = ℤ_{ring} \times_{𝑠} ℤ_{ring}$
	pzriprng.i	$⊢ I = ℤ \times \{0\}$
Assertion	pzriprnglem4	$⊢ I \in SubGrp (R)$

Proof

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

Metamath Proof Explorer

Theorem pzriprnglem4

Proof