Theorem 2zrngagrp

Description: R is an (additive) group. (Contributed by AV, 6-Jan-2020)

	Ref	Expression
Hypotheses	2zrng.e	⊢ 𝐸 = { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) }
	2zrngbas.r	⊢ 𝑅 = ( ℂfld ↾s 𝐸 )
Assertion	2zrngagrp	⊢ 𝑅 ∈ Grp

Proof

Step	Hyp	Ref	Expression
1		2zrng.e	⊢ 𝐸 = { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) }
2		2zrngbas.r	⊢ 𝑅 = ( ℂfld ↾s 𝐸 )
3	1 2	2zrngamnd	⊢ 𝑅 ∈ Mnd
4		eqeq1	⊢ ( 𝑧 = 𝑦 → ( 𝑧 = ( 2 · 𝑥 ) ↔ 𝑦 = ( 2 · 𝑥 ) ) )
5	4	rexbidv	⊢ ( 𝑧 = 𝑦 → ( ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) ↔ ∃ 𝑥 ∈ ℤ 𝑦 = ( 2 · 𝑥 ) ) )
6	5 1	elrab2	⊢ ( 𝑦 ∈ 𝐸 ↔ ( 𝑦 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑦 = ( 2 · 𝑥 ) ) )
7		znegcl	⊢ ( 𝑦 ∈ ℤ → - 𝑦 ∈ ℤ )
8	7	adantr	⊢ ( ( 𝑦 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑦 = ( 2 · 𝑥 ) ) → - 𝑦 ∈ ℤ )
9		nfv	⊢ Ⅎ 𝑥 𝑦 ∈ ℤ
10		nfre1	⊢ Ⅎ 𝑥 ∃ 𝑥 ∈ ℤ - 𝑦 = ( 2 · 𝑥 )
11		znegcl	⊢ ( 𝑥 ∈ ℤ → - 𝑥 ∈ ℤ )
12	11	adantl	⊢ ( ( 𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ ) → - 𝑥 ∈ ℤ )
13	12	adantr	⊢ ( ( ( 𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ∧ 𝑦 = ( 2 · 𝑥 ) ) → - 𝑥 ∈ ℤ )
14		oveq2	⊢ ( 𝑧 = - 𝑥 → ( 2 · 𝑧 ) = ( 2 · - 𝑥 ) )
15	14	eqeq2d	⊢ ( 𝑧 = - 𝑥 → ( - 𝑦 = ( 2 · 𝑧 ) ↔ - 𝑦 = ( 2 · - 𝑥 ) ) )
16	15	adantl	⊢ ( ( ( ( 𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ∧ 𝑦 = ( 2 · 𝑥 ) ) ∧ 𝑧 = - 𝑥 ) → ( - 𝑦 = ( 2 · 𝑧 ) ↔ - 𝑦 = ( 2 · - 𝑥 ) ) )
17		negeq	⊢ ( 𝑦 = ( 2 · 𝑥 ) → - 𝑦 = - ( 2 · 𝑥 ) )
18		2cnd	⊢ ( 𝑥 ∈ ℤ → 2 ∈ ℂ )
19		zcn	⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℂ )
20	18 19	mulneg2d	⊢ ( 𝑥 ∈ ℤ → ( 2 · - 𝑥 ) = - ( 2 · 𝑥 ) )
21	20	eqcomd	⊢ ( 𝑥 ∈ ℤ → - ( 2 · 𝑥 ) = ( 2 · - 𝑥 ) )
22	21	adantl	⊢ ( ( 𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ ) → - ( 2 · 𝑥 ) = ( 2 · - 𝑥 ) )
23	17 22	sylan9eqr	⊢ ( ( ( 𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ∧ 𝑦 = ( 2 · 𝑥 ) ) → - 𝑦 = ( 2 · - 𝑥 ) )
24	13 16 23	rspcedvd	⊢ ( ( ( 𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ∧ 𝑦 = ( 2 · 𝑥 ) ) → ∃ 𝑧 ∈ ℤ - 𝑦 = ( 2 · 𝑧 ) )
25		oveq2	⊢ ( 𝑥 = 𝑧 → ( 2 · 𝑥 ) = ( 2 · 𝑧 ) )
26	25	eqeq2d	⊢ ( 𝑥 = 𝑧 → ( - 𝑦 = ( 2 · 𝑥 ) ↔ - 𝑦 = ( 2 · 𝑧 ) ) )
27	26	cbvrexvw	⊢ ( ∃ 𝑥 ∈ ℤ - 𝑦 = ( 2 · 𝑥 ) ↔ ∃ 𝑧 ∈ ℤ - 𝑦 = ( 2 · 𝑧 ) )
28	24 27	sylibr	⊢ ( ( ( 𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ ) ∧ 𝑦 = ( 2 · 𝑥 ) ) → ∃ 𝑥 ∈ ℤ - 𝑦 = ( 2 · 𝑥 ) )
29	28	exp31	⊢ ( 𝑦 ∈ ℤ → ( 𝑥 ∈ ℤ → ( 𝑦 = ( 2 · 𝑥 ) → ∃ 𝑥 ∈ ℤ - 𝑦 = ( 2 · 𝑥 ) ) ) )
30	9 10 29	rexlimd	⊢ ( 𝑦 ∈ ℤ → ( ∃ 𝑥 ∈ ℤ 𝑦 = ( 2 · 𝑥 ) → ∃ 𝑥 ∈ ℤ - 𝑦 = ( 2 · 𝑥 ) ) )
31	30	imp	⊢ ( ( 𝑦 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑦 = ( 2 · 𝑥 ) ) → ∃ 𝑥 ∈ ℤ - 𝑦 = ( 2 · 𝑥 ) )
32		eqeq1	⊢ ( 𝑧 = - 𝑦 → ( 𝑧 = ( 2 · 𝑥 ) ↔ - 𝑦 = ( 2 · 𝑥 ) ) )
33	32	rexbidv	⊢ ( 𝑧 = - 𝑦 → ( ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) ↔ ∃ 𝑥 ∈ ℤ - 𝑦 = ( 2 · 𝑥 ) ) )
34	33 1	elrab2	⊢ ( - 𝑦 ∈ 𝐸 ↔ ( - 𝑦 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ - 𝑦 = ( 2 · 𝑥 ) ) )
35	8 31 34	sylanbrc	⊢ ( ( 𝑦 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑦 = ( 2 · 𝑥 ) ) → - 𝑦 ∈ 𝐸 )
36	6 35	sylbi	⊢ ( 𝑦 ∈ 𝐸 → - 𝑦 ∈ 𝐸 )
37		oveq1	⊢ ( 𝑧 = - 𝑦 → ( 𝑧 + 𝑦 ) = ( - 𝑦 + 𝑦 ) )
38	37	eqeq1d	⊢ ( 𝑧 = - 𝑦 → ( ( 𝑧 + 𝑦 ) = 0 ↔ ( - 𝑦 + 𝑦 ) = 0 ) )
39	38	adantl	⊢ ( ( 𝑦 ∈ 𝐸 ∧ 𝑧 = - 𝑦 ) → ( ( 𝑧 + 𝑦 ) = 0 ↔ ( - 𝑦 + 𝑦 ) = 0 ) )
40		elrabi	⊢ ( 𝑦 ∈ { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) } → 𝑦 ∈ ℤ )
41	40 1	eleq2s	⊢ ( 𝑦 ∈ 𝐸 → 𝑦 ∈ ℤ )
42	41	zcnd	⊢ ( 𝑦 ∈ 𝐸 → 𝑦 ∈ ℂ )
43	42	negcld	⊢ ( 𝑦 ∈ 𝐸 → - 𝑦 ∈ ℂ )
44	43 42	addcomd	⊢ ( 𝑦 ∈ 𝐸 → ( - 𝑦 + 𝑦 ) = ( 𝑦 + - 𝑦 ) )
45	42	negidd	⊢ ( 𝑦 ∈ 𝐸 → ( 𝑦 + - 𝑦 ) = 0 )
46	44 45	eqtrd	⊢ ( 𝑦 ∈ 𝐸 → ( - 𝑦 + 𝑦 ) = 0 )
47	36 39 46	rspcedvd	⊢ ( 𝑦 ∈ 𝐸 → ∃ 𝑧 ∈ 𝐸 ( 𝑧 + 𝑦 ) = 0 )
48	47	rgen	⊢ ∀ 𝑦 ∈ 𝐸 ∃ 𝑧 ∈ 𝐸 ( 𝑧 + 𝑦 ) = 0
49	1 2	2zrngbas	⊢ 𝐸 = ( Base ‘ 𝑅 )
50	1 2	2zrngadd	⊢ + = ( +g ‘ 𝑅 )
51	1 2	2zrng0	⊢ 0 = ( 0g ‘ 𝑅 )
52	49 50 51	isgrp	⊢ ( 𝑅 ∈ Grp ↔ ( 𝑅 ∈ Mnd ∧ ∀ 𝑦 ∈ 𝐸 ∃ 𝑧 ∈ 𝐸 ( 𝑧 + 𝑦 ) = 0 ) )
53	3 48 52	mpbir2an	⊢ 𝑅 ∈ Grp