Theorem mulgnndir 13743

Description: Sum of group multiples, for positive multiples. (Contributed by Mario Carneiro, 11-Dec-2014.) (Revised by AV, 29-Aug-2021.)

Hypotheses

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

Assertion

Ref	Expression
mulgnndir	⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋)))

Proof of Theorem mulgnndir

Dummy variables 𝑥 𝑦 𝑧 𝑢 𝑣 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		sgrpmgm 13495	. . . . . 6 ⊢ (𝐺 ∈ Smgrp → 𝐺 ∈ Mgm)
2		mulgnndir.b	. . . . . . 7 ⊢ 𝐵 = (Base‘𝐺)
3		mulgnndir.p	. . . . . . 7 ⊢ + = (+g‘𝐺)
4	2, 3	mgmcl 13447	. . . . . 6 ⊢ ((𝐺 ∈ Mgm ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵)
5	1, 4	syl3an1 1306	. . . . 5 ⊢ ((𝐺 ∈ Smgrp ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 + 𝑦) ∈ 𝐵)
6	5	3expb 1230	. . . 4 ⊢ ((𝐺 ∈ Smgrp ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) ∈ 𝐵)
7	6	adantlr 477	. . 3 ⊢ (((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑥 + 𝑦) ∈ 𝐵)
8	2, 3	sgrpass 13496	. . . 4 ⊢ ((𝐺 ∈ Smgrp ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
9	8	adantlr 477	. . 3 ⊢ (((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑧 ∈ 𝐵)) → ((𝑥 + 𝑦) + 𝑧) = (𝑥 + (𝑦 + 𝑧)))
10		simpr2 1030	. . . . . 6 ⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → 𝑁 ∈ ℕ)
11		nnuz 9792	. . . . . 6 ⊢ ℕ = (ℤ≥‘1)
12	10, 11	eleqtrdi 2324	. . . . 5 ⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → 𝑁 ∈ (ℤ≥‘1))
13		simpr1 1029	. . . . . 6 ⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → 𝑀 ∈ ℕ)
14	13	nnzd 9601	. . . . 5 ⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → 𝑀 ∈ ℤ)
15		eluzadd 9785	. . . . 5 ⊢ ((𝑁 ∈ (ℤ≥‘1) ∧ 𝑀 ∈ ℤ) → (𝑁 + 𝑀) ∈ (ℤ≥‘(1 + 𝑀)))
16	12, 14, 15	syl2anc 411	. . . 4 ⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → (𝑁 + 𝑀) ∈ (ℤ≥‘(1 + 𝑀)))
17	13	nncnd 9157	. . . . 5 ⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → 𝑀 ∈ ℂ)
18	10	nncnd 9157	. . . . 5 ⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → 𝑁 ∈ ℂ)
19	17, 18	addcomd 8330	. . . 4 ⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → (𝑀 + 𝑁) = (𝑁 + 𝑀))
20		ax-1cn 8125	. . . . . 6 ⊢ 1 ∈ ℂ
21		addcom 8316	. . . . . 6 ⊢ ((𝑀 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑀 + 1) = (1 + 𝑀))
22	17, 20, 21	sylancl 413	. . . . 5 ⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → (𝑀 + 1) = (1 + 𝑀))
23	22	fveq2d 5643	. . . 4 ⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → (ℤ≥‘(𝑀 + 1)) = (ℤ≥‘(1 + 𝑀)))
24	16, 19, 23	3eltr4d 2315	. . 3 ⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → (𝑀 + 𝑁) ∈ (ℤ≥‘(𝑀 + 1)))
25	13, 11	eleqtrdi 2324	. . 3 ⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → 𝑀 ∈ (ℤ≥‘1))
26		simpr3 1031	. . . 4 ⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → 𝑋 ∈ 𝐵)
27	11, 26	ialgrlemconst 12620	. . 3 ⊢ (((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) ∧ 𝑥 ∈ (ℤ≥‘1)) → ((ℕ × {𝑋})‘𝑥) ∈ 𝐵)
28	7, 9, 24, 25, 27	seq3split 10751	. 2 ⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → (seq1( + , (ℕ × {𝑋}))‘(𝑀 + 𝑁)) = ((seq1( + , (ℕ × {𝑋}))‘𝑀) + (seq(𝑀 + 1)( + , (ℕ × {𝑋}))‘(𝑀 + 𝑁))))
29	13, 10	nnaddcld 9191	. . 3 ⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → (𝑀 + 𝑁) ∈ ℕ)
30		mulgnndir.t	. . . 4 ⊢ · = (.g‘𝐺)
31		eqid 2231	. . . 4 ⊢ seq1( + , (ℕ × {𝑋})) = seq1( + , (ℕ × {𝑋}))
32	2, 3, 30, 31	mulgnn 13718	. . 3 ⊢ (((𝑀 + 𝑁) ∈ ℕ ∧ 𝑋 ∈ 𝐵) → ((𝑀 + 𝑁) · 𝑋) = (seq1( + , (ℕ × {𝑋}))‘(𝑀 + 𝑁)))
33	29, 26, 32	syl2anc 411	. 2 ⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → ((𝑀 + 𝑁) · 𝑋) = (seq1( + , (ℕ × {𝑋}))‘(𝑀 + 𝑁)))
34	2, 3, 30, 31	mulgnn 13718	. . . 4 ⊢ ((𝑀 ∈ ℕ ∧ 𝑋 ∈ 𝐵) → (𝑀 · 𝑋) = (seq1( + , (ℕ × {𝑋}))‘𝑀))
35	13, 26, 34	syl2anc 411	. . 3 ⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → (𝑀 · 𝑋) = (seq1( + , (ℕ × {𝑋}))‘𝑀))
36		elfznn 10289	. . . . . . 7 ⊢ (𝑥 ∈ (1...𝑁) → 𝑥 ∈ ℕ)
37		fvconst2g 5868	. . . . . . 7 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑥 ∈ ℕ) → ((ℕ × {𝑋})‘𝑥) = 𝑋)
38	26, 36, 37	syl2an 289	. . . . . 6 ⊢ (((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) ∧ 𝑥 ∈ (1...𝑁)) → ((ℕ × {𝑋})‘𝑥) = 𝑋)
39		nnaddcl 9163	. . . . . . . 8 ⊢ ((𝑥 ∈ ℕ ∧ 𝑀 ∈ ℕ) → (𝑥 + 𝑀) ∈ ℕ)
40	36, 13, 39	syl2anr 290	. . . . . . 7 ⊢ (((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) ∧ 𝑥 ∈ (1...𝑁)) → (𝑥 + 𝑀) ∈ ℕ)
41		fvconst2g 5868	. . . . . . 7 ⊢ ((𝑋 ∈ 𝐵 ∧ (𝑥 + 𝑀) ∈ ℕ) → ((ℕ × {𝑋})‘(𝑥 + 𝑀)) = 𝑋)
42	26, 40, 41	syl2an2r 599	. . . . . 6 ⊢ (((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) ∧ 𝑥 ∈ (1...𝑁)) → ((ℕ × {𝑋})‘(𝑥 + 𝑀)) = 𝑋)
43	38, 42	eqtr4d 2267	. . . . 5 ⊢ (((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) ∧ 𝑥 ∈ (1...𝑁)) → ((ℕ × {𝑋})‘𝑥) = ((ℕ × {𝑋})‘(𝑥 + 𝑀)))
44		elnnuz 9793	. . . . . . 7 ⊢ (𝑢 ∈ ℕ ↔ 𝑢 ∈ (ℤ≥‘1))
45	44	biimpri 133	. . . . . 6 ⊢ (𝑢 ∈ (ℤ≥‘1) → 𝑢 ∈ ℕ)
46		fvconst2g 5868	. . . . . . . 8 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑢 ∈ ℕ) → ((ℕ × {𝑋})‘𝑢) = 𝑋)
47		simpl 109	. . . . . . . 8 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑢 ∈ ℕ) → 𝑋 ∈ 𝐵)
48	46, 47	eqeltrd 2308	. . . . . . 7 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑢 ∈ ℕ) → ((ℕ × {𝑋})‘𝑢) ∈ 𝐵)
49	48	elexd 2816	. . . . . 6 ⊢ ((𝑋 ∈ 𝐵 ∧ 𝑢 ∈ ℕ) → ((ℕ × {𝑋})‘𝑢) ∈ V)
50	26, 45, 49	syl2an 289	. . . . 5 ⊢ (((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) ∧ 𝑢 ∈ (ℤ≥‘1)) → ((ℕ × {𝑋})‘𝑢) ∈ V)
51		1nn 9154	. . . . . . . . 9 ⊢ 1 ∈ ℕ
52	51	a1i 9	. . . . . . . 8 ⊢ (((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) ∧ 𝑢 ∈ (ℤ≥‘(1 + 𝑀))) → 1 ∈ ℕ)
53	13	adantr 276	. . . . . . . 8 ⊢ (((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) ∧ 𝑢 ∈ (ℤ≥‘(1 + 𝑀))) → 𝑀 ∈ ℕ)
54	52, 53	nnaddcld 9191	. . . . . . 7 ⊢ (((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) ∧ 𝑢 ∈ (ℤ≥‘(1 + 𝑀))) → (1 + 𝑀) ∈ ℕ)
55		eluznn 9834	. . . . . . 7 ⊢ (((1 + 𝑀) ∈ ℕ ∧ 𝑢 ∈ (ℤ≥‘(1 + 𝑀))) → 𝑢 ∈ ℕ)
56	54, 55	sylancom 420	. . . . . 6 ⊢ (((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) ∧ 𝑢 ∈ (ℤ≥‘(1 + 𝑀))) → 𝑢 ∈ ℕ)
57	26, 56, 49	syl2an2r 599	. . . . 5 ⊢ (((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) ∧ 𝑢 ∈ (ℤ≥‘(1 + 𝑀))) → ((ℕ × {𝑋})‘𝑢) ∈ V)
58		simprl 531	. . . . . 6 ⊢ (((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) ∧ (𝑢 ∈ V ∧ 𝑣 ∈ V)) → 𝑢 ∈ V)
59		plusgslid 13200	. . . . . . . . 9 ⊢ (+g = Slot (+g‘ndx) ∧ (+g‘ndx) ∈ ℕ)
60	59	slotex 13114	. . . . . . . 8 ⊢ (𝐺 ∈ Smgrp → (+g‘𝐺) ∈ V)
61	3, 60	eqeltrid 2318	. . . . . . 7 ⊢ (𝐺 ∈ Smgrp → + ∈ V)
62	61	ad2antrr 488	. . . . . 6 ⊢ (((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) ∧ (𝑢 ∈ V ∧ 𝑣 ∈ V)) → + ∈ V)
63		simprr 533	. . . . . 6 ⊢ (((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) ∧ (𝑢 ∈ V ∧ 𝑣 ∈ V)) → 𝑣 ∈ V)
64		ovexg 6052	. . . . . 6 ⊢ ((𝑢 ∈ V ∧ + ∈ V ∧ 𝑣 ∈ V) → (𝑢 + 𝑣) ∈ V)
65	58, 62, 63, 64	syl3anc 1273	. . . . 5 ⊢ (((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) ∧ (𝑢 ∈ V ∧ 𝑣 ∈ V)) → (𝑢 + 𝑣) ∈ V)
66	12, 14, 43, 50, 57, 65	seq3shft2 10744	. . . 4 ⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → (seq1( + , (ℕ × {𝑋}))‘𝑁) = (seq(1 + 𝑀)( + , (ℕ × {𝑋}))‘(𝑁 + 𝑀)))
67	2, 3, 30, 31	mulgnn 13718	. . . . 5 ⊢ ((𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵) → (𝑁 · 𝑋) = (seq1( + , (ℕ × {𝑋}))‘𝑁))
68	10, 26, 67	syl2anc 411	. . . 4 ⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → (𝑁 · 𝑋) = (seq1( + , (ℕ × {𝑋}))‘𝑁))
69	22	seqeq1d 10716	. . . . 5 ⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → seq(𝑀 + 1)( + , (ℕ × {𝑋})) = seq(1 + 𝑀)( + , (ℕ × {𝑋})))
70	69, 19	fveq12d 5646	. . . 4 ⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → (seq(𝑀 + 1)( + , (ℕ × {𝑋}))‘(𝑀 + 𝑁)) = (seq(1 + 𝑀)( + , (ℕ × {𝑋}))‘(𝑁 + 𝑀)))
71	66, 68, 70	3eqtr4d 2274	. . 3 ⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → (𝑁 · 𝑋) = (seq(𝑀 + 1)( + , (ℕ × {𝑋}))‘(𝑀 + 𝑁)))
72	35, 71	oveq12d 6036	. 2 ⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → ((𝑀 · 𝑋) + (𝑁 · 𝑋)) = ((seq1( + , (ℕ × {𝑋}))‘𝑀) + (seq(𝑀 + 1)( + , (ℕ × {𝑋}))‘(𝑀 + 𝑁))))
73	28, 33, 72	3eqtr4d 2274	1 ⊢ ((𝐺 ∈ Smgrp ∧ (𝑀 ∈ ℕ ∧ 𝑁 ∈ ℕ ∧ 𝑋 ∈ 𝐵)) → ((𝑀 + 𝑁) · 𝑋) = ((𝑀 · 𝑋) + (𝑁 · 𝑋)))

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 1004   = wceq 1397   ∈ wcel 2202  Vcvv 2802  {csn 3669   × cxp 4723  ‘cfv 5326  (class class class)co 6018  ℂcc 8030  1c1 8033   + caddc 8035  ℕcn 9143  ℤcz 9479  ℤ_≥cuz 9755  ...cfz 10243  seqcseq 10710  Basecbs 13087  +_gcplusg 13165  Mgmcmgm 13442  Smgrpcsgrp 13489  ._gcmg 13711

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-13 2204  ax-14 2205  ax-ext 2213  ax-coll 4204  ax-sep 4207  ax-nul 4215  ax-pow 4264  ax-pr 4299  ax-un 4530  ax-setind 4635  ax-iinf 4686  ax-cnex 8123  ax-resscn 8124  ax-1cn 8125  ax-1re 8126  ax-icn 8127  ax-addcl 8128  ax-addrcl 8129  ax-mulcl 8130  ax-addcom 8132  ax-addass 8134  ax-distr 8136  ax-i2m1 8137  ax-0lt1 8138  ax-0id 8140  ax-rnegex 8141  ax-cnre 8143  ax-pre-ltirr 8144  ax-pre-ltwlin 8145  ax-pre-lttrn 8146  ax-pre-ltadd 8148

This theorem depends on definitions:  df-bi 117  df-dc 842  df-3or 1005  df-3an 1006  df-tru 1400  df-fal 1403  df-nf 1509  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ne 2403  df-nel 2498  df-ral 2515  df-rex 2516  df-reu 2517  df-rab 2519  df-v 2804  df-sbc 3032  df-csb 3128  df-dif 3202  df-un 3204  df-in 3206  df-ss 3213  df-nul 3495  df-if 3606  df-pw 3654  df-sn 3675  df-pr 3676  df-op 3678  df-uni 3894  df-int 3929  df-iun 3972  df-br 4089  df-opab 4151  df-mpt 4152  df-tr 4188  df-id 4390  df-iord 4463  df-on 4465  df-ilim 4466  df-suc 4468  df-iom 4689  df-xp 4731  df-rel 4732  df-cnv 4733  df-co 4734  df-dm 4735  df-rn 4736  df-res 4737  df-ima 4738  df-iota 5286  df-fun 5328  df-fn 5329  df-f 5330  df-f1 5331  df-fo 5332  df-f1o 5333  df-fv 5334  df-riota 5971  df-ov 6021  df-oprab 6022  df-mpo 6023  df-1st 6303  df-2nd 6304  df-recs 6471  df-frec 6557  df-pnf 8216  df-mnf 8217  df-xr 8218  df-ltxr 8219  df-le 8220  df-sub 8352  df-neg 8353  df-inn 9144  df-2 9202  df-n0 9403  df-z 9480  df-uz 9756  df-fz 10244  df-seqfrec 10711  df-ndx 13090  df-slot 13091  df-base 13093  df-plusg 13178  df-0g 13346  df-mgm 13444  df-sgrp 13490  df-minusg 13592  df-mulg 13712

This theorem is referenced by:  mulgnn0dir  13744  mulgnnass  13749