Theorem lmodvsmmulgdi 14458

Description: Distributive law for a group multiple of a scalar multiplication. (Contributed by AV, 2-Sep-2019.)

Hypotheses

Ref	Expression
lmodvsmmulgdi.v	⊢ 𝑉 = (Base‘𝑊)
lmodvsmmulgdi.f	⊢ 𝐹 = (Scalar‘𝑊)
lmodvsmmulgdi.s	⊢ · = ( ·𝑠 ‘𝑊)
lmodvsmmulgdi.k	⊢ 𝐾 = (Base‘𝐹)
lmodvsmmulgdi.p	⊢ ↑ = (.g‘𝑊)
lmodvsmmulgdi.e	⊢ 𝐸 = (.g‘𝐹)

Assertion

Ref	Expression
lmodvsmmulgdi	⊢ ((𝑊 ∈ LMod ∧ (𝐶 ∈ 𝐾 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉)) → (𝑁 ↑ (𝐶 · 𝑋)) = ((𝑁𝐸𝐶) · 𝑋))

Proof of Theorem lmodvsmmulgdi

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

Step	Hyp	Ref	Expression
1		oveq1 6056	. . . . . . 7 ⊢ (𝑥 = 0 → (𝑥 ↑ (𝐶 · 𝑋)) = (0 ↑ (𝐶 · 𝑋)))
2		oveq1 6056	. . . . . . . 8 ⊢ (𝑥 = 0 → (𝑥𝐸𝐶) = (0𝐸𝐶))
3	2	oveq1d 6064	. . . . . . 7 ⊢ (𝑥 = 0 → ((𝑥𝐸𝐶) · 𝑋) = ((0𝐸𝐶) · 𝑋))
4	1, 3	eqeq12d 2247	. . . . . 6 ⊢ (𝑥 = 0 → ((𝑥 ↑ (𝐶 · 𝑋)) = ((𝑥𝐸𝐶) · 𝑋) ↔ (0 ↑ (𝐶 · 𝑋)) = ((0𝐸𝐶) · 𝑋)))
5	4	imbi2d 230	. . . . 5 ⊢ (𝑥 = 0 → ((((𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑥 ↑ (𝐶 · 𝑋)) = ((𝑥𝐸𝐶) · 𝑋)) ↔ (((𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (0 ↑ (𝐶 · 𝑋)) = ((0𝐸𝐶) · 𝑋))))
6		oveq1 6056	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝑥 ↑ (𝐶 · 𝑋)) = (𝑦 ↑ (𝐶 · 𝑋)))
7		oveq1 6056	. . . . . . . 8 ⊢ (𝑥 = 𝑦 → (𝑥𝐸𝐶) = (𝑦𝐸𝐶))
8	7	oveq1d 6064	. . . . . . 7 ⊢ (𝑥 = 𝑦 → ((𝑥𝐸𝐶) · 𝑋) = ((𝑦𝐸𝐶) · 𝑋))
9	6, 8	eqeq12d 2247	. . . . . 6 ⊢ (𝑥 = 𝑦 → ((𝑥 ↑ (𝐶 · 𝑋)) = ((𝑥𝐸𝐶) · 𝑋) ↔ (𝑦 ↑ (𝐶 · 𝑋)) = ((𝑦𝐸𝐶) · 𝑋)))
10	9	imbi2d 230	. . . . 5 ⊢ (𝑥 = 𝑦 → ((((𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑥 ↑ (𝐶 · 𝑋)) = ((𝑥𝐸𝐶) · 𝑋)) ↔ (((𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑦 ↑ (𝐶 · 𝑋)) = ((𝑦𝐸𝐶) · 𝑋))))
11		oveq1 6056	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → (𝑥 ↑ (𝐶 · 𝑋)) = ((𝑦 + 1) ↑ (𝐶 · 𝑋)))
12		oveq1 6056	. . . . . . . 8 ⊢ (𝑥 = (𝑦 + 1) → (𝑥𝐸𝐶) = ((𝑦 + 1)𝐸𝐶))
13	12	oveq1d 6064	. . . . . . 7 ⊢ (𝑥 = (𝑦 + 1) → ((𝑥𝐸𝐶) · 𝑋) = (((𝑦 + 1)𝐸𝐶) · 𝑋))
14	11, 13	eqeq12d 2247	. . . . . 6 ⊢ (𝑥 = (𝑦 + 1) → ((𝑥 ↑ (𝐶 · 𝑋)) = ((𝑥𝐸𝐶) · 𝑋) ↔ ((𝑦 + 1) ↑ (𝐶 · 𝑋)) = (((𝑦 + 1)𝐸𝐶) · 𝑋)))
15	14	imbi2d 230	. . . . 5 ⊢ (𝑥 = (𝑦 + 1) → ((((𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑥 ↑ (𝐶 · 𝑋)) = ((𝑥𝐸𝐶) · 𝑋)) ↔ (((𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → ((𝑦 + 1) ↑ (𝐶 · 𝑋)) = (((𝑦 + 1)𝐸𝐶) · 𝑋))))
16		oveq1 6056	. . . . . . 7 ⊢ (𝑥 = 𝑁 → (𝑥 ↑ (𝐶 · 𝑋)) = (𝑁 ↑ (𝐶 · 𝑋)))
17		oveq1 6056	. . . . . . . 8 ⊢ (𝑥 = 𝑁 → (𝑥𝐸𝐶) = (𝑁𝐸𝐶))
18	17	oveq1d 6064	. . . . . . 7 ⊢ (𝑥 = 𝑁 → ((𝑥𝐸𝐶) · 𝑋) = ((𝑁𝐸𝐶) · 𝑋))
19	16, 18	eqeq12d 2247	. . . . . 6 ⊢ (𝑥 = 𝑁 → ((𝑥 ↑ (𝐶 · 𝑋)) = ((𝑥𝐸𝐶) · 𝑋) ↔ (𝑁 ↑ (𝐶 · 𝑋)) = ((𝑁𝐸𝐶) · 𝑋)))
20	19	imbi2d 230	. . . . 5 ⊢ (𝑥 = 𝑁 → ((((𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑥 ↑ (𝐶 · 𝑋)) = ((𝑥𝐸𝐶) · 𝑋)) ↔ (((𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑁 ↑ (𝐶 · 𝑋)) = ((𝑁𝐸𝐶) · 𝑋))))
21		simpr 110	. . . . . . 7 ⊢ (((𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → 𝑊 ∈ LMod)
22		simpr 110	. . . . . . . 8 ⊢ ((𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) → 𝑋 ∈ 𝑉)
23	22	adantr 276	. . . . . . 7 ⊢ (((𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → 𝑋 ∈ 𝑉)
24		lmodvsmmulgdi.v	. . . . . . . 8 ⊢ 𝑉 = (Base‘𝑊)
25		lmodvsmmulgdi.f	. . . . . . . 8 ⊢ 𝐹 = (Scalar‘𝑊)
26		lmodvsmmulgdi.s	. . . . . . . 8 ⊢ · = ( ·𝑠 ‘𝑊)
27		eqid 2232	. . . . . . . 8 ⊢ (0g‘𝐹) = (0g‘𝐹)
28		eqid 2232	. . . . . . . 8 ⊢ (0g‘𝑊) = (0g‘𝑊)
29	24, 25, 26, 27, 28	lmod0vs 14456	. . . . . . 7 ⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → ((0g‘𝐹) · 𝑋) = (0g‘𝑊))
30	21, 23, 29	syl2anc 411	. . . . . 6 ⊢ (((𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → ((0g‘𝐹) · 𝑋) = (0g‘𝑊))
31		simpl 109	. . . . . . . . 9 ⊢ ((𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) → 𝐶 ∈ 𝐾)
32	31	adantr 276	. . . . . . . 8 ⊢ (((𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → 𝐶 ∈ 𝐾)
33		lmodvsmmulgdi.k	. . . . . . . . 9 ⊢ 𝐾 = (Base‘𝐹)
34		lmodvsmmulgdi.e	. . . . . . . . 9 ⊢ 𝐸 = (.g‘𝐹)
35	33, 27, 34	mulg0 13831	. . . . . . . 8 ⊢ (𝐶 ∈ 𝐾 → (0𝐸𝐶) = (0g‘𝐹))
36	32, 35	syl 14	. . . . . . 7 ⊢ (((𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (0𝐸𝐶) = (0g‘𝐹))
37	36	oveq1d 6064	. . . . . 6 ⊢ (((𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → ((0𝐸𝐶) · 𝑋) = ((0g‘𝐹) · 𝑋))
38	24, 25, 26, 33	lmodvscl 14440	. . . . . . . 8 ⊢ ((𝑊 ∈ LMod ∧ 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) → (𝐶 · 𝑋) ∈ 𝑉)
39	21, 32, 23, 38	syl3anc 1274	. . . . . . 7 ⊢ (((𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝐶 · 𝑋) ∈ 𝑉)
40		lmodvsmmulgdi.p	. . . . . . . 8 ⊢ ↑ = (.g‘𝑊)
41	24, 28, 40	mulg0 13831	. . . . . . 7 ⊢ ((𝐶 · 𝑋) ∈ 𝑉 → (0 ↑ (𝐶 · 𝑋)) = (0g‘𝑊))
42	39, 41	syl 14	. . . . . 6 ⊢ (((𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (0 ↑ (𝐶 · 𝑋)) = (0g‘𝑊))
43	30, 37, 42	3eqtr4rd 2276	. . . . 5 ⊢ (((𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (0 ↑ (𝐶 · 𝑋)) = ((0𝐸𝐶) · 𝑋))
44		lmodgrp 14429	. . . . . . . . . . . 12 ⊢ (𝑊 ∈ LMod → 𝑊 ∈ Grp)
45	44	grpmndd 13715	. . . . . . . . . . 11 ⊢ (𝑊 ∈ LMod → 𝑊 ∈ Mnd)
46	45	ad2antll 491	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ0 ∧ ((𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → 𝑊 ∈ Mnd)
47		simpl 109	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ0 ∧ ((𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → 𝑦 ∈ ℕ0)
48	39	adantl 277	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ0 ∧ ((𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → (𝐶 · 𝑋) ∈ 𝑉)
49		eqid 2232	. . . . . . . . . . 11 ⊢ (+g‘𝑊) = (+g‘𝑊)
50	24, 40, 49	mulgnn0p1 13839	. . . . . . . . . 10 ⊢ ((𝑊 ∈ Mnd ∧ 𝑦 ∈ ℕ0 ∧ (𝐶 · 𝑋) ∈ 𝑉) → ((𝑦 + 1) ↑ (𝐶 · 𝑋)) = ((𝑦 ↑ (𝐶 · 𝑋))(+g‘𝑊)(𝐶 · 𝑋)))
51	46, 47, 48, 50	syl3anc 1274	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ0 ∧ ((𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → ((𝑦 + 1) ↑ (𝐶 · 𝑋)) = ((𝑦 ↑ (𝐶 · 𝑋))(+g‘𝑊)(𝐶 · 𝑋)))
52	51	adantr 276	. . . . . . . 8 ⊢ (((𝑦 ∈ ℕ0 ∧ ((𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) ∧ (𝑦 ↑ (𝐶 · 𝑋)) = ((𝑦𝐸𝐶) · 𝑋)) → ((𝑦 + 1) ↑ (𝐶 · 𝑋)) = ((𝑦 ↑ (𝐶 · 𝑋))(+g‘𝑊)(𝐶 · 𝑋)))
53		oveq1 6056	. . . . . . . . 9 ⊢ ((𝑦 ↑ (𝐶 · 𝑋)) = ((𝑦𝐸𝐶) · 𝑋) → ((𝑦 ↑ (𝐶 · 𝑋))(+g‘𝑊)(𝐶 · 𝑋)) = (((𝑦𝐸𝐶) · 𝑋)(+g‘𝑊)(𝐶 · 𝑋)))
54	21	adantl 277	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℕ0 ∧ ((𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → 𝑊 ∈ LMod)
55	25	lmodring 14430	. . . . . . . . . . . . . 14 ⊢ (𝑊 ∈ LMod → 𝐹 ∈ Ring)
56		ringmnd 14139	. . . . . . . . . . . . . 14 ⊢ (𝐹 ∈ Ring → 𝐹 ∈ Mnd)
57	55, 56	syl 14	. . . . . . . . . . . . 13 ⊢ (𝑊 ∈ LMod → 𝐹 ∈ Mnd)
58	57	ad2antll 491	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ ℕ0 ∧ ((𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → 𝐹 ∈ Mnd)
59		simprll 539	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ ℕ0 ∧ ((𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → 𝐶 ∈ 𝐾)
60	33, 34, 58, 47, 59	mulgnn0cld 13849	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℕ0 ∧ ((𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → (𝑦𝐸𝐶) ∈ 𝐾)
61	23	adantl 277	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℕ0 ∧ ((𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → 𝑋 ∈ 𝑉)
62		eqid 2232	. . . . . . . . . . . 12 ⊢ (+g‘𝐹) = (+g‘𝐹)
63	24, 49, 25, 26, 33, 62	lmodvsdir 14447	. . . . . . . . . . 11 ⊢ ((𝑊 ∈ LMod ∧ ((𝑦𝐸𝐶) ∈ 𝐾 ∧ 𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉)) → (((𝑦𝐸𝐶)(+g‘𝐹)𝐶) · 𝑋) = (((𝑦𝐸𝐶) · 𝑋)(+g‘𝑊)(𝐶 · 𝑋)))
64	54, 60, 59, 61, 63	syl13anc 1276	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ0 ∧ ((𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → (((𝑦𝐸𝐶)(+g‘𝐹)𝐶) · 𝑋) = (((𝑦𝐸𝐶) · 𝑋)(+g‘𝑊)(𝐶 · 𝑋)))
65	33, 34, 62	mulgnn0p1 13839	. . . . . . . . . . . . 13 ⊢ ((𝐹 ∈ Mnd ∧ 𝑦 ∈ ℕ0 ∧ 𝐶 ∈ 𝐾) → ((𝑦 + 1)𝐸𝐶) = ((𝑦𝐸𝐶)(+g‘𝐹)𝐶))
66	58, 47, 59, 65	syl3anc 1274	. . . . . . . . . . . 12 ⊢ ((𝑦 ∈ ℕ0 ∧ ((𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → ((𝑦 + 1)𝐸𝐶) = ((𝑦𝐸𝐶)(+g‘𝐹)𝐶))
67	66	eqcomd 2238	. . . . . . . . . . 11 ⊢ ((𝑦 ∈ ℕ0 ∧ ((𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → ((𝑦𝐸𝐶)(+g‘𝐹)𝐶) = ((𝑦 + 1)𝐸𝐶))
68	67	oveq1d 6064	. . . . . . . . . 10 ⊢ ((𝑦 ∈ ℕ0 ∧ ((𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → (((𝑦𝐸𝐶)(+g‘𝐹)𝐶) · 𝑋) = (((𝑦 + 1)𝐸𝐶) · 𝑋))
69	64, 68	eqtr3d 2267	. . . . . . . . 9 ⊢ ((𝑦 ∈ ℕ0 ∧ ((𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) → (((𝑦𝐸𝐶) · 𝑋)(+g‘𝑊)(𝐶 · 𝑋)) = (((𝑦 + 1)𝐸𝐶) · 𝑋))
70	53, 69	sylan9eqr 2287	. . . . . . . 8 ⊢ (((𝑦 ∈ ℕ0 ∧ ((𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) ∧ (𝑦 ↑ (𝐶 · 𝑋)) = ((𝑦𝐸𝐶) · 𝑋)) → ((𝑦 ↑ (𝐶 · 𝑋))(+g‘𝑊)(𝐶 · 𝑋)) = (((𝑦 + 1)𝐸𝐶) · 𝑋))
71	52, 70	eqtrd 2265	. . . . . . 7 ⊢ (((𝑦 ∈ ℕ0 ∧ ((𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod)) ∧ (𝑦 ↑ (𝐶 · 𝑋)) = ((𝑦𝐸𝐶) · 𝑋)) → ((𝑦 + 1) ↑ (𝐶 · 𝑋)) = (((𝑦 + 1)𝐸𝐶) · 𝑋))
72	71	exp31 364	. . . . . 6 ⊢ (𝑦 ∈ ℕ0 → (((𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → ((𝑦 ↑ (𝐶 · 𝑋)) = ((𝑦𝐸𝐶) · 𝑋) → ((𝑦 + 1) ↑ (𝐶 · 𝑋)) = (((𝑦 + 1)𝐸𝐶) · 𝑋))))
73	72	a2d 26	. . . . 5 ⊢ (𝑦 ∈ ℕ0 → ((((𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑦 ↑ (𝐶 · 𝑋)) = ((𝑦𝐸𝐶) · 𝑋)) → (((𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → ((𝑦 + 1) ↑ (𝐶 · 𝑋)) = (((𝑦 + 1)𝐸𝐶) · 𝑋))))
74	5, 10, 15, 20, 43, 73	nn0ind 9688	. . . 4 ⊢ (𝑁 ∈ ℕ0 → (((𝐶 ∈ 𝐾 ∧ 𝑋 ∈ 𝑉) ∧ 𝑊 ∈ LMod) → (𝑁 ↑ (𝐶 · 𝑋)) = ((𝑁𝐸𝐶) · 𝑋)))
75	74	exp4c 368	. . 3 ⊢ (𝑁 ∈ ℕ0 → (𝐶 ∈ 𝐾 → (𝑋 ∈ 𝑉 → (𝑊 ∈ LMod → (𝑁 ↑ (𝐶 · 𝑋)) = ((𝑁𝐸𝐶) · 𝑋)))))
76	75	3imp21 1225	. 2 ⊢ ((𝐶 ∈ 𝐾 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉) → (𝑊 ∈ LMod → (𝑁 ↑ (𝐶 · 𝑋)) = ((𝑁𝐸𝐶) · 𝑋)))
77	76	impcom 125	1 ⊢ ((𝑊 ∈ LMod ∧ (𝐶 ∈ 𝐾 ∧ 𝑁 ∈ ℕ0 ∧ 𝑋 ∈ 𝑉)) → (𝑁 ↑ (𝐶 · 𝑋)) = ((𝑁𝐸𝐶) · 𝑋))

Syntax hints:   → wi 4   ∧ wa 104   ∧ w3a 1005   = wceq 1398   ∈ wcel 2203  ‘cfv 5351  (class class class)co 6049  0cc0 8123  1c1 8124   + caddc 8126  ℕ₀cn0 9492  Basecbs 13201  +_gcplusg 13279  Scalarcsca 13282   ·_𝑠 cvsca 13283  0_gc0g 13458  Mndcmnd 13618  ._gcmg 13825  Ringcrg 14129  LModclmod 14422

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2205  ax-14 2206  ax-ext 2214  ax-coll 4224  ax-sep 4227  ax-nul 4235  ax-pow 4286  ax-pr 4321  ax-un 4553  ax-setind 4658  ax-iinf 4709  ax-cnex 8214  ax-resscn 8215  ax-1cn 8216  ax-1re 8217  ax-icn 8218  ax-addcl 8219  ax-addrcl 8220  ax-mulcl 8221  ax-addcom 8223  ax-addass 8225  ax-distr 8227  ax-i2m1 8228  ax-0lt1 8229  ax-0id 8231  ax-rnegex 8232  ax-cnre 8234  ax-pre-ltirr 8235  ax-pre-ltwlin 8236  ax-pre-lttrn 8237  ax-pre-ltadd 8239

This theorem depends on definitions:  df-bi 117  df-dc 843  df-3or 1006  df-3an 1007  df-tru 1401  df-fal 1404  df-nf 1510  df-sb 1812  df-eu 2083  df-mo 2084  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ne 2413  df-nel 2508  df-ral 2525  df-rex 2526  df-reu 2527  df-rmo 2528  df-rab 2529  df-v 2814  df-sbc 3042  df-csb 3138  df-dif 3212  df-un 3214  df-in 3216  df-ss 3223  df-nul 3508  df-if 3620  df-pw 3670  df-sn 3694  df-pr 3695  df-op 3697  df-uni 3914  df-int 3949  df-iun 3992  df-br 4109  df-opab 4171  df-mpt 4172  df-tr 4208  df-id 4413  df-iord 4486  df-on 4488  df-ilim 4489  df-suc 4491  df-iom 4712  df-xp 4754  df-rel 4755  df-cnv 4756  df-co 4757  df-dm 4758  df-rn 4759  df-res 4760  df-ima 4761  df-iota 5311  df-fun 5353  df-fn 5354  df-f 5355  df-f1 5356  df-fo 5357  df-f1o 5358  df-fv 5359  df-riota 6002  df-ov 6052  df-oprab 6053  df-mpo 6054  df-1st 6333  df-2nd 6334  df-recs 6535  df-frec 6621  df-pnf 8306  df-mnf 8307  df-xr 8308  df-ltxr 8309  df-le 8310  df-sub 8442  df-neg 8443  df-inn 9234  df-2 9292  df-3 9293  df-4 9294  df-5 9295  df-6 9296  df-n0 9493  df-z 9574  df-uz 9850  df-seqfrec 10806  df-ndx 13204  df-slot 13205  df-base 13207  df-plusg 13292  df-mulr 13293  df-sca 13295  df-vsca 13296  df-0g 13460  df-mgm 13558  df-sgrp 13604  df-mnd 13619  df-grp 13705  df-minusg 13706  df-mulg 13826  df-ring 14131  df-lmod 14424

This theorem is referenced by: (None)