Theorem mapdh6dN 39337

Description: Lemmma for mapdh6N 39345. (Contributed by NM, 1-May-2015.) (New usage is discouraged.)

Hypotheses

Ref	Expression
mapdh.q	⊢ 𝑄 = (0g‘𝐶)
mapdh.i	⊢ 𝐼 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)})))))
mapdh.h	⊢ 𝐻 = (LHyp‘𝐾)
mapdh.m	⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)
mapdh.u	⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
mapdh.v	⊢ 𝑉 = (Base‘𝑈)
mapdh.s	⊢ − = (-g‘𝑈)
mapdhc.o	⊢ 0 = (0g‘𝑈)
mapdh.n	⊢ 𝑁 = (LSpan‘𝑈)
mapdh.c	⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)
mapdh.d	⊢ 𝐷 = (Base‘𝐶)
mapdh.r	⊢ 𝑅 = (-g‘𝐶)
mapdh.j	⊢ 𝐽 = (LSpan‘𝐶)
mapdh.k	⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
mapdhc.f	⊢ (𝜑 → 𝐹 ∈ 𝐷)
mapdh.mn	⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹}))
mapdhcl.x	⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))
mapdh.p	⊢ + = (+g‘𝑈)
mapdh.a	⊢ ✚ = (+g‘𝐶)
mapdh6d.xn	⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))
mapdh6d.yz	⊢ (𝜑 → (𝑁‘{𝑌}) = (𝑁‘{𝑍}))
mapdh6d.y	⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))
mapdh6d.z	⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 }))
mapdh6d.w	⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 }))
mapdh6d.wn	⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌}))

Assertion

Ref	Expression
mapdh6dN	⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, (𝑤 + (𝑌 + 𝑍))⟩) = ((𝐼‘⟨𝑋, 𝐹, 𝑤⟩) ✚ (𝐼‘⟨𝑋, 𝐹, (𝑌 + 𝑍)⟩)))

Distinct variable groups:   𝑥,𝐷,ℎ   ℎ,𝐹,𝑥   𝑥,𝐽   𝑥,𝑀   𝑥,𝑁   𝑥, 0   𝑥,𝑄   𝑥,𝑅   𝑥, −   ℎ,𝑋,𝑥   ℎ,𝑌,𝑥   𝜑,ℎ   0 ,ℎ   𝐶,ℎ   𝐷,ℎ   ℎ,𝐽   ℎ,𝑀   ℎ,𝑁   𝑅,ℎ   𝑈,ℎ   − ,ℎ   𝑤,ℎ   ℎ,𝑍,𝑥   ✚ ,ℎ   ℎ,𝐼,𝑥   + ,ℎ,𝑥   𝑥,𝑤

Allowed substitution hints:   𝜑(𝑥,𝑤)   𝐶(𝑥,𝑤)   𝐷(𝑤)   + (𝑤)   ✚ (𝑥,𝑤)   𝑄(𝑤,ℎ)   𝑅(𝑤)   𝑈(𝑥,𝑤)   𝐹(𝑤)   𝐻(𝑥,𝑤,ℎ)   𝐼(𝑤)   𝐽(𝑤)   𝐾(𝑥,𝑤,ℎ)   𝑀(𝑤)   − (𝑤)   𝑁(𝑤)   𝑉(𝑥,𝑤,ℎ)   𝑊(𝑥,𝑤,ℎ)   𝑋(𝑤)   𝑌(𝑤)   0 (𝑤)   𝑍(𝑤)

Proof of Theorem mapdh6dN

