Theorem mulgdirlem 19196

Description: Lemma for mulgdir 19197. (Contributed by Mario Carneiro, 13-Dec-2014.)

Hypotheses

Ref	Expression
mulgnndir.b	⊢ 𝐵 = (Base‘𝐺)
mulgnndir.t	⊢ · = (.g‘𝐺)
mulgnndir.p	⊢ + = (+g‘𝐺)

Assertion

Ref	Expression
mulgdirlem	⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋)))

Proof of Theorem mulgdirlem

Step	Hyp	Ref	Expression
1		simpl1 1210	. . . . . 6 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → 𝐺 ∈ Grp)
2	1	grpmndd 19038	. . . . 5 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → 𝐺 ∈ Mnd)
3		simprl 783	. . . . 5 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → 𝑀 ∈ ℕ0)
4		simprr 785	. . . . 5 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → 𝑁 ∈ ℕ0)
5		simpl23 1272	. . . . 5 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → 𝑋 ∈ 𝐵)
6		mulgnndir.b	. . . . . 6 ⊢ 𝐵 = (Base‘𝐺)
7		mulgnndir.t	. . . . . 6 ⊢ · = (.g‘𝐺)
8		mulgnndir.p	. . . . . 6 ⊢ + = (+g‘𝐺)
9	6, 7, 8	mulgnn0dir 19195	. . . . 5 ⊢ ((𝐺 ∈ Mnd ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵)) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋)))
10	2, 3, 4, 5, 9	syl13anc 1399	. . . 4 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ 𝑁 ∈ ℕ0)) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋)))
11	10	anassrs 473	. . 3 ⊢ ((((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ 𝑀 ∈ ℕ0) ∧ 𝑁 ∈ ℕ0) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋)))
12		simpl1 1210	. . . . . . . . . 10 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → 𝐺 ∈ Grp)
13		simp22 1226	. . . . . . . . . . 11 ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) → 𝑁 ∈ ℤ)
14	13	adantr 486	. . . . . . . . . 10 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → 𝑁 ∈ ℤ)
15		simpl23 1272	. . . . . . . . . 10 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → 𝑋 ∈ 𝐵)
16		eqid 2766	. . . . . . . . . . 11 ⊢ (invg‘𝐺) = (invg‘𝐺)
17	6, 7, 16	mulgneg 19183	. . . . . . . . . 10 ⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (-𝑁 · 𝑋) = ((invg‘𝐺)‘(𝑁 · 𝑋)))
18	12, 14, 15, 17	syl3anc 1398	. . . . . . . . 9 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → (-𝑁 · 𝑋) = ((invg‘𝐺)‘(𝑁 · 𝑋)))
19	18	oveq1d 7438	. . . . . . . 8 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → ((-𝑁 · 𝑋) + (𝑁 · 𝑋)) = (((invg‘𝐺)‘(𝑁 · 𝑋)) + (𝑁 · 𝑋)))
20	6, 7	mulgcl 19182	. . . . . . . . . 10 ⊢ ((𝐺 ∈ Grp ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (𝑁 · 𝑋) ∈ 𝐵)
21	12, 14, 15, 20	syl3anc 1398	. . . . . . . . 9 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → (𝑁 · 𝑋) ∈ 𝐵)
22		eqid 2766	. . . . . . . . . 10 ⊢ (0g‘𝐺) = (0g‘𝐺)
23	6, 8, 22, 16	grplinv 19081	. . . . . . . . 9 ⊢ ((𝐺 ∈ Grp ∧ (𝑁 · 𝑋) ∈ 𝐵) → (((invg‘𝐺)‘(𝑁 · 𝑋)) + (𝑁 · 𝑋)) = (0g‘𝐺))
24	12, 21, 23	syl2anc 596	. . . . . . . 8 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → (((invg‘𝐺)‘(𝑁 · 𝑋)) + (𝑁 · 𝑋)) = (0g‘𝐺))
25	19, 24	eqtrd 2801	. . . . . . 7 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → ((-𝑁 · 𝑋) + (𝑁 · 𝑋)) = (0g‘𝐺))
26	25	oveq2d 7439	. . . . . 6 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → (((𝑀 + 𝑁) · 𝑋) + ((-𝑁 · 𝑋) + (𝑁 · 𝑋))) = (((𝑀 + 𝑁) · 𝑋) + (0g‘𝐺)))
27		simpl3 1212	. . . . . . . . 9 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → (𝑀 + 𝑁) ∈ ℕ0)
28		nn0z 12633	. . . . . . . . 9 ⊢ ((𝑀 + 𝑁) ∈ ℕ0 → (𝑀 + 𝑁) ∈ ℤ)
29	27, 28	syl 18	. . . . . . . 8 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → (𝑀 + 𝑁) ∈ ℤ)
30	6, 7	mulgcl 19182	. . . . . . . 8 ⊢ ((𝐺 ∈ Grp ∧ (𝑀 + 𝑁) ∈ ℤ ∧ 𝑋 ∈ 𝐵) → ((𝑀 + 𝑁) · 𝑋) ∈ 𝐵)
31	12, 29, 15, 30	syl3anc 1398	. . . . . . 7 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → ((𝑀 + 𝑁) · 𝑋) ∈ 𝐵)
32	6, 8, 22	grprid 19060	. . . . . . 7 ⊢ ((𝐺 ∈ Grp ∧ ((𝑀 + 𝑁) · 𝑋) ∈ 𝐵) → (((𝑀 + 𝑁) · 𝑋) + (0g‘𝐺)) = ((𝑀 + 𝑁) · 𝑋))
33	12, 31, 32	syl2anc 596	. . . . . 6 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → (((𝑀 + 𝑁) · 𝑋) + (0g‘𝐺)) = ((𝑀 + 𝑁) · 𝑋))
34	26, 33	eqtrd 2801	. . . . 5 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → (((𝑀 + 𝑁) · 𝑋) + ((-𝑁 · 𝑋) + (𝑁 · 𝑋))) = ((𝑀 + 𝑁) · 𝑋))
35		nn0z 12633	. . . . . . . . 9 ⊢ (-𝑁 ∈ ℕ0 → -𝑁 ∈ ℤ)
36	35	ad2antll 742	. . . . . . . 8 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → -𝑁 ∈ ℤ)
37	6, 7	mulgcl 19182	. . . . . . . 8 ⊢ ((𝐺 ∈ Grp ∧ -𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (-𝑁 · 𝑋) ∈ 𝐵)
38	12, 36, 15, 37	syl3anc 1398	. . . . . . 7 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → (-𝑁 · 𝑋) ∈ 𝐵)
39	6, 8	grpass 19034	. . . . . . 7 ⊢ ((𝐺 ∈ Grp ∧ (((𝑀 + 𝑁) · 𝑋) ∈ 𝐵 ∧ (-𝑁 · 𝑋) ∈ 𝐵 ∧ (𝑁 · 𝑋) ∈ 𝐵)) → ((((𝑀 + 𝑁) · 𝑋) + (-𝑁 · 𝑋)) + (𝑁 · 𝑋)) = (((𝑀 + 𝑁) · 𝑋) + ((-𝑁 · 𝑋) + (𝑁 · 𝑋))))
40	12, 31, 38, 21, 39	syl13anc 1399	. . . . . 6 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → ((((𝑀 + 𝑁) · 𝑋) + (-𝑁 · 𝑋)) + (𝑁 · 𝑋)) = (((𝑀 + 𝑁) · 𝑋) + ((-𝑁 · 𝑋) + (𝑁 · 𝑋))))
41	12	grpmndd 19038	. . . . . . . . 9 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → 𝐺 ∈ Mnd)
42		simprr 785	. . . . . . . . 9 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → -𝑁 ∈ ℕ0)
43	6, 7, 8	mulgnn0dir 19195	. . . . . . . . 9 ⊢ ((𝐺 ∈ Mnd ∧ ((𝑀 + 𝑁) ∈ ℕ0 ∧ -𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝐵)) → (((𝑀 + 𝑁) + -𝑁) · 𝑋) = (((𝑀 + 𝑁) · 𝑋) + (-𝑁 · 𝑋)))
44	41, 27, 42, 15, 43	syl13anc 1399	. . . . . . . 8 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → (((𝑀 + 𝑁) + -𝑁) · 𝑋) = (((𝑀 + 𝑁) · 𝑋) + (-𝑁 · 𝑋)))
45		simp21 1225	. . . . . . . . . . . . . 14 ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) → 𝑀 ∈ ℤ)
46	45	zcnd 12719	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) → 𝑀 ∈ ℂ)
47	13	zcnd 12719	. . . . . . . . . . . . 13 ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) → 𝑁 ∈ ℂ)
48	46, 47	addcld 11246	. . . . . . . . . . . 12 ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) → (𝑀 + 𝑁) ∈ ℂ)
49	48	adantr 486	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → (𝑀 + 𝑁) ∈ ℂ)
50	47	adantr 486	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → 𝑁 ∈ ℂ)
51	49, 50	negsubd 11593	. . . . . . . . . 10 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → ((𝑀 + 𝑁) + -𝑁) = ((𝑀 + 𝑁) − 𝑁))
52	46	adantr 486	. . . . . . . . . . 11 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → 𝑀 ∈ ℂ)
53	52, 50	pncand 11588	. . . . . . . . . 10 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → ((𝑀 + 𝑁) − 𝑁) = 𝑀)
54	51, 53	eqtrd 2801	. . . . . . . . 9 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → ((𝑀 + 𝑁) + -𝑁) = 𝑀)
55	54	oveq1d 7438	. . . . . . . 8 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → (((𝑀 + 𝑁) + -𝑁) · 𝑋) = (𝑀 · 𝑋))
56	44, 55	eqtr3d 2803	. . . . . . 7 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → (((𝑀 + 𝑁) · 𝑋) + (-𝑁 · 𝑋)) = (𝑀 · 𝑋))
57	56	oveq1d 7438	. . . . . 6 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → ((((𝑀 + 𝑁) · 𝑋) + (-𝑁 · 𝑋)) + (𝑁 · 𝑋)) = ((𝑀 · 𝑋) + (𝑁 · 𝑋)))
58	40, 57	eqtr3d 2803	. . . . 5 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → (((𝑀 + 𝑁) · 𝑋) + ((-𝑁 · 𝑋) + (𝑁 · 𝑋))) = ((𝑀 · 𝑋) + (𝑁 · 𝑋)))
59	34, 58	eqtr3d 2803	. . . 4 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ (𝑀 ∈ ℕ0 ∧ -𝑁 ∈ ℕ0)) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋)))
60	59	anassrs 473	. . 3 ⊢ ((((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ 𝑀 ∈ ℕ0) ∧ -𝑁 ∈ ℕ0) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋)))
61		elznn0 12624	. . . . . 6 ⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ0 ∨ -𝑁 ∈ ℕ0)))
62	61	simprbi 503	. . . . 5 ⊢ (𝑁 ∈ ℤ → (𝑁 ∈ ℕ0 ∨ -𝑁 ∈ ℕ0))
63	13, 62	syl 18	. . . 4 ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) → (𝑁 ∈ ℕ0 ∨ -𝑁 ∈ ℕ0))
64	63	adantr 486	. . 3 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ 𝑀 ∈ ℕ0) → (𝑁 ∈ ℕ0 ∨ -𝑁 ∈ ℕ0))
65	11, 60, 64	mpjaodan 973	. 2 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ 𝑀 ∈ ℕ0) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋)))
66		simpl1 1210	. . . 4 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0) → 𝐺 ∈ Grp)
67	45	adantr 486	. . . . 5 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0) → 𝑀 ∈ ℤ)
68		simpl23 1272	. . . . 5 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0) → 𝑋 ∈ 𝐵)
69	6, 7	mulgcl 19182	. . . . 5 ⊢ ((𝐺 ∈ Grp ∧ 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (𝑀 · 𝑋) ∈ 𝐵)
70	66, 67, 68, 69	syl3anc 1398	. . . 4 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0) → (𝑀 · 𝑋) ∈ 𝐵)
71	67	znegcld 12720	. . . . 5 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0) → -𝑀 ∈ ℤ)
72	6, 7	mulgcl 19182	. . . . 5 ⊢ ((𝐺 ∈ Grp ∧ -𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (-𝑀 · 𝑋) ∈ 𝐵)
73	66, 71, 68, 72	syl3anc 1398	. . . 4 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0) → (-𝑀 · 𝑋) ∈ 𝐵)
74	28	3ad2ant3 1153	. . . . . 6 ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) → (𝑀 + 𝑁) ∈ ℤ)
75	74	adantr 486	. . . . 5 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0) → (𝑀 + 𝑁) ∈ ℤ)
76	66, 75, 68, 30	syl3anc 1398	. . . 4 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0) → ((𝑀 + 𝑁) · 𝑋) ∈ 𝐵)
77	6, 8	grpass 19034	. . . 4 ⊢ ((𝐺 ∈ Grp ∧ ((𝑀 · 𝑋) ∈ 𝐵 ∧ (-𝑀 · 𝑋) ∈ 𝐵 ∧ ((𝑀 + 𝑁) · 𝑋) ∈ 𝐵)) → (((𝑀 · 𝑋) + (-𝑀 · 𝑋)) + ((𝑀 + 𝑁) · 𝑋)) = ((𝑀 · 𝑋) + ((-𝑀 · 𝑋) + ((𝑀 + 𝑁) · 𝑋))))
78	66, 70, 73, 76, 77	syl13anc 1399	. . 3 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0) → (((𝑀 · 𝑋) + (-𝑀 · 𝑋)) + ((𝑀 + 𝑁) · 𝑋)) = ((𝑀 · 𝑋) + ((-𝑀 · 𝑋) + ((𝑀 + 𝑁) · 𝑋))))
79	6, 7, 16	mulgneg 19183	. . . . . . . 8 ⊢ ((𝐺 ∈ Grp ∧ 𝑀 ∈ ℤ ∧ 𝑋 ∈ 𝐵) → (-𝑀 · 𝑋) = ((invg‘𝐺)‘(𝑀 · 𝑋)))
80	66, 67, 68, 79	syl3anc 1398	. . . . . . 7 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0) → (-𝑀 · 𝑋) = ((invg‘𝐺)‘(𝑀 · 𝑋)))
81	80	oveq2d 7439	. . . . . 6 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0) → ((𝑀 · 𝑋) + (-𝑀 · 𝑋)) = ((𝑀 · 𝑋) + ((invg‘𝐺)‘(𝑀 · 𝑋))))
82	6, 8, 22, 16	grprinv 19082	. . . . . . 7 ⊢ ((𝐺 ∈ Grp ∧ (𝑀 · 𝑋) ∈ 𝐵) → ((𝑀 · 𝑋) + ((invg‘𝐺)‘(𝑀 · 𝑋))) = (0g‘𝐺))
83	66, 70, 82	syl2anc 596	. . . . . 6 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0) → ((𝑀 · 𝑋) + ((invg‘𝐺)‘(𝑀 · 𝑋))) = (0g‘𝐺))
84	81, 83	eqtrd 2801	. . . . 5 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0) → ((𝑀 · 𝑋) + (-𝑀 · 𝑋)) = (0g‘𝐺))
85	84	oveq1d 7438	. . . 4 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0) → (((𝑀 · 𝑋) + (-𝑀 · 𝑋)) + ((𝑀 + 𝑁) · 𝑋)) = ((0g‘𝐺) + ((𝑀 + 𝑁) · 𝑋)))
86	6, 8, 22	grplid 19059	. . . . 5 ⊢ ((𝐺 ∈ Grp ∧ ((𝑀 + 𝑁) · 𝑋) ∈ 𝐵) → ((0g‘𝐺) + ((𝑀 + 𝑁) · 𝑋)) = ((𝑀 + 𝑁) · 𝑋))
87	66, 76, 86	syl2anc 596	. . . 4 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0) → ((0g‘𝐺) + ((𝑀 + 𝑁) · 𝑋)) = ((𝑀 + 𝑁) · 𝑋))
88	85, 87	eqtrd 2801	. . 3 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0) → (((𝑀 · 𝑋) + (-𝑀 · 𝑋)) + ((𝑀 + 𝑁) · 𝑋)) = ((𝑀 + 𝑁) · 𝑋))
89	66	grpmndd 19038	. . . . . 6 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0) → 𝐺 ∈ Mnd)
90		simpr 490	. . . . . 6 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0) → -𝑀 ∈ ℕ0)
91		simpl3 1212	. . . . . 6 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0) → (𝑀 + 𝑁) ∈ ℕ0)
92	6, 7, 8	mulgnn0dir 19195	. . . . . 6 ⊢ ((𝐺 ∈ Mnd ∧ (-𝑀 ∈ ℕ0 ∧ (𝑀 + 𝑁) ∈ ℕ0 ∧ 𝑋 ∈ 𝐵)) → ((-𝑀 + (𝑀 + 𝑁)) · 𝑋) = ((-𝑀 · 𝑋) + ((𝑀 + 𝑁) · 𝑋)))
93	89, 90, 91, 68, 92	syl13anc 1399	. . . . 5 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0) → ((-𝑀 + (𝑀 + 𝑁)) · 𝑋) = ((-𝑀 · 𝑋) + ((𝑀 + 𝑁) · 𝑋)))
94	46	adantr 486	. . . . . . . . 9 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0) → 𝑀 ∈ ℂ)
95	94	negcld 11574	. . . . . . . 8 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0) → -𝑀 ∈ ℂ)
96	48	adantr 486	. . . . . . . 8 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0) → (𝑀 + 𝑁) ∈ ℂ)
97	95, 96	addcomd 11430	. . . . . . 7 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0) → (-𝑀 + (𝑀 + 𝑁)) = ((𝑀 + 𝑁) + -𝑀))
98	96, 94	negsubd 11593	. . . . . . 7 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0) → ((𝑀 + 𝑁) + -𝑀) = ((𝑀 + 𝑁) − 𝑀))
99	47	adantr 486	. . . . . . . 8 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0) → 𝑁 ∈ ℂ)
100	94, 99	pncan2d 11589	. . . . . . 7 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0) → ((𝑀 + 𝑁) − 𝑀) = 𝑁)
101	97, 98, 100	3eqtrd 2805	. . . . . 6 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0) → (-𝑀 + (𝑀 + 𝑁)) = 𝑁)
102	101	oveq1d 7438	. . . . 5 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0) → ((-𝑀 + (𝑀 + 𝑁)) · 𝑋) = (𝑁 · 𝑋))
103	93, 102	eqtr3d 2803	. . . 4 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0) → ((-𝑀 · 𝑋) + ((𝑀 + 𝑁) · 𝑋)) = (𝑁 · 𝑋))
104	103	oveq2d 7439	. . 3 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0) → ((𝑀 · 𝑋) + ((-𝑀 · 𝑋) + ((𝑀 + 𝑁) · 𝑋))) = ((𝑀 · 𝑋) + (𝑁 · 𝑋)))
105	78, 88, 104	3eqtr3d 2809	. 2 ⊢ (((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) ∧ -𝑀 ∈ ℕ0) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋)))
106		elznn0 12624	. . . 4 ⊢ (𝑀 ∈ ℤ ↔ (𝑀 ∈ ℝ ∧ (𝑀 ∈ ℕ0 ∨ -𝑀 ∈ ℕ0)))
107	106	simprbi 503	. . 3 ⊢ (𝑀 ∈ ℤ → (𝑀 ∈ ℕ0 ∨ -𝑀 ∈ ℕ0))
108	45, 107	syl 18	. 2 ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) → (𝑀 ∈ ℕ0 ∨ -𝑀 ∈ ℕ0))
109	65, 105, 108	mpjaodan 973	1 ⊢ ((𝐺 ∈ Grp ∧ (𝑀 ∈ ℤ ∧ 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵) ∧ (𝑀 + 𝑁) ∈ ℕ0) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∨ wo 861   ∧ w3a 1103   = wceq 1570   ∈ wcel 2146  ‘cfv 6543  (class class class)co 7423  ℂcc 11116  ℝcr 11117   + caddc 11121   − cmin 11459  -cneg 11460  ℕ₀cn0 12522  ℤcz 12609  Basecbs 17294  +_gcplusg 17335  0_gc0g 17517  Mndcmnd 18817  Grpcgrp 19025  inv_gcminusg 19026  ._gcmg 19158

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-10 2179  ax-11 2195  ax-12 2216  ax-ext 2738  ax-sep 5262  ax-nul 5274  ax-pow 5341  ax-pr 5409  ax-un 7745  ax-cnex 11174  ax-resscn 11175  ax-1cn 11176  ax-icn 11177  ax-addcl 11178  ax-addrcl 11179  ax-mulcl 11180  ax-mulrcl 11181  ax-mulcom 11182  ax-addass 11183  ax-mulass 11184  ax-distr 11185  ax-i2m1 11186  ax-1ne0 11187  ax-1rid 11188  ax-rnegex 11189  ax-rrecex 11190  ax-cnre 11191  ax-pre-lttri 11192  ax-pre-lttrn 11193  ax-pre-ltadd 11194  ax-pre-mulgt0 11195

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2570  df-eu 2600  df-clab 2745  df-cleq 2758  df-clel 2841  df-nfc 2915  df-ne 2962  df-nel 3068  df-ral 3083  df-rex 3093  df-rmo 3372  df-reu 3373  df-rab 3420  df-v 3460  df-sbc 3748  df-csb 3857  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3928  df-nul 4290  df-if 4493  df-pw 4569  df-sn 4595  df-pr 4597  df-op 4601  df-uni 4878  df-iun 4963  df-br 5115  df-opab 5179  df-mpt 5198  df-tr 5224  df-id 5561  df-eprel 5566  df-po 5574  df-so 5575  df-fr 5619  df-we 5621  df-xp 5672  df-rel 5673  df-cnv 5674  df-co 5675  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679  df-pred 6309  df-ord 6370  df-on 6371  df-lim 6372  df-suc 6373  df-iota 6499  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7380  df-ov 7426  df-oprab 7427  df-mpo 7428  df-om 7872  df-1st 7995  df-2nd 7996  df-frecs 8287  df-wrecs 8318  df-recs 8367  df-rdg 8406  df-er 8703  df-en 8953  df-dom 8954  df-sdom 8955  df-pnf 11263  df-mnf 11264  df-xr 11265  df-ltxr 11266  df-le 11267  df-sub 11461  df-neg 11462  df-nn 12252  df-n0 12523  df-z 12610  df-uz 12881  df-fz 13554  df-seq 14058  df-0g 17519  df-mgm 18723  df-sgrp 18802  df-mnd 18818  df-grp 19028  df-minusg 19029  df-mulg 19159

This theorem is used by:  mulgdir  19197