2zrngamgm

	Ref	Expression
Hypotheses	2zrng.e	$⊢ E = \{z \in ℤ \| \exists x \in ℤ z = 2 x\}$
	2zrngbas.r	$⊢ R = ℂ_{fld} ↾_{𝑠} E$
Assertion	2zrngamgm	$⊢ R \in Mgm$

Proof

Step	Hyp	Ref	Expression
1		2zrng.e	$⊢ E = \{z \in ℤ \| \exists x \in ℤ z = 2 x\}$
2		2zrngbas.r	$⊢ R = ℂ_{fld} ↾_{𝑠} E$
3		eqeq1	$⊢ z = a \to (z = 2 x \leftrightarrow a = 2 x)$
4	3	rexbidv	$⊢ z = a \to (\exists x \in ℤ z = 2 x \leftrightarrow \exists x \in ℤ a = 2 x)$
5	4 1	elrab2	$⊢ a \in E \leftrightarrow (a \in ℤ \land \exists x \in ℤ a = 2 x)$
6		eqeq1	$⊢ z = b \to (z = 2 x \leftrightarrow b = 2 x)$
7	6	rexbidv	$⊢ z = b \to (\exists x \in ℤ z = 2 x \leftrightarrow \exists x \in ℤ b = 2 x)$
8	7 1	elrab2	$⊢ b \in E \leftrightarrow (b \in ℤ \land \exists x \in ℤ b = 2 x)$
9		oveq2	$⊢ x = y \to 2 x = 2 y$
10	9	eqeq2d	$⊢ x = y \to (a = 2 x \leftrightarrow a = 2 y)$
11	10	cbvrexvw	$⊢ \exists x \in ℤ a = 2 x \leftrightarrow \exists y \in ℤ a = 2 y$
12		zaddcl	$⊢ (a \in ℤ \land b \in ℤ) \to a + b \in ℤ$
13	12	ancoms	$⊢ (b \in ℤ \land a \in ℤ) \to a + b \in ℤ$
14	13	adantr	$⊢ ((b \in ℤ \land a \in ℤ) \land (\exists x \in ℤ b = 2 x \land \exists y \in ℤ a = 2 y)) \to a + b \in ℤ$
15		simpl	$⊢ (y \in ℤ \land a = 2 y) \to y \in ℤ$
16		simpl	$⊢ (x \in ℤ \land b = 2 x) \to x \in ℤ$
17		zaddcl	$⊢ (y \in ℤ \land x \in ℤ) \to y + x \in ℤ$
18	15 16 17	syl2anr	$⊢ ((x \in ℤ \land b = 2 x) \land (y \in ℤ \land a = 2 y)) \to y + x \in ℤ$
19	18	adantr	$⊢ (((x \in ℤ \land b = 2 x) \land (y \in ℤ \land a = 2 y)) \land (b \in ℤ \land a \in ℤ)) \to y + x \in ℤ$
20		oveq2	$⊢ z = y + x \to 2 z = 2 (y + x)$
21	20	eqeq2d	$⊢ z = y + x \to (2 (y + x) = 2 z \leftrightarrow 2 (y + x) = 2 (y + x))$
22	21	adantl	$⊢ ((((x \in ℤ \land b = 2 x) \land (y \in ℤ \land a = 2 y)) \land (b \in ℤ \land a \in ℤ)) \land z = y + x) \to (2 (y + x) = 2 z \leftrightarrow 2 (y + x) = 2 (y + x))$
23		eqidd	$⊢ (((x \in ℤ \land b = 2 x) \land (y \in ℤ \land a = 2 y)) \land (b \in ℤ \land a \in ℤ)) \to 2 (y + x) = 2 (y + x)$
24	19 22 23	rspcedvd	$⊢ (((x \in ℤ \land b = 2 x) \land (y \in ℤ \land a = 2 y)) \land (b \in ℤ \land a \in ℤ)) \to \exists z \in ℤ 2 (y + x) = 2 z$
25		simpr	$⊢ (y \in ℤ \land a = 2 y) \to a = 2 y$
26		simpr	$⊢ (x \in ℤ \land b = 2 x) \to b = 2 x$
27	25 26	oveqan12rd	$⊢ ((x \in ℤ \land b = 2 x) \land (y \in ℤ \land a = 2 y)) \to a + b = 2 y + 2 x$
28	27	adantr	$⊢ (((x \in ℤ \land b = 2 x) \land (y \in ℤ \land a = 2 y)) \land (b \in ℤ \land a \in ℤ)) \to a + b = 2 y + 2 x$
29		2cnd	$⊢ ((x \in ℤ \land b = 2 x) \land (y \in ℤ \land a = 2 y)) \to 2 \in ℂ$
30		zcn	$⊢ y \in ℤ \to y \in ℂ$
31	30	adantr	$⊢ (y \in ℤ \land a = 2 y) \to y \in ℂ$
32	31	adantl	$⊢ ((x \in ℤ \land b = 2 x) \land (y \in ℤ \land a = 2 y)) \to y \in ℂ$
33		zcn	$⊢ x \in ℤ \to x \in ℂ$
34	33	adantr	$⊢ (x \in ℤ \land b = 2 x) \to x \in ℂ$
35	34	adantr	$⊢ ((x \in ℤ \land b = 2 x) \land (y \in ℤ \land a = 2 y)) \to x \in ℂ$
36	29 32 35	adddid	$⊢ ((x \in ℤ \land b = 2 x) \land (y \in ℤ \land a = 2 y)) \to 2 (y + x) = 2 y + 2 x$
37	36	adantr	$⊢ (((x \in ℤ \land b = 2 x) \land (y \in ℤ \land a = 2 y)) \land (b \in ℤ \land a \in ℤ)) \to 2 (y + x) = 2 y + 2 x$
38	28 37	eqtr4d	$⊢ (((x \in ℤ \land b = 2 x) \land (y \in ℤ \land a = 2 y)) \land (b \in ℤ \land a \in ℤ)) \to a + b = 2 (y + x)$
39	38	eqeq1d	$⊢ (((x \in ℤ \land b = 2 x) \land (y \in ℤ \land a = 2 y)) \land (b \in ℤ \land a \in ℤ)) \to (a + b = 2 z \leftrightarrow 2 (y + x) = 2 z)$
40	39	rexbidv	$⊢ (((x \in ℤ \land b = 2 x) \land (y \in ℤ \land a = 2 y)) \land (b \in ℤ \land a \in ℤ)) \to (\exists z \in ℤ a + b = 2 z \leftrightarrow \exists z \in ℤ 2 (y + x) = 2 z)$
41	24 40	mpbird	$⊢ (((x \in ℤ \land b = 2 x) \land (y \in ℤ \land a = 2 y)) \land (b \in ℤ \land a \in ℤ)) \to \exists z \in ℤ a + b = 2 z$
42	41	ex	$⊢ ((x \in ℤ \land b = 2 x) \land (y \in ℤ \land a = 2 y)) \to ((b \in ℤ \land a \in ℤ) \to \exists z \in ℤ a + b = 2 z)$
43	42	rexlimdvaa	$⊢ (x \in ℤ \land b = 2 x) \to (\exists y \in ℤ a = 2 y \to ((b \in ℤ \land a \in ℤ) \to \exists z \in ℤ a + b = 2 z))$
44	43	rexlimiva	$⊢ \exists x \in ℤ b = 2 x \to (\exists y \in ℤ a = 2 y \to ((b \in ℤ \land a \in ℤ) \to \exists z \in ℤ a + b = 2 z))$
45	44	imp	$⊢ (\exists x \in ℤ b = 2 x \land \exists y \in ℤ a = 2 y) \to ((b \in ℤ \land a \in ℤ) \to \exists z \in ℤ a + b = 2 z)$
46		oveq2	$⊢ x = z \to 2 x = 2 z$
47	46	eqeq2d	$⊢ x = z \to (a + b = 2 x \leftrightarrow a + b = 2 z)$
48	47	cbvrexvw	$⊢ \exists x \in ℤ a + b = 2 x \leftrightarrow \exists z \in ℤ a + b = 2 z$
49	45 48	syl6ibr	$⊢ (\exists x \in ℤ b = 2 x \land \exists y \in ℤ a = 2 y) \to ((b \in ℤ \land a \in ℤ) \to \exists x \in ℤ a + b = 2 x)$
50	49	impcom	$⊢ ((b \in ℤ \land a \in ℤ) \land (\exists x \in ℤ b = 2 x \land \exists y \in ℤ a = 2 y)) \to \exists x \in ℤ a + b = 2 x$
51		eqeq1	$⊢ z = a + b \to (z = 2 x \leftrightarrow a + b = 2 x)$
52	51	rexbidv	$⊢ z = a + b \to (\exists x \in ℤ z = 2 x \leftrightarrow \exists x \in ℤ a + b = 2 x)$
53	52 1	elrab2	$⊢ a + b \in E \leftrightarrow (a + b \in ℤ \land \exists x \in ℤ a + b = 2 x)$
54	14 50 53	sylanbrc	$⊢ ((b \in ℤ \land a \in ℤ) \land (\exists x \in ℤ b = 2 x \land \exists y \in ℤ a = 2 y)) \to a + b \in E$
55	54	exp32	$⊢ (b \in ℤ \land a \in ℤ) \to (\exists x \in ℤ b = 2 x \to (\exists y \in ℤ a = 2 y \to a + b \in E))$
56	55	impancom	$⊢ (b \in ℤ \land \exists x \in ℤ b = 2 x) \to (a \in ℤ \to (\exists y \in ℤ a = 2 y \to a + b \in E))$
57	56	com13	$⊢ \exists y \in ℤ a = 2 y \to (a \in ℤ \to ((b \in ℤ \land \exists x \in ℤ b = 2 x) \to a + b \in E))$
58	11 57	sylbi	$⊢ \exists x \in ℤ a = 2 x \to (a \in ℤ \to ((b \in ℤ \land \exists x \in ℤ b = 2 x) \to a + b \in E))$
59	58	impcom	$⊢ (a \in ℤ \land \exists x \in ℤ a = 2 x) \to ((b \in ℤ \land \exists x \in ℤ b = 2 x) \to a + b \in E)$
60	59	imp	$⊢ ((a \in ℤ \land \exists x \in ℤ a = 2 x) \land (b \in ℤ \land \exists x \in ℤ b = 2 x)) \to a + b \in E$
61	5 8 60	syl2anb	$⊢ (a \in E \land b \in E) \to a + b \in E$
62	61	rgen2	$⊢ \forall a \in E \forall b \in E a + b \in E$
63		0z	$⊢ 0 \in ℤ$
64		2cn	$⊢ 2 \in ℂ$
65		0zd	$⊢ 2 \in ℂ \to 0 \in ℤ$
66		oveq2	$⊢ x = 0 \to 2 x = 2 \cdot 0$
67	66	eqeq2d	$⊢ x = 0 \to (0 = 2 x \leftrightarrow 0 = 2 \cdot 0)$
68	67	adantl	$⊢ (2 \in ℂ \land x = 0) \to (0 = 2 x \leftrightarrow 0 = 2 \cdot 0)$
69		mul01	$⊢ 2 \in ℂ \to 2 \cdot 0 = 0$
70	69	eqcomd	$⊢ 2 \in ℂ \to 0 = 2 \cdot 0$
71	65 68 70	rspcedvd	$⊢ 2 \in ℂ \to \exists x \in ℤ 0 = 2 x$
72	64 71	ax-mp	$⊢ \exists x \in ℤ 0 = 2 x$
73		eqeq1	$⊢ z = 0 \to (z = 2 x \leftrightarrow 0 = 2 x)$
74	73	rexbidv	$⊢ z = 0 \to (\exists x \in ℤ z = 2 x \leftrightarrow \exists x \in ℤ 0 = 2 x)$
75	74	elrab	$⊢ 0 \in \{z \in ℤ \| \exists x \in ℤ z = 2 x\} \leftrightarrow (0 \in ℤ \land \exists x \in ℤ 0 = 2 x)$
76	63 72 75	mpbir2an	$⊢ 0 \in \{z \in ℤ \| \exists x \in ℤ z = 2 x\}$
77	76 1	eleqtrri	$⊢ 0 \in E$
78	1 2	2zrngbas	$⊢ E = {Base}_{R}$
79	1 2	2zrngadd	$⊢ + = +_{R}$
80	78 79	ismgmn0	$⊢ 0 \in E \to (R \in Mgm \leftrightarrow \forall a \in E \forall b \in E a + b \in E)$
81	77 80	ax-mp	$⊢ R \in Mgm \leftrightarrow \forall a \in E \forall b \in E a + b \in E$
82	62 81	mpbir	$⊢ R \in Mgm$

Metamath Proof Explorer

Theorem 2zrngamgm

Proof