Theorem mulgass 18655

Description: Product of group multiples, generalized to ℤ. (Contributed by Mario Carneiro, 13-Dec-2014.)

Hypotheses

Ref	Expression
mulgass.b	⊢ 𝐵 = (Base‘𝐺)
mulgass.t	⊢ · = (.g‘𝐺)

Assertion

Ref	Expression
mulgass	⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋)))

Proof of Theorem mulgass

Step	Hyp	Ref	Expression
1		simpr1 1192	. . 3 ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → 𝑀 ∈ ℤ)
2		elznn0 12264	. . . 4 ⊢ (𝑀 ∈ ℤ ↔ (𝑀 ∈ ℝ ∧ (𝑀 ∈ ℕ0 ∨ -𝑀 ∈ ℕ0)))
3	2	simprbi 496	. . 3 ⊢ (𝑀 ∈ ℤ → (𝑀 ∈ ℕ0 ∨ -𝑀 ∈ ℕ0))
4	1, 3	syl 17	. 2 ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → (𝑀 ∈ ℕ0 ∨ -𝑀 ∈ ℕ0))
5		simpr2 1193	. . 3 ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → 𝑁 ∈ ℤ)
6		elznn0 12264	. . . 4 ⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ0 ∨ -𝑁 ∈ ℕ0)))
7	6	simprbi 496	. . 3 ⊢ (𝑁 ∈ ℤ → (𝑁 ∈ ℕ0 ∨ -𝑁 ∈ ℕ0))
8	5, 7	syl 17	. 2 ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → (𝑁 ∈ ℕ0 ∨ -𝑁 ∈ ℕ0))
9		grpmnd 18499	. . . . . 6 ⊢ (𝐺 ∈ Grp → 𝐺 ∈ Mnd)
10	9	ad2antrr 722	. . . . 5 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → 𝐺 ∈ Mnd)
11		simprl 767	. . . . 5 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → 𝑀 ∈ ℕ0)
12		simprr 769	. . . . 5 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → 𝑁 ∈ ℕ0)
13		simplr3 1215	. . . . 5 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → 𝑋 ∈ 𝐵)
14		mulgass.b	. . . . . 6 ⊢ 𝐵 = (Base‘𝐺)
15		mulgass.t	. . . . . 6 ⊢ · = (.g‘𝐺)
16	14, 15	mulgnn0ass 18654	. . . . 5 ⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵)) → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋)))
17	10, 11, 12, 13, 16	syl13anc 1370	. . . 4 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋)))
18	17	ex 412	. . 3 ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → ((𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋))))
19	1	zcnd 12356	. . . . . . . . 9 ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → 𝑀 ∈ ℂ)
20	5	zcnd 12356	. . . . . . . . 9 ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → 𝑁 ∈ ℂ)
21	19, 20	mulneg1d 11358	. . . . . . . 8 ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → (-𝑀 · 𝑁) = -(𝑀 · 𝑁))
22	21	adantr 480	. . . . . . 7 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (-𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (-𝑀 · 𝑁) = -(𝑀 · 𝑁))
23	22	oveq1d 7270	. . . . . 6 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (-𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → ((-𝑀 · 𝑁) · 𝑋) = (-(𝑀 · 𝑁) · 𝑋))
24	9	ad2antrr 722	. . . . . . 7 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (-𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → 𝐺 ∈ Mnd)
25		simprl 767	. . . . . . 7 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (-𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → -𝑀 ∈ ℕ0)
26		simprr 769	. . . . . . 7 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (-𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → 𝑁 ∈ ℕ0)
27		simpr3 1194	. . . . . . . 8 ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → 𝑋 ∈ 𝐵)
28	27	adantr 480	. . . . . . 7 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (-𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → 𝑋 ∈ 𝐵)
29	14, 15	mulgnn0ass 18654	. . . . . . 7 ⊢ ((𝐺 ∈ Mnd ∧ (-𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵)) → ((-𝑀 · 𝑁) · 𝑋) = (-𝑀 · (𝑁 · 𝑋)))
30	24, 25, 26, 28, 29	syl13anc 1370	. . . . . 6 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (-𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → ((-𝑀 · 𝑁) · 𝑋) = (-𝑀 · (𝑁 · 𝑋)))
31	23, 30	eqtr3d 2780	. . . . 5 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (-𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → (-(𝑀 · 𝑁) · 𝑋) = (-𝑀 · (𝑁 · 𝑋)))
32		fveq2 6756	. . . . . . 7 ⊢ ((-(𝑀 · 𝑁) · 𝑋) = (-𝑀 · (𝑁 · 𝑋)) → ((invg‘𝐺)‘(-(𝑀 · 𝑁) · 𝑋)) = ((invg‘𝐺)‘(-𝑀 · (𝑁 · 𝑋))))
33		simpl 482	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → 𝐺 ∈ Grp)
34	1, 5	zmulcld 12361	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → (𝑀 · 𝑁) ∈ ℤ)
35		eqid 2738	. . . . . . . . . . . 12 ⊢ (invg‘𝐺) = (invg‘𝐺)
36	14, 15, 35	mulgneg 18637	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ Grp ∧ (𝑀 · 𝑁) ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (-(𝑀 · 𝑁) · 𝑋) = ((invg‘𝐺)‘((𝑀 · 𝑁) · 𝑋)))
37	33, 34, 27, 36	syl3anc 1369	. . . . . . . . . 10 ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → (-(𝑀 · 𝑁) · 𝑋) = ((invg‘𝐺)‘((𝑀 · 𝑁) · 𝑋)))
38	37	fveq2d 6760	. . . . . . . . 9 ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → ((invg‘𝐺)‘(-(𝑀 · 𝑁) · 𝑋)) = ((invg‘𝐺)‘((invg‘𝐺)‘((𝑀 · 𝑁) · 𝑋))))
39	14, 15	mulgcl 18636	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ Grp ∧ (𝑀 · 𝑁) ∈ ℤ ∧ 𝑋 ∈ 𝐵) → ((𝑀 · 𝑁) · 𝑋) ∈ 𝐵)
40	33, 34, 27, 39	syl3anc 1369	. . . . . . . . . 10 ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → ((𝑀 · 𝑁) · 𝑋) ∈ 𝐵)
41	14, 35	grpinvinv 18557	. . . . . . . . . 10 ⊢ ((𝐺 ∈ Grp ∧ ((𝑀 · 𝑁) · 𝑋) ∈ 𝐵) → ((invg‘𝐺)‘((invg‘𝐺)‘((𝑀 · 𝑁) · 𝑋))) = ((𝑀 · 𝑁) · 𝑋))
42	40, 41	syldan 590	. . . . . . . . 9 ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → ((invg‘𝐺)‘((invg‘𝐺)‘((𝑀 · 𝑁) · 𝑋))) = ((𝑀 · 𝑁) · 𝑋))
43	38, 42	eqtrd 2778	. . . . . . . 8 ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → ((invg‘𝐺)‘(-(𝑀 · 𝑁) · 𝑋)) = ((𝑀 · 𝑁) · 𝑋))
44	14, 15	mulgcl 18636	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (𝑁 · 𝑋) ∈ 𝐵)
45	33, 5, 27, 44	syl3anc 1369	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → (𝑁 · 𝑋) ∈ 𝐵)
46	14, 15, 35	mulgneg 18637	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ Grp ∧ 𝑀 ∈ ℤ ∧ (𝑁 · 𝑋) ∈ 𝐵) → (-𝑀 · (𝑁 · 𝑋)) = ((invg‘𝐺)‘(𝑀 · (𝑁 · 𝑋))))
47	33, 1, 45, 46	syl3anc 1369	. . . . . . . . . 10 ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → (-𝑀 · (𝑁 · 𝑋)) = ((invg‘𝐺)‘(𝑀 · (𝑁 · 𝑋))))
48	47	fveq2d 6760	. . . . . . . . 9 ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → ((invg‘𝐺)‘(-𝑀 · (𝑁 · 𝑋))) = ((invg‘𝐺)‘((invg‘𝐺)‘(𝑀 · (𝑁 · 𝑋)))))
49	14, 15	mulgcl 18636	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ Grp ∧ 𝑀 ∈ ℤ ∧ (𝑁 · 𝑋) ∈ 𝐵) → (𝑀 · (𝑁 · 𝑋)) ∈ 𝐵)
50	33, 1, 45, 49	syl3anc 1369	. . . . . . . . . 10 ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → (𝑀 · (𝑁 · 𝑋)) ∈ 𝐵)
51	14, 35	grpinvinv 18557	. . . . . . . . . 10 ⊢ ((𝐺 ∈ Grp ∧ (𝑀 · (𝑁 · 𝑋)) ∈ 𝐵) → ((invg‘𝐺)‘((invg‘𝐺)‘(𝑀 · (𝑁 · 𝑋)))) = (𝑀 · (𝑁 · 𝑋)))
52	50, 51	syldan 590	. . . . . . . . 9 ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → ((invg‘𝐺)‘((invg‘𝐺)‘(𝑀 · (𝑁 · 𝑋)))) = (𝑀 · (𝑁 · 𝑋)))
53	48, 52	eqtrd 2778	. . . . . . . 8 ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → ((invg‘𝐺)‘(-𝑀 · (𝑁 · 𝑋))) = (𝑀 · (𝑁 · 𝑋)))
54	43, 53	eqeq12d 2754	. . . . . . 7 ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → (((invg‘𝐺)‘(-(𝑀 · 𝑁) · 𝑋)) = ((invg‘𝐺)‘(-𝑀 · (𝑁 · 𝑋))) ↔ ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋))))
55	32, 54	syl5ib 243	. . . . . 6 ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → ((-(𝑀 · 𝑁) · 𝑋) = (-𝑀 · (𝑁 · 𝑋)) → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋))))
56	55	imp 406	. . . . 5 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (-(𝑀 · 𝑁) · 𝑋) = (-𝑀 · (𝑁 · 𝑋))) → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋)))
57	31, 56	syldan 590	. . . 4 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (-𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋)))
58	57	ex 412	. . 3 ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → ((-𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0) → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋))))
59	9	ad2antrr 722	. . . . . . 7 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → 𝐺 ∈ Mnd)
60		simprl 767	. . . . . . 7 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → 𝑀 ∈ ℕ0)
61		simprr 769	. . . . . . 7 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → -𝑁 ∈ ℕ0)
62	27	adantr 480	. . . . . . 7 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → 𝑋 ∈ 𝐵)
63	14, 15	mulgnn0ass 18654	. . . . . . 7 ⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵)) → ((𝑀 · -𝑁) · 𝑋) = (𝑀 · (-𝑁 · 𝑋)))
64	59, 60, 61, 62, 63	syl13anc 1370	. . . . . 6 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → ((𝑀 · -𝑁) · 𝑋) = (𝑀 · (-𝑁 · 𝑋)))
65	19, 20	mulneg2d 11359	. . . . . . . 8 ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → (𝑀 · -𝑁) = -(𝑀 · 𝑁))
66	65	adantr 480	. . . . . . 7 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → (𝑀 · -𝑁) = -(𝑀 · 𝑁))
67	66	oveq1d 7270	. . . . . 6 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → ((𝑀 · -𝑁) · 𝑋) = (-(𝑀 · 𝑁) · 𝑋))
68	14, 15, 35	mulgneg 18637	. . . . . . . . . 10 ⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (-𝑁 · 𝑋) = ((invg‘𝐺)‘(𝑁 · 𝑋)))
69	33, 5, 27, 68	syl3anc 1369	. . . . . . . . 9 ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → (-𝑁 · 𝑋) = ((invg‘𝐺)‘(𝑁 · 𝑋)))
70	69	oveq2d 7271	. . . . . . . 8 ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → (𝑀 · (-𝑁 · 𝑋)) = (𝑀 · ((invg‘𝐺)‘(𝑁 · 𝑋))))
71	14, 15, 35	mulgneg2 18652	. . . . . . . . 9 ⊢ ((𝐺 ∈ Grp ∧ 𝑀 ∈ ℤ ∧ (𝑁 · 𝑋) ∈ 𝐵) → (-𝑀 · (𝑁 · 𝑋)) = (𝑀 · ((invg‘𝐺)‘(𝑁 · 𝑋))))
72	33, 1, 45, 71	syl3anc 1369	. . . . . . . 8 ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → (-𝑀 · (𝑁 · 𝑋)) = (𝑀 · ((invg‘𝐺)‘(𝑁 · 𝑋))))
73	70, 72	eqtr4d 2781	. . . . . . 7 ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → (𝑀 · (-𝑁 · 𝑋)) = (-𝑀 · (𝑁 · 𝑋)))
74	73	adantr 480	. . . . . 6 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → (𝑀 · (-𝑁 · 𝑋)) = (-𝑀 · (𝑁 · 𝑋)))
75	64, 67, 74	3eqtr3d 2786	. . . . 5 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → (-(𝑀 · 𝑁) · 𝑋) = (-𝑀 · (𝑁 · 𝑋)))
76	75, 56	syldan 590	. . . 4 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋)))
77	76	ex 412	. . 3 ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → ((𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0) → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋))))
78	9	ad2antrr 722	. . . . . 6 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (-𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → 𝐺 ∈ Mnd)
79		simprl 767	. . . . . 6 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (-𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → -𝑀 ∈ ℕ0)
80		simprr 769	. . . . . 6 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (-𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → -𝑁 ∈ ℕ0)
81	27	adantr 480	. . . . . 6 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (-𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → 𝑋 ∈ 𝐵)
82	14, 15	mulgnn0ass 18654	. . . . . 6 ⊢ ((𝐺 ∈ Mnd ∧ (-𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵)) → ((-𝑀 · -𝑁) · 𝑋) = (-𝑀 · (-𝑁 · 𝑋)))
83	78, 79, 80, 81, 82	syl13anc 1370	. . . . 5 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (-𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → ((-𝑀 · -𝑁) · 𝑋) = (-𝑀 · (-𝑁 · 𝑋)))
84	19, 20	mul2negd 11360	. . . . . . 7 ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → (-𝑀 · -𝑁) = (𝑀 · 𝑁))
85	84	oveq1d 7270	. . . . . 6 ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → ((-𝑀 · -𝑁) · 𝑋) = ((𝑀 · 𝑁) · 𝑋))
86	85	adantr 480	. . . . 5 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (-𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → ((-𝑀 · -𝑁) · 𝑋) = ((𝑀 · 𝑁) · 𝑋))
87	33	adantr 480	. . . . . . 7 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (-𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → 𝐺 ∈ Grp)
88	1	adantr 480	. . . . . . 7 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (-𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → 𝑀 ∈ ℤ)
89		nn0z 12273	. . . . . . . . 9 ⊢ (-𝑁 ∈ ℕ0 → -𝑁 ∈ ℤ)
90	89	ad2antll 725	. . . . . . . 8 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (-𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → -𝑁 ∈ ℤ)
91	14, 15	mulgcl 18636	. . . . . . . 8 ⊢ ((𝐺 ∈ Grp ∧ -𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (-𝑁 · 𝑋) ∈ 𝐵)
92	87, 90, 81, 91	syl3anc 1369	. . . . . . 7 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (-𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → (-𝑁 · 𝑋) ∈ 𝐵)
93	14, 15, 35	mulgneg2 18652	. . . . . . 7 ⊢ ((𝐺 ∈ Grp ∧ 𝑀 ∈ ℤ ∧ (-𝑁 · 𝑋) ∈ 𝐵) → (-𝑀 · (-𝑁 · 𝑋)) = (𝑀 · ((invg‘𝐺)‘(-𝑁 · 𝑋))))
94	87, 88, 92, 93	syl3anc 1369	. . . . . 6 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (-𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → (-𝑀 · (-𝑁 · 𝑋)) = (𝑀 · ((invg‘𝐺)‘(-𝑁 · 𝑋))))
95	14, 15, 35	mulgneg 18637	. . . . . . . . 9 ⊢ ((𝐺 ∈ Grp ∧ -𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (--𝑁 · 𝑋) = ((invg‘𝐺)‘(-𝑁 · 𝑋)))
96	87, 90, 81, 95	syl3anc 1369	. . . . . . . 8 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (-𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → (--𝑁 · 𝑋) = ((invg‘𝐺)‘(-𝑁 · 𝑋)))
97	20	negnegd 11253	. . . . . . . . . 10 ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → --𝑁 = 𝑁)
98	97	adantr 480	. . . . . . . . 9 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (-𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → --𝑁 = 𝑁)
99	98	oveq1d 7270	. . . . . . . 8 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (-𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → (--𝑁 · 𝑋) = (𝑁 · 𝑋))
100	96, 99	eqtr3d 2780	. . . . . . 7 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (-𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → ((invg‘𝐺)‘(-𝑁 · 𝑋)) = (𝑁 · 𝑋))
101	100	oveq2d 7271	. . . . . 6 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (-𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → (𝑀 · ((invg‘𝐺)‘(-𝑁 · 𝑋))) = (𝑀 · (𝑁 · 𝑋)))
102	94, 101	eqtrd 2778	. . . . 5 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (-𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → (-𝑀 · (-𝑁 · 𝑋)) = (𝑀 · (𝑁 · 𝑋)))
103	83, 86, 102	3eqtr3d 2786	. . . 4 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) ∧ (-𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋)))
104	103	ex 412	. . 3 ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → ((-𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0) → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋))))
105	18, 58, 77, 104	ccased 1035	. 2 ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → (((𝑀 ∈ ℕ0 ∨ -𝑀 ∈ ℕ0) ∧ (𝑁 ∈ ℕ0 ∨ -𝑁 ∈ ℕ0)) → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋))))
106	4, 8, 105	mp2and 695	1 ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵)) → ((𝑀 · 𝑁) · 𝑋) = (𝑀 · (𝑁 · 𝑋)))

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 843   ∧ w3a 1085   = wceq 1539   ∈ wcel 2108  ‘cfv 6418  (class class class)co 7255  ℝcr 10801   · cmul 10807  -cneg 11136  ℕ₀cn0 12163  ℤcz 12249  Basecbs 16840  Mndcmnd 18300  Grpcgrp 18492  inv_gcminusg 18493  ._gcmg 18615

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pow 5283  ax-pr 5347  ax-un 7566  ax-cnex 10858  ax-resscn 10859  ax-1cn 10860  ax-icn 10861  ax-addcl 10862  ax-addrcl 10863  ax-mulcl 10864  ax-mulrcl 10865  ax-mulcom 10866  ax-addass 10867  ax-mulass 10868  ax-distr 10869  ax-i2m1 10870  ax-1ne0 10871  ax-1rid 10872  ax-rnegex 10873  ax-rrecex 10874  ax-cnre 10875  ax-pre-lttri 10876  ax-pre-lttrn 10877  ax-pre-ltadd 10878  ax-pre-mulgt0 10879

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3068  df-rex 3069  df-reu 3070  df-rmo 3071  df-rab 3072  df-v 3424  df-sbc 3712  df-csb 3829  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3902  df-nul 4254  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5154  df-tr 5188  df-id 5480  df-eprel 5486  df-po 5494  df-so 5495  df-fr 5535  df-we 5537  df-xp 5586  df-rel 5587  df-cnv 5588  df-co 5589  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593  df-pred 6191  df-ord 6254  df-on 6255  df-lim 6256  df-suc 6257  df-iota 6376  df-fun 6420  df-fn 6421  df-f 6422  df-f1 6423  df-fo 6424  df-f1o 6425  df-fv 6426  df-riota 7212  df-ov 7258  df-oprab 7259  df-mpo 7260  df-om 7688  df-1st 7804  df-2nd 7805  df-frecs 8068  df-wrecs 8099  df-recs 8173  df-rdg 8212  df-er 8456  df-en 8692  df-dom 8693  df-sdom 8694  df-pnf 10942  df-mnf 10943  df-xr 10944  df-ltxr 10945  df-le 10946  df-sub 11137  df-neg 11138  df-nn 11904  df-n0 12164  df-z 12250  df-uz 12512  df-fz 13169  df-seq 13650  df-0g 17069  df-mgm 18241  df-sgrp 18290  df-mnd 18301  df-grp 18495  df-minusg 18496  df-mulg 18616

This theorem is referenced by:  mulgassr  18656  odmod  19069  odmulgid  19076  odbezout  19080  gexdvdsi  19103  pgpfac1lem2  19593  pgpfac1lem3a  19594  pgpfac1lem3  19595  mulgrhm  20611  zlmlmod  20640