Theorem 2zrngmmgm

Description: R is a (multiplicative) magma. (Contributed by AV, 11-Feb-2020)

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

Proof

Step	Hyp	Ref	Expression
1		2zrng.e	⊢ 𝐸 = { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) }
2		2zrngbas.r	⊢ 𝑅 = ( ℂfld ↾s 𝐸 )
3		2zrngmmgm.1	⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
4		eqeq1	⊢ ( 𝑧 = 𝑎 → ( 𝑧 = ( 2 · 𝑥 ) ↔ 𝑎 = ( 2 · 𝑥 ) ) )
5	4	rexbidv	⊢ ( 𝑧 = 𝑎 → ( ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) ↔ ∃ 𝑥 ∈ ℤ 𝑎 = ( 2 · 𝑥 ) ) )
6	5 1	elrab2	⊢ ( 𝑎 ∈ 𝐸 ↔ ( 𝑎 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑎 = ( 2 · 𝑥 ) ) )
7		eqeq1	⊢ ( 𝑧 = 𝑏 → ( 𝑧 = ( 2 · 𝑥 ) ↔ 𝑏 = ( 2 · 𝑥 ) ) )
8	7	rexbidv	⊢ ( 𝑧 = 𝑏 → ( ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) ↔ ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ) )
9	8 1	elrab2	⊢ ( 𝑏 ∈ 𝐸 ↔ ( 𝑏 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ) )
10		zmulcl	⊢ ( ( 𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( 𝑎 · 𝑏 ) ∈ ℤ )
11	10	ad2ant2r	⊢ ( ( ( 𝑎 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑎 = ( 2 · 𝑥 ) ) ∧ ( 𝑏 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ) ) → ( 𝑎 · 𝑏 ) ∈ ℤ )
12		nfv	⊢ Ⅎ 𝑥 𝑎 ∈ ℤ
13		nfv	⊢ Ⅎ 𝑥 𝑏 ∈ ℤ
14		nfre1	⊢ Ⅎ 𝑥 ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 )
15	13 14	nfan	⊢ Ⅎ 𝑥 ( 𝑏 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) )
16		nfv	⊢ Ⅎ 𝑥 ∃ 𝑦 ∈ ℤ ( 𝑎 · 𝑏 ) = ( 2 · 𝑦 )
17	15 16	nfim	⊢ Ⅎ 𝑥 ( ( 𝑏 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ) → ∃ 𝑦 ∈ ℤ ( 𝑎 · 𝑏 ) = ( 2 · 𝑦 ) )
18	12 17	nfim	⊢ Ⅎ 𝑥 ( 𝑎 ∈ ℤ → ( ( 𝑏 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ) → ∃ 𝑦 ∈ ℤ ( 𝑎 · 𝑏 ) = ( 2 · 𝑦 ) ) )
19		simpll	⊢ ( ( ( 𝑥 ∈ ℤ ∧ 𝑎 = ( 2 · 𝑥 ) ) ∧ 𝑎 ∈ ℤ ) → 𝑥 ∈ ℤ )
20		simpl	⊢ ( ( 𝑏 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ) → 𝑏 ∈ ℤ )
21		zmulcl	⊢ ( ( 𝑥 ∈ ℤ ∧ 𝑏 ∈ ℤ ) → ( 𝑥 · 𝑏 ) ∈ ℤ )
22	19 20 21	syl2an	⊢ ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑎 = ( 2 · 𝑥 ) ) ∧ 𝑎 ∈ ℤ ) ∧ ( 𝑏 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ) ) → ( 𝑥 · 𝑏 ) ∈ ℤ )
23		oveq2	⊢ ( 𝑦 = ( 𝑥 · 𝑏 ) → ( 2 · 𝑦 ) = ( 2 · ( 𝑥 · 𝑏 ) ) )
24	23	eqeq2d	⊢ ( 𝑦 = ( 𝑥 · 𝑏 ) → ( ( 𝑎 · 𝑏 ) = ( 2 · 𝑦 ) ↔ ( 𝑎 · 𝑏 ) = ( 2 · ( 𝑥 · 𝑏 ) ) ) )
25	24	adantl	⊢ ( ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑎 = ( 2 · 𝑥 ) ) ∧ 𝑎 ∈ ℤ ) ∧ ( 𝑏 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ) ) ∧ 𝑦 = ( 𝑥 · 𝑏 ) ) → ( ( 𝑎 · 𝑏 ) = ( 2 · 𝑦 ) ↔ ( 𝑎 · 𝑏 ) = ( 2 · ( 𝑥 · 𝑏 ) ) ) )
26		oveq1	⊢ ( 𝑎 = ( 2 · 𝑥 ) → ( 𝑎 · 𝑏 ) = ( ( 2 · 𝑥 ) · 𝑏 ) )
27	26	ad3antlr	⊢ ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑎 = ( 2 · 𝑥 ) ) ∧ 𝑎 ∈ ℤ ) ∧ ( 𝑏 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ) ) → ( 𝑎 · 𝑏 ) = ( ( 2 · 𝑥 ) · 𝑏 ) )
28		2cnd	⊢ ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑎 = ( 2 · 𝑥 ) ) ∧ 𝑎 ∈ ℤ ) ∧ ( 𝑏 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ) ) → 2 ∈ ℂ )
29		zcn	⊢ ( 𝑥 ∈ ℤ → 𝑥 ∈ ℂ )
30	29	ad3antrrr	⊢ ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑎 = ( 2 · 𝑥 ) ) ∧ 𝑎 ∈ ℤ ) ∧ ( 𝑏 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ) ) → 𝑥 ∈ ℂ )
31		zcn	⊢ ( 𝑏 ∈ ℤ → 𝑏 ∈ ℂ )
32	31	adantr	⊢ ( ( 𝑏 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ) → 𝑏 ∈ ℂ )
33	32	adantl	⊢ ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑎 = ( 2 · 𝑥 ) ) ∧ 𝑎 ∈ ℤ ) ∧ ( 𝑏 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ) ) → 𝑏 ∈ ℂ )
34	28 30 33	mulassd	⊢ ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑎 = ( 2 · 𝑥 ) ) ∧ 𝑎 ∈ ℤ ) ∧ ( 𝑏 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ) ) → ( ( 2 · 𝑥 ) · 𝑏 ) = ( 2 · ( 𝑥 · 𝑏 ) ) )
35	27 34	eqtrd	⊢ ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑎 = ( 2 · 𝑥 ) ) ∧ 𝑎 ∈ ℤ ) ∧ ( 𝑏 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ) ) → ( 𝑎 · 𝑏 ) = ( 2 · ( 𝑥 · 𝑏 ) ) )
36	22 25 35	rspcedvd	⊢ ( ( ( ( 𝑥 ∈ ℤ ∧ 𝑎 = ( 2 · 𝑥 ) ) ∧ 𝑎 ∈ ℤ ) ∧ ( 𝑏 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ) ) → ∃ 𝑦 ∈ ℤ ( 𝑎 · 𝑏 ) = ( 2 · 𝑦 ) )
37	36	exp41	⊢ ( 𝑥 ∈ ℤ → ( 𝑎 = ( 2 · 𝑥 ) → ( 𝑎 ∈ ℤ → ( ( 𝑏 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ) → ∃ 𝑦 ∈ ℤ ( 𝑎 · 𝑏 ) = ( 2 · 𝑦 ) ) ) ) )
38	18 37	rexlimi	⊢ ( ∃ 𝑥 ∈ ℤ 𝑎 = ( 2 · 𝑥 ) → ( 𝑎 ∈ ℤ → ( ( 𝑏 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ) → ∃ 𝑦 ∈ ℤ ( 𝑎 · 𝑏 ) = ( 2 · 𝑦 ) ) ) )
39	38	impcom	⊢ ( ( 𝑎 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑎 = ( 2 · 𝑥 ) ) → ( ( 𝑏 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ) → ∃ 𝑦 ∈ ℤ ( 𝑎 · 𝑏 ) = ( 2 · 𝑦 ) ) )
40	39	imp	⊢ ( ( ( 𝑎 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑎 = ( 2 · 𝑥 ) ) ∧ ( 𝑏 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ) ) → ∃ 𝑦 ∈ ℤ ( 𝑎 · 𝑏 ) = ( 2 · 𝑦 ) )
41		eqeq1	⊢ ( 𝑧 = ( 𝑎 · 𝑏 ) → ( 𝑧 = ( 2 · 𝑥 ) ↔ ( 𝑎 · 𝑏 ) = ( 2 · 𝑥 ) ) )
42	41	rexbidv	⊢ ( 𝑧 = ( 𝑎 · 𝑏 ) → ( ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) ↔ ∃ 𝑥 ∈ ℤ ( 𝑎 · 𝑏 ) = ( 2 · 𝑥 ) ) )
43	42 1	elrab2	⊢ ( ( 𝑎 · 𝑏 ) ∈ 𝐸 ↔ ( ( 𝑎 · 𝑏 ) ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ ( 𝑎 · 𝑏 ) = ( 2 · 𝑥 ) ) )
44		oveq2	⊢ ( 𝑥 = 𝑦 → ( 2 · 𝑥 ) = ( 2 · 𝑦 ) )
45	44	eqeq2d	⊢ ( 𝑥 = 𝑦 → ( ( 𝑎 · 𝑏 ) = ( 2 · 𝑥 ) ↔ ( 𝑎 · 𝑏 ) = ( 2 · 𝑦 ) ) )
46	45	cbvrexvw	⊢ ( ∃ 𝑥 ∈ ℤ ( 𝑎 · 𝑏 ) = ( 2 · 𝑥 ) ↔ ∃ 𝑦 ∈ ℤ ( 𝑎 · 𝑏 ) = ( 2 · 𝑦 ) )
47	46	anbi2i	⊢ ( ( ( 𝑎 · 𝑏 ) ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ ( 𝑎 · 𝑏 ) = ( 2 · 𝑥 ) ) ↔ ( ( 𝑎 · 𝑏 ) ∈ ℤ ∧ ∃ 𝑦 ∈ ℤ ( 𝑎 · 𝑏 ) = ( 2 · 𝑦 ) ) )
48	43 47	bitri	⊢ ( ( 𝑎 · 𝑏 ) ∈ 𝐸 ↔ ( ( 𝑎 · 𝑏 ) ∈ ℤ ∧ ∃ 𝑦 ∈ ℤ ( 𝑎 · 𝑏 ) = ( 2 · 𝑦 ) ) )
49	11 40 48	sylanbrc	⊢ ( ( ( 𝑎 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑎 = ( 2 · 𝑥 ) ) ∧ ( 𝑏 ∈ ℤ ∧ ∃ 𝑥 ∈ ℤ 𝑏 = ( 2 · 𝑥 ) ) ) → ( 𝑎 · 𝑏 ) ∈ 𝐸 )
50	6 9 49	syl2anb	⊢ ( ( 𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸 ) → ( 𝑎 · 𝑏 ) ∈ 𝐸 )
51	50	rgen2	⊢ ∀ 𝑎 ∈ 𝐸 ∀ 𝑏 ∈ 𝐸 ( 𝑎 · 𝑏 ) ∈ 𝐸
52	1	0even	⊢ 0 ∈ 𝐸
53	1 2	2zrngbas	⊢ 𝐸 = ( Base ‘ 𝑅 )
54	3 53	mgpbas	⊢ 𝐸 = ( Base ‘ 𝑀 )
55	1 2	2zrngmul	⊢ · = ( .r ‘ 𝑅 )
56	3 55	mgpplusg	⊢ · = ( +g ‘ 𝑀 )
57	54 56	ismgmn0	⊢ ( 0 ∈ 𝐸 → ( 𝑀 ∈ Mgm ↔ ∀ 𝑎 ∈ 𝐸 ∀ 𝑏 ∈ 𝐸 ( 𝑎 · 𝑏 ) ∈ 𝐸 ) )
58	52 57	ax-mp	⊢ ( 𝑀 ∈ Mgm ↔ ∀ 𝑎 ∈ 𝐸 ∀ 𝑏 ∈ 𝐸 ( 𝑎 · 𝑏 ) ∈ 𝐸 )
59	51 58	mpbir	⊢ 𝑀 ∈ Mgm