Step	Hyp	Ref	Expression
1		mapdh.h	. . . . . 6 ⊢ 𝐻 = (LHyp‘𝐾)
2		mapdh.c	. . . . . 6 ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)
3		mapdh.k	. . . . . 6 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
4	1, 2, 3	lcdlmod 39190	. . . . 5 ⊢ (𝜑 → 𝐶 ∈ LMod)
5		mapdh.q	. . . . . 6 ⊢ 𝑄 = (0g‘𝐶)
6		mapdh.i	. . . . . 6 ⊢ 𝐼 = (𝑥 ∈ V ↦ if((2nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st ‘(1st ‘𝑥)) − (2nd ‘𝑥))})) = (𝐽‘{((2nd ‘(1st ‘𝑥))𝑅ℎ)})))))
7		mapdh.m	. . . . . 6 ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)
8		mapdh.u	. . . . . 6 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
9		mapdh.v	. . . . . 6 ⊢ 𝑉 = (Base‘𝑈)
10		mapdh.s	. . . . . 6 ⊢ − = (-g‘𝑈)
11		mapdhc.o	. . . . . 6 ⊢ 0 = (0g‘𝑈)
12		mapdh.n	. . . . . 6 ⊢ 𝑁 = (LSpan‘𝑈)
13		mapdh.d	. . . . . 6 ⊢ 𝐷 = (Base‘𝐶)
14		mapdh.r	. . . . . 6 ⊢ 𝑅 = (-g‘𝐶)
15		mapdh.j	. . . . . 6 ⊢ 𝐽 = (LSpan‘𝐶)
16		mapdhc.f	. . . . . 6 ⊢ (𝜑 → 𝐹 ∈ 𝐷)
17		mapdh.mn	. . . . . 6 ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹}))
18		mapdhcl.x	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))
19		mapdh6d.w	. . . . . . 7 ⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 }))
20	19	eldifad 3870	. . . . . 6 ⊢ (𝜑 → 𝑤 ∈ 𝑉)
21	1, 8, 3	dvhlvec 38707	. . . . . . . . 9 ⊢ (𝜑 → 𝑈 ∈ LVec)
22	18	eldifad 3870	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
23		mapdh6d.y	. . . . . . . . . 10 ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))
24	23	eldifad 3870	. . . . . . . . 9 ⊢ (𝜑 → 𝑌 ∈ 𝑉)
25		mapdh6d.wn	. . . . . . . . 9 ⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌}))
26	9, 12, 21, 20, 22, 24, 25	lspindpi 19972	. . . . . . . 8 ⊢ (𝜑 → ((𝑁‘{𝑤}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑤}) ≠ (𝑁‘{𝑌})))
27	26	simpld 498	. . . . . . 7 ⊢ (𝜑 → (𝑁‘{𝑤}) ≠ (𝑁‘{𝑋}))
28	27	necomd 3006	. . . . . 6 ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑤}))
29	5, 6, 1, 7, 8, 9, 10, 11, 12, 2, 13, 14, 15, 3, 16, 17, 18, 20, 28	mapdhcl 39325	. . . . 5 ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑤⟩) ∈ 𝐷)
30		mapdh.a	. . . . . 6 ⊢ ✚ = (+g‘𝐶)
31	13, 30, 5	lmod0vrid 19733	. . . . 5 ⊢ ((𝐶 ∈ LMod ∧ (𝐼‘⟨𝑋, 𝐹, 𝑤⟩) ∈ 𝐷) → ((𝐼‘⟨𝑋, 𝐹, 𝑤⟩) ✚ 𝑄) = (𝐼‘⟨𝑋, 𝐹, 𝑤⟩))
32	4, 29, 31	syl2anc 587	. . . 4 ⊢ (𝜑 → ((𝐼‘⟨𝑋, 𝐹, 𝑤⟩) ✚ 𝑄) = (𝐼‘⟨𝑋, 𝐹, 𝑤⟩))
33	32	adantr 484	. . 3 ⊢ ((𝜑 ∧ (𝑌 + 𝑍) = 0 ) → ((𝐼‘⟨𝑋, 𝐹, 𝑤⟩) ✚ 𝑄) = (𝐼‘⟨𝑋, 𝐹, 𝑤⟩))
34		oteq3 4774	. . . . . 6 ⊢ ((𝑌 + 𝑍) = 0 → ⟨𝑋, 𝐹, (𝑌 + 𝑍)⟩ = ⟨𝑋, 𝐹, 0 ⟩)
35	34	fveq2d 6662	. . . . 5 ⊢ ((𝑌 + 𝑍) = 0 → (𝐼‘⟨𝑋, 𝐹, (𝑌 + 𝑍)⟩) = (𝐼‘⟨𝑋, 𝐹, 0 ⟩))
36	5, 6, 11, 18, 16	mapdhval0 39323	. . . . 5 ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 0 ⟩) = 𝑄)
37	35, 36	sylan9eqr 2815	. . . 4 ⊢ ((𝜑 ∧ (𝑌 + 𝑍) = 0 ) → (𝐼‘⟨𝑋, 𝐹, (𝑌 + 𝑍)⟩) = 𝑄)
38	37	oveq2d 7166	. . 3 ⊢ ((𝜑 ∧ (𝑌 + 𝑍) = 0 ) → ((𝐼‘⟨𝑋, 𝐹, 𝑤⟩) ✚ (𝐼‘⟨𝑋, 𝐹, (𝑌 + 𝑍)⟩)) = ((𝐼‘⟨𝑋, 𝐹, 𝑤⟩) ✚ 𝑄))
39		oveq2 7158	. . . . . 6 ⊢ ((𝑌 + 𝑍) = 0 → (𝑤 + (𝑌 + 𝑍)) = (𝑤 + 0 ))
40	1, 8, 3	dvhlmod 38708	. . . . . . 7 ⊢ (𝜑 → 𝑈 ∈ LMod)
41		mapdh.p	. . . . . . . 8 ⊢ + = (+g‘𝑈)
42	9, 41, 11	lmod0vrid 19733	. . . . . . 7 ⊢ ((𝑈 ∈ LMod ∧ 𝑤 ∈ 𝑉) → (𝑤 + 0 ) = 𝑤)
43	40, 20, 42	syl2anc 587	. . . . . 6 ⊢ (𝜑 → (𝑤 + 0 ) = 𝑤)
44	39, 43	sylan9eqr 2815	. . . . 5 ⊢ ((𝜑 ∧ (𝑌 + 𝑍) = 0 ) → (𝑤 + (𝑌 + 𝑍)) = 𝑤)
45	44	oteq3d 4777	. . . 4 ⊢ ((𝜑 ∧ (𝑌 + 𝑍) = 0 ) → ⟨𝑋, 𝐹, (𝑤 + (𝑌 + 𝑍))⟩ = ⟨𝑋, 𝐹, 𝑤⟩)
46	45	fveq2d 6662	. . 3 ⊢ ((𝜑 ∧ (𝑌 + 𝑍) = 0 ) → (𝐼‘⟨𝑋, 𝐹, (𝑤 + (𝑌 + 𝑍))⟩) = (𝐼‘⟨𝑋, 𝐹, 𝑤⟩))
47	33, 38, 46	3eqtr4rd 2804	. 2 ⊢ ((𝜑 ∧ (𝑌 + 𝑍) = 0 ) → (𝐼‘⟨𝑋, 𝐹, (𝑤 + (𝑌 + 𝑍))⟩) = ((𝐼‘⟨𝑋, 𝐹, 𝑤⟩) ✚ (𝐼‘⟨𝑋, 𝐹, (𝑌 + 𝑍)⟩)))
48	3	adantr 484	. . 3 ⊢ ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
49	16	adantr 484	. . 3 ⊢ ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → 𝐹 ∈ 𝐷)
50	17	adantr 484	. . 3 ⊢ ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹}))
51	18	adantr 484	. . 3 ⊢ ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → 𝑋 ∈ (𝑉 ∖ { 0 }))
52	19	adantr 484	. . 3 ⊢ ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → 𝑤 ∈ (𝑉 ∖ { 0 }))
53		mapdh6d.z	. . . . . . 7 ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 }))
54	53	eldifad 3870	. . . . . 6 ⊢ (𝜑 → 𝑍 ∈ 𝑉)
55	9, 41	lmodvacl 19716	. . . . . 6 ⊢ ((𝑈 ∈ LMod ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉) → (𝑌 + 𝑍) ∈ 𝑉)
56	40, 24, 54, 55	syl3anc 1368	. . . . 5 ⊢ (𝜑 → (𝑌 + 𝑍) ∈ 𝑉)
57	56	anim1i 617	. . . 4 ⊢ ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → ((𝑌 + 𝑍) ∈ 𝑉 ∧ (𝑌 + 𝑍) ≠ 0 ))
58		eldifsn 4677	. . . 4 ⊢ ((𝑌 + 𝑍) ∈ (𝑉 ∖ { 0 }) ↔ ((𝑌 + 𝑍) ∈ 𝑉 ∧ (𝑌 + 𝑍) ≠ 0 ))
59	57, 58	sylibr 237	. . 3 ⊢ ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → (𝑌 + 𝑍) ∈ (𝑉 ∖ { 0 }))
60		mapdh6d.yz	. . . . . . 7 ⊢ (𝜑 → (𝑁‘{𝑌}) = (𝑁‘{𝑍}))
61		mapdh6d.xn	. . . . . . . . 9 ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))
62	9, 12, 21, 22, 24, 54, 61	lspindpi 19972	. . . . . . . 8 ⊢ (𝜑 → ((𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}) ∧ (𝑁‘{𝑋}) ≠ (𝑁‘{𝑍})))
63	62	simpld 498	. . . . . . 7 ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))
64	9, 41, 11, 12, 21, 18, 23, 53, 19, 60, 63, 25	mapdindp1 39318	. . . . . 6 ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{(𝑌 + 𝑍)}))
65	9, 41, 11, 12, 21, 18, 23, 53, 19, 60, 63, 25	mapdindp2 39319	. . . . . 6 ⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, (𝑌 + 𝑍)}))
66	9, 11, 12, 21, 18, 56, 20, 64, 65	lspindp1 19973	. . . . 5 ⊢ (𝜑 → ((𝑁‘{𝑤}) ≠ (𝑁‘{(𝑌 + 𝑍)}) ∧ ¬ 𝑋 ∈ (𝑁‘{𝑤, (𝑌 + 𝑍)})))
67	66	simprd 499	. . . 4 ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑤, (𝑌 + 𝑍)}))
68	67	adantr 484	. . 3 ⊢ ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → ¬ 𝑋 ∈ (𝑁‘{𝑤, (𝑌 + 𝑍)}))
69	26	simprd 499	. . . . . . . . 9 ⊢ (𝜑 → (𝑁‘{𝑤}) ≠ (𝑁‘{𝑌}))
70	9, 11, 12, 21, 19, 24, 69	lspsnne1 19957	. . . . . . . 8 ⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑌}))
71		eqid 2758	. . . . . . . . . 10 ⊢ (LSSum‘𝑈) = (LSSum‘𝑈)
72	9, 12, 71, 40, 24, 54	lsmpr 19929	. . . . . . . . 9 ⊢ (𝜑 → (𝑁‘{𝑌, 𝑍}) = ((𝑁‘{𝑌})(LSSum‘𝑈)(𝑁‘{𝑍})))
73	60	oveq2d 7166	. . . . . . . . 9 ⊢ (𝜑 → ((𝑁‘{𝑌})(LSSum‘𝑈)(𝑁‘{𝑌})) = ((𝑁‘{𝑌})(LSSum‘𝑈)(𝑁‘{𝑍})))
74		eqid 2758	. . . . . . . . . . . . 13 ⊢ (LSubSp‘𝑈) = (LSubSp‘𝑈)
75	9, 74, 12	lspsncl 19817	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ LMod ∧ 𝑌 ∈ 𝑉) → (𝑁‘{𝑌}) ∈ (LSubSp‘𝑈))
76	40, 24, 75	syl2anc 587	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑁‘{𝑌}) ∈ (LSubSp‘𝑈))
77	74	lsssubg 19797	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ LMod ∧ (𝑁‘{𝑌}) ∈ (LSubSp‘𝑈)) → (𝑁‘{𝑌}) ∈ (SubGrp‘𝑈))
78	40, 76, 77	syl2anc 587	. . . . . . . . . 10 ⊢ (𝜑 → (𝑁‘{𝑌}) ∈ (SubGrp‘𝑈))
79	71	lsmidm 18855	. . . . . . . . . 10 ⊢ ((𝑁‘{𝑌}) ∈ (SubGrp‘𝑈) → ((𝑁‘{𝑌})(LSSum‘𝑈)(𝑁‘{𝑌})) = (𝑁‘{𝑌}))
80	78, 79	syl 17	. . . . . . . . 9 ⊢ (𝜑 → ((𝑁‘{𝑌})(LSSum‘𝑈)(𝑁‘{𝑌})) = (𝑁‘{𝑌}))
81	72, 73, 80	3eqtr2d 2799	. . . . . . . 8 ⊢ (𝜑 → (𝑁‘{𝑌, 𝑍}) = (𝑁‘{𝑌}))
82	70, 81	neleqtrrd 2874	. . . . . . 7 ⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑌, 𝑍}))
83	9, 41, 12, 40, 24, 54, 20, 82	lspindp4 19977	. . . . . 6 ⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑌, (𝑌 + 𝑍)}))
84	9, 12, 21, 20, 24, 56, 83	lspindpi 19972	. . . . 5 ⊢ (𝜑 → ((𝑁‘{𝑤}) ≠ (𝑁‘{𝑌}) ∧ (𝑁‘{𝑤}) ≠ (𝑁‘{(𝑌 + 𝑍)})))
85	84	simprd 499	. . . 4 ⊢ (𝜑 → (𝑁‘{𝑤}) ≠ (𝑁‘{(𝑌 + 𝑍)}))
86	85	adantr 484	. . 3 ⊢ ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → (𝑁‘{𝑤}) ≠ (𝑁‘{(𝑌 + 𝑍)}))
87		eqidd 2759	. . 3 ⊢ ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → (𝐼‘⟨𝑋, 𝐹, 𝑤⟩) = (𝐼‘⟨𝑋, 𝐹, 𝑤⟩))
88		eqidd 2759	. . 3 ⊢ ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → (𝐼‘⟨𝑋, 𝐹, (𝑌 + 𝑍)⟩) = (𝐼‘⟨𝑋, 𝐹, (𝑌 + 𝑍)⟩))
89	5, 6, 1, 7, 8, 9, 10, 11, 12, 2, 13, 14, 15, 48, 49, 50, 51, 41, 30, 52, 59, 68, 86, 87, 88	mapdh6aN 39333	. 2 ⊢ ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → (𝐼‘⟨𝑋, 𝐹, (𝑤 + (𝑌 + 𝑍))⟩) = ((𝐼‘⟨𝑋, 𝐹, 𝑤⟩) ✚ (𝐼‘⟨𝑋, 𝐹, (𝑌 + 𝑍)⟩)))
90	47, 89	pm2.61dane 3038	1 ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, (𝑤 + (𝑌 + 𝑍))⟩) = ((𝐼‘⟨𝑋, 𝐹, 𝑤⟩) ✚ (𝐼‘⟨𝑋, 𝐹, (𝑌 + 𝑍)⟩)))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111   ≠ wne 2951  Vcvv 3409   ∖ cdif 3855  ifcif 4420  {csn 4522  {cpr 4524  ⟨cotp 4530   ↦ cmpt 5112  ‘cfv 6335  ℩crio 7107  (class class class)co 7150  1^st c1st 7691  2^nd c2nd 7692  Basecbs 16541  +_gcplusg 16623  0_gc0g 16771  -_gcsg 18171  SubGrpcsubg 18340  LSSumclsm 18826  LModclmod 19702  LSubSpclss 19771  LSpanclspn 19811  HLchlt 36948  LHypclh 37582  DVecHcdvh 38676  LCDualclcd 39184  mapdcmpd 39222

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-rep 5156  ax-sep 5169  ax-nul 5176  ax-pow 5234  ax-pr 5298  ax-un 7459  ax-cnex 10631  ax-resscn 10632  ax-1cn 10633  ax-icn 10634  ax-addcl 10635  ax-addrcl 10636  ax-mulcl 10637  ax-mulrcl 10638  ax-mulcom 10639  ax-addass 10640  ax-mulass 10641  ax-distr 10642  ax-i2m1 10643  ax-1ne0 10644  ax-1rid 10645  ax-rnegex 10646  ax-rrecex 10647  ax-cnre 10648  ax-pre-lttri 10649  ax-pre-lttrn 10650  ax-pre-ltadd 10651  ax-pre-mulgt0 10652  ax-riotaBAD 36551

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-nel 3056  df-ral 3075  df-rex 3076  df-reu 3077  df-rmo 3078  df-rab 3079  df-v 3411  df-sbc 3697  df-csb 3806  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-pss 3877  df-nul 4226  df-if 4421  df-pw 4496  df-sn 4523  df-pr 4525  df-tp 4527  df-op 4529  df-ot 4531  df-uni 4799  df-int 4839  df-iun 4885  df-iin 4886  df-br 5033  df-opab 5095  df-mpt 5113  df-tr 5139  df-id 5430  df-eprel 5435  df-po 5443  df-so 5444  df-fr 5483  df-we 5485  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-res 5536  df-ima 5537  df-pred 6126  df-ord 6172  df-on 6173  df-lim 6174  df-suc 6175  df-iota 6294  df-fun 6337  df-fn 6338  df-f 6339  df-f1 6340  df-fo 6341  df-f1o 6342  df-fv 6343  df-riota 7108  df-ov 7153  df-oprab 7154  df-mpo 7155  df-of 7405  df-om 7580  df-1st 7693  df-2nd 7694  df-tpos 7902  df-undef 7949  df-wrecs 7957  df-recs 8018  df-rdg 8056  df-1o 8112  df-er 8299  df-map 8418  df-en 8528  df-dom 8529  df-sdom 8530  df-fin 8531  df-pnf 10715  df-mnf 10716  df-xr 10717  df-ltxr 10718  df-le 10719  df-sub 10910  df-neg 10911  df-nn 11675  df-2 11737  df-3 11738  df-4 11739  df-5 11740  df-6 11741  df-n0 11935  df-z 12021  df-uz 12283  df-fz 12940  df-struct 16543  df-ndx 16544  df-slot 16545  df-base 16547  df-sets 16548  df-ress 16549  df-plusg 16636  df-mulr 16637  df-sca 16639  df-vsca 16640  df-0g 16773  df-mre 16915  df-mrc 16916  df-acs 16918  df-proset 17604  df-poset 17622  df-plt 17634  df-lub 17650  df-glb 17651  df-join 17652  df-meet 17653  df-p0 17715  df-p1 17716  df-lat 17722  df-clat 17784  df-mgm 17918  df-sgrp 17967  df-mnd 17978  df-submnd 18023  df-grp 18172  df-minusg 18173  df-sbg 18174  df-subg 18343  df-cntz 18514  df-oppg 18541  df-lsm 18828  df-cmn 18975  df-abl 18976  df-mgp 19308  df-ur 19320  df-ring 19367  df-oppr 19444  df-dvdsr 19462  df-unit 19463  df-invr 19493  df-dvr 19504  df-drng 19572  df-lmod 19704  df-lss 19772  df-lsp 19812  df-lvec 19943  df-lsatoms 36574  df-lshyp 36575  df-lcv 36617  df-lfl 36656  df-lkr 36684  df-ldual 36722  df-oposet 36774  df-ol 36776  df-oml 36777  df-covers 36864  df-ats 36865  df-atl 36896  df-cvlat 36920  df-hlat 36949  df-llines 37096  df-lplanes 37097  df-lvols 37098  df-lines 37099  df-psubsp 37101  df-pmap 37102  df-padd 37394  df-lhyp 37586  df-laut 37587  df-ldil 37702  df-ltrn 37703  df-trl 37757  df-tgrp 38341  df-tendo 38353  df-edring 38355  df-dveca 38601  df-disoa 38627  df-dvech 38677  df-dib 38737  df-dic 38771  df-dih 38827  df-doch 38946  df-djh 38993  df-lcdual 39185  df-mapd 39223

This theorem is referenced by:  mapdh6gN  39340