Theorem 2zrngamgm

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

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

Proof

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