lcfrlem35 - Mathbox for Norm Megill

	Mathbox for Norm Megill		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > lcfrlem35		Structured version Visualization version GIF version

Theorem lcfrlem35 35667

Description: Lemma for lcfr 35675. (Contributed by NM, 2-Mar-2015.)

**Hypotheses**
Ref	Expression
lcfrlem17.h	⊢ 𝐻 = (LHyp‘𝐾)
lcfrlem17.o	⊢ ⊥ = ((ocH‘𝐾)‘𝑊)
lcfrlem17.u	⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
lcfrlem17.v	⊢ 𝑉 = (Base‘𝑈)
lcfrlem17.p	⊢ + = (+_g‘𝑈)
lcfrlem17.z	⊢ 0 = (0_g‘𝑈)
lcfrlem17.n	⊢ 𝑁 = (LSpan‘𝑈)
lcfrlem17.a	⊢ 𝐴 = (LSAtoms‘𝑈)
lcfrlem17.k	⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
lcfrlem17.x	⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))
lcfrlem17.y	⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))
lcfrlem17.ne	⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))
lcfrlem22.b	⊢ 𝐵 = ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)}))
lcfrlem24.t	⊢ · = ( ·_𝑠 ‘𝑈)
lcfrlem24.s	⊢ 𝑆 = (Scalar‘𝑈)
lcfrlem24.q	⊢ 𝑄 = (0_g‘𝑆)
lcfrlem24.r	⊢ 𝑅 = (Base‘𝑆)
lcfrlem24.j	⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥)))))
lcfrlem24.ib	⊢ (𝜑 → 𝐼 ∈ 𝐵)
lcfrlem24.l	⊢ 𝐿 = (LKer‘𝑈)
lcfrlem25.d	⊢ 𝐷 = (LDual‘𝑈)
lcfrlem28.jn	⊢ (𝜑 → ((𝐽‘𝑌)‘𝐼) ≠ 𝑄)
lcfrlem29.i	⊢ 𝐹 = (inv_r‘𝑆)
lcfrlem30.m	⊢ − = (-_g‘𝐷)
lcfrlem30.c	⊢ 𝐶 = ((𝐽‘𝑋) − (((𝐹‘((𝐽‘𝑌)‘𝐼))(._r‘𝑆)((𝐽‘𝑋)‘𝐼))( ·_𝑠 ‘𝐷)(𝐽‘𝑌)))

**Assertion**
Ref	Expression
lcfrlem35	⊢ (𝜑 → ( ⊥ ‘{(𝑋 + 𝑌)}) = (𝐿‘𝐶))

Distinct variable groups: 𝑣,𝑘,𝑤,𝑥, ⊥ + ,𝑘,𝑣,𝑤,𝑥 𝑅,𝑘,𝑣,𝑥 𝑆,𝑘 · ,𝑘,𝑣,𝑤,𝑥 𝑣,𝑉,𝑥 𝑘,𝑋,𝑣,𝑤,𝑥 𝑘,𝑌,𝑣,𝑤,𝑥 𝑥, 0 Allowed substitution hints: 𝜑(𝑥,𝑤,𝑣,𝑘) 𝐴(𝑥,𝑤,𝑣,𝑘) 𝐵(𝑥,𝑤,𝑣,𝑘) 𝐶(𝑥,𝑤,𝑣,𝑘) 𝐷(𝑥,𝑤,𝑣,𝑘) 𝑄(𝑥,𝑤,𝑣,𝑘) 𝑅(𝑤) 𝑆(𝑥,𝑤,𝑣) 𝑈(𝑥,𝑤,𝑣,𝑘) 𝐹(𝑥,𝑤,𝑣,𝑘) 𝐻(𝑥,𝑤,𝑣,𝑘) 𝐼(𝑥,𝑤,𝑣,𝑘) 𝐽(𝑥,𝑤,𝑣,𝑘) 𝐾(𝑥,𝑤,𝑣,𝑘) 𝐿(𝑥,𝑤,𝑣,𝑘) − (𝑥,𝑤,𝑣,𝑘) 𝑁(𝑥,𝑤,𝑣,𝑘) 𝑉(𝑤,𝑘) 𝑊(𝑥,𝑤,𝑣,𝑘) 0 (𝑤,𝑣,𝑘)

Proof of Theorem lcfrlem35 Dummy variable 𝑓 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		lcfrlem17.h	. . . 4 ⊢ 𝐻 = (LHyp‘𝐾)
2		lcfrlem17.o	. . . 4 ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)
3		lcfrlem17.u	. . . 4 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
4		lcfrlem17.v	. . . 4 ⊢ 𝑉 = (Base‘𝑈)
5		lcfrlem17.p	. . . 4 ⊢ + = (+_g‘𝑈)
6		lcfrlem17.z	. . . 4 ⊢ 0 = (0_g‘𝑈)
7		lcfrlem17.n	. . . 4 ⊢ 𝑁 = (LSpan‘𝑈)
8		lcfrlem17.a	. . . 4 ⊢ 𝐴 = (LSAtoms‘𝑈)
9		lcfrlem17.k	. . . 4 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
10		lcfrlem17.x	. . . 4 ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))
11		lcfrlem17.y	. . . 4 ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))
12		lcfrlem17.ne	. . . 4 ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))
13		lcfrlem22.b	. . . 4 ⊢ 𝐵 = ((𝑁‘{𝑋, 𝑌}) ∩ ( ⊥ ‘{(𝑋 + 𝑌)}))
14		eqid 2609	. . . 4 ⊢ (LSSum‘𝑈) = (LSSum‘𝑈)
15	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14	lcfrlem23 35655	. . 3 ⊢ (𝜑 → (( ⊥ ‘{𝑋, 𝑌})(LSSum‘𝑈)𝐵) = ( ⊥ ‘{(𝑋 + 𝑌)}))
16		lcfrlem24.t	. . . . . 6 ⊢ · = ( ·_𝑠 ‘𝑈)
17		lcfrlem24.s	. . . . . 6 ⊢ 𝑆 = (Scalar‘𝑈)
18		lcfrlem24.q	. . . . . 6 ⊢ 𝑄 = (0_g‘𝑆)
19		lcfrlem24.r	. . . . . 6 ⊢ 𝑅 = (Base‘𝑆)
20		lcfrlem24.j	. . . . . 6 ⊢ 𝐽 = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑣 ∈ 𝑉 ↦ (℩𝑘 ∈ 𝑅 ∃𝑤 ∈ ( ⊥ ‘{𝑥})𝑣 = (𝑤 + (𝑘 · 𝑥)))))
21		lcfrlem24.ib	. . . . . 6 ⊢ (𝜑 → 𝐼 ∈ 𝐵)
22		lcfrlem24.l	. . . . . 6 ⊢ 𝐿 = (LKer‘𝑈)
23	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 16, 17, 18, 19, 20, 21, 22	lcfrlem24 35656	. . . . 5 ⊢ (𝜑 → ( ⊥ ‘{𝑋, 𝑌}) = ((𝐿‘(𝐽‘𝑋)) ∩ (𝐿‘(𝐽‘𝑌))))
24		eqid 2609	. . . . . 6 ⊢ (._r‘𝑆) = (._r‘𝑆)
25		lcfrlem29.i	. . . . . 6 ⊢ 𝐹 = (inv_r‘𝑆)
26		eqid 2609	. . . . . 6 ⊢ (LFnl‘𝑈) = (LFnl‘𝑈)
27		lcfrlem25.d	. . . . . 6 ⊢ 𝐷 = (LDual‘𝑈)
28		eqid 2609	. . . . . 6 ⊢ ( ·_𝑠 ‘𝐷) = ( ·_𝑠 ‘𝐷)
29		lcfrlem30.m	. . . . . 6 ⊢ − = (-_g‘𝐷)
30	1, 3, 9	dvhlvec 35199	. . . . . 6 ⊢ (𝜑 → 𝑈 ∈ LVec)
31		eqid 2609	. . . . . . 7 ⊢ (0_g‘𝐷) = (0_g‘𝐷)
32		eqid 2609	. . . . . . 7 ⊢ {𝑓 ∈ (LFnl‘𝑈) ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} = {𝑓 ∈ (LFnl‘𝑈) ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)}
33	1, 2, 3, 4, 5, 16, 17, 19, 6, 26, 22, 27, 31, 32, 20, 9, 10	lcfrlem10 35642	. . . . . 6 ⊢ (𝜑 → (𝐽‘𝑋) ∈ (LFnl‘𝑈))
34	1, 2, 3, 4, 5, 16, 17, 19, 6, 26, 22, 27, 31, 32, 20, 9, 11	lcfrlem10 35642	. . . . . 6 ⊢ (𝜑 → (𝐽‘𝑌) ∈ (LFnl‘𝑈))
35		eqid 2609	. . . . . . . 8 ⊢ (LSubSp‘𝑈) = (LSubSp‘𝑈)
36	1, 3, 9	dvhlmod 35200	. . . . . . . 8 ⊢ (𝜑 → 𝑈 ∈ LMod)
37	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13	lcfrlem22 35654	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ∈ 𝐴)
38	35, 8, 36, 37	lsatlssel 33085	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ (LSubSp‘𝑈))
39	4, 35	lssel 18707	. . . . . . 7 ⊢ ((𝐵 ∈ (LSubSp‘𝑈) ∧ 𝐼 ∈ 𝐵) → 𝐼 ∈ 𝑉)
40	38, 21, 39	syl2anc 690	. . . . . 6 ⊢ (𝜑 → 𝐼 ∈ 𝑉)
41		lcfrlem28.jn	. . . . . 6 ⊢ (𝜑 → ((𝐽‘𝑌)‘𝐼) ≠ 𝑄)
42		lcfrlem30.c	. . . . . 6 ⊢ 𝐶 = ((𝐽‘𝑋) − (((𝐹‘((𝐽‘𝑌)‘𝐼))(._r‘𝑆)((𝐽‘𝑋)‘𝐼))( ·_𝑠 ‘𝐷)(𝐽‘𝑌)))
43	4, 17, 24, 18, 25, 26, 27, 28, 29, 30, 33, 34, 40, 41, 42, 22	lcfrlem2 35633	. . . . 5 ⊢ (𝜑 → ((𝐿‘(𝐽‘𝑋)) ∩ (𝐿‘(𝐽‘𝑌))) ⊆ (𝐿‘𝐶))
44	23, 43	eqsstrd 3601	. . . 4 ⊢ (𝜑 → ( ⊥ ‘{𝑋, 𝑌}) ⊆ (𝐿‘𝐶))
45	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 16, 17, 18, 19, 20, 21, 22, 27, 41	lcfrlem28 35660	. . . . . 6 ⊢ (𝜑 → 𝐼 ≠ 0 )
46	6, 7, 8, 30, 37, 21, 45	lsatel 33093	. . . . 5 ⊢ (𝜑 → 𝐵 = (𝑁‘{𝐼}))
47	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 16, 17, 18, 19, 20, 21, 22, 27, 41, 25, 29, 42	lcfrlem30 35662	. . . . . . 7 ⊢ (𝜑 → 𝐶 ∈ (LFnl‘𝑈))
48	26, 22, 35	lkrlss 33183	. . . . . . 7 ⊢ ((𝑈 ∈ LMod ∧ 𝐶 ∈ (LFnl‘𝑈)) → (𝐿‘𝐶) ∈ (LSubSp‘𝑈))
49	36, 47, 48	syl2anc 690	. . . . . 6 ⊢ (𝜑 → (𝐿‘𝐶) ∈ (LSubSp‘𝑈))
50	4, 17, 24, 18, 25, 26, 27, 28, 29, 30, 33, 34, 40, 41, 42, 22	lcfrlem3 35634	. . . . . 6 ⊢ (𝜑 → 𝐼 ∈ (𝐿‘𝐶))
51	35, 7, 36, 49, 50	lspsnel5a 18765	. . . . 5 ⊢ (𝜑 → (𝑁‘{𝐼}) ⊆ (𝐿‘𝐶))
52	46, 51	eqsstrd 3601	. . . 4 ⊢ (𝜑 → 𝐵 ⊆ (𝐿‘𝐶))
53	35	lsssssubg 18727	. . . . . . 7 ⊢ (𝑈 ∈ LMod → (LSubSp‘𝑈) ⊆ (SubGrp‘𝑈))
54	36, 53	syl 17	. . . . . 6 ⊢ (𝜑 → (LSubSp‘𝑈) ⊆ (SubGrp‘𝑈))
55	10	eldifad 3551	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
56	11	eldifad 3551	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ∈ 𝑉)
57		prssi 4292	. . . . . . . 8 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → {𝑋, 𝑌} ⊆ 𝑉)
58	55, 56, 57	syl2anc 690	. . . . . . 7 ⊢ (𝜑 → {𝑋, 𝑌} ⊆ 𝑉)
59	1, 3, 4, 35, 2	dochlss 35444	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ {𝑋, 𝑌} ⊆ 𝑉) → ( ⊥ ‘{𝑋, 𝑌}) ∈ (LSubSp‘𝑈))
60	9, 58, 59	syl2anc 690	. . . . . 6 ⊢ (𝜑 → ( ⊥ ‘{𝑋, 𝑌}) ∈ (LSubSp‘𝑈))
61	54, 60	sseldd 3568	. . . . 5 ⊢ (𝜑 → ( ⊥ ‘{𝑋, 𝑌}) ∈ (SubGrp‘𝑈))
62	54, 38	sseldd 3568	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ (SubGrp‘𝑈))
63	54, 49	sseldd 3568	. . . . 5 ⊢ (𝜑 → (𝐿‘𝐶) ∈ (SubGrp‘𝑈))
64	14	lsmlub 17849	. . . . 5 ⊢ ((( ⊥ ‘{𝑋, 𝑌}) ∈ (SubGrp‘𝑈) ∧ 𝐵 ∈ (SubGrp‘𝑈) ∧ (𝐿‘𝐶) ∈ (SubGrp‘𝑈)) → ((( ⊥ ‘{𝑋, 𝑌}) ⊆ (𝐿‘𝐶) ∧ 𝐵 ⊆ (𝐿‘𝐶)) ↔ (( ⊥ ‘{𝑋, 𝑌})(LSSum‘𝑈)𝐵) ⊆ (𝐿‘𝐶)))
65	61, 62, 63, 64	syl3anc 1317	. . . 4 ⊢ (𝜑 → ((( ⊥ ‘{𝑋, 𝑌}) ⊆ (𝐿‘𝐶) ∧ 𝐵 ⊆ (𝐿‘𝐶)) ↔ (( ⊥ ‘{𝑋, 𝑌})(LSSum‘𝑈)𝐵) ⊆ (𝐿‘𝐶)))
66	44, 52, 65	mpbi2and 957	. . 3 ⊢ (𝜑 → (( ⊥ ‘{𝑋, 𝑌})(LSSum‘𝑈)𝐵) ⊆ (𝐿‘𝐶))
67	15, 66	eqsstr3d 3602	. 2 ⊢ (𝜑 → ( ⊥ ‘{(𝑋 + 𝑌)}) ⊆ (𝐿‘𝐶))
68		eqid 2609	. . 3 ⊢ (LSHyp‘𝑈) = (LSHyp‘𝑈)
69	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12	lcfrlem17 35649	. . . 4 ⊢ (𝜑 → (𝑋 + 𝑌) ∈ (𝑉 ∖ { 0 }))
70	1, 2, 3, 4, 6, 68, 9, 69	dochsnshp 35543	. . 3 ⊢ (𝜑 → ( ⊥ ‘{(𝑋 + 𝑌)}) ∈ (LSHyp‘𝑈))
71	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 16, 17, 18, 19, 20, 21, 22, 27, 41, 25, 29, 42	lcfrlem34 35666	. . . 4 ⊢ (𝜑 → 𝐶 ≠ (0_g‘𝐷))
72	68, 26, 22, 27, 31, 30, 47	lduallkr3 33250	. . . 4 ⊢ (𝜑 → ((𝐿‘𝐶) ∈ (LSHyp‘𝑈) ↔ 𝐶 ≠ (0_g‘𝐷)))
73	71, 72	mpbird 245	. . 3 ⊢ (𝜑 → (𝐿‘𝐶) ∈ (LSHyp‘𝑈))
74	68, 30, 70, 73	lshpcmp 33076	. 2 ⊢ (𝜑 → (( ⊥ ‘{(𝑋 + 𝑌)}) ⊆ (𝐿‘𝐶) ↔ ( ⊥ ‘{(𝑋 + 𝑌)}) = (𝐿‘𝐶)))
75	67, 74	mpbid 220	1 ⊢ (𝜑 → ( ⊥ ‘{(𝑋 + 𝑌)}) = (𝐿‘𝐶))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 194 ∧ wa 382 = wceq 1474 ∈ wcel 1976 ≠ wne 2779 ∃wrex 2896 {crab 2899 ∖ cdif 3536 ∩ cin 3538 ⊆ wss 3539 {csn 4124 {cpr 4126 ↦ cmpt 4637 ‘cfv 5789 ℩crio 6487 (class class class)co 6526 Basecbs 15643 +_gcplusg 15716 ._rcmulr 15717 Scalarcsca 15719 ·_𝑠 cvsca 15720 0_gc0g 15871 -_gcsg 17195 SubGrpcsubg 17359 LSSumclsm 17820 inv_rcinvr 18442 LModclmod 18634 LSubSpclss 18701 LSpanclspn 18740 LSAtomsclsa 33062 LSHypclsh 33063 LFnlclfn 33145 LKerclk 33173 LDualcld 33211 HLchlt 33438 LHypclh 34071 DVecHcdvh 35168 ocHcoch 35437

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1712 ax-4 1727 ax-5 1826 ax-6 1874 ax-7 1921 ax-8 1978 ax-9 1985 ax-10 2005 ax-11 2020 ax-12 2033 ax-13 2233 ax-ext 2589 ax-rep 4693 ax-sep 4703 ax-nul 4711 ax-pow 4763 ax-pr 4827 ax-un 6824 ax-cnex 9848 ax-resscn 9849 ax-1cn 9850 ax-icn 9851 ax-addcl 9852 ax-addrcl 9853 ax-mulcl 9854 ax-mulrcl 9855 ax-mulcom 9856 ax-addass 9857 ax-mulass 9858 ax-distr 9859 ax-i2m1 9860 ax-1ne0 9861 ax-1rid 9862 ax-rnegex 9863 ax-rrecex 9864 ax-cnre 9865 ax-pre-lttri 9866 ax-pre-lttrn 9867 ax-pre-ltadd 9868 ax-pre-mulgt0 9869 ax-riotaBAD 33040

This theorem depends on definitions: df-bi 195 df-or 383 df-an 384 df-3or 1031 df-3an 1032 df-tru 1477 df-fal 1480 df-ex 1695 df-nf 1700 df-sb 1867 df-eu 2461 df-mo 2462 df-clab 2596 df-cleq 2602 df-clel 2605 df-nfc 2739 df-ne 2781 df-nel 2782 df-ral 2900 df-rex 2901 df-reu 2902 df-rmo 2903 df-rab 2904 df-v 3174 df-sbc 3402 df-csb 3499 df-dif 3542 df-un 3544 df-in 3546 df-ss 3553 df-pss 3555 df-nul 3874 df-if 4036 df-pw 4109 df-sn 4125 df-pr 4127 df-tp 4129 df-op 4131 df-uni 4367 df-int 4405 df-iun 4451 df-iin 4452 df-br 4578 df-opab 4638 df-mpt 4639 df-tr 4675 df-eprel 4938 df-id 4942 df-po 4948 df-so 4949 df-fr 4986 df-we 4988 df-xp 5033 df-rel 5034 df-cnv 5035 df-co 5036 df-dm 5037 df-rn 5038 df-res 5039 df-ima 5040 df-pred 5582 df-ord 5628 df-on 5629 df-lim 5630 df-suc 5631 df-iota 5753 df-fun 5791 df-fn 5792 df-f 5793 df-f1 5794 df-fo 5795 df-f1o 5796 df-fv 5797 df-riota 6488 df-ov 6529 df-oprab 6530 df-mpt2 6531 df-of 6772 df-om 6935 df-1st 7036 df-2nd 7037 df-tpos 7216 df-undef 7263 df-wrecs 7271 df-recs 7332 df-rdg 7370 df-1o 7424 df-oadd 7428 df-er 7606 df-map 7723 df-en 7819 df-dom 7820 df-sdom 7821 df-fin 7822 df-pnf 9932 df-mnf 9933 df-xr 9934 df-ltxr 9935 df-le 9936 df-sub 10119 df-neg 10120 df-nn 10870 df-2 10928 df-3 10929 df-4 10930 df-5 10931 df-6 10932 df-n0 11142 df-z 11213 df-uz 11522 df-fz 12155 df-struct 15645 df-ndx 15646 df-slot 15647 df-base 15648 df-sets 15649 df-ress 15650 df-plusg 15729 df-mulr 15730 df-sca 15732 df-vsca 15733 df-0g 15873 df-mre 16017 df-mrc 16018 df-acs 16020 df-preset 16699 df-poset 16717 df-plt 16729 df-lub 16745 df-glb 16746 df-join 16747 df-meet 16748 df-p0 16810 df-p1 16811 df-lat 16817 df-clat 16879 df-mgm 17013 df-sgrp 17055 df-mnd 17066 df-submnd 17107 df-grp 17196 df-minusg 17197 df-sbg 17198 df-subg 17362 df-cntz 17521 df-oppg 17547 df-lsm 17822 df-cmn 17966 df-abl 17967 df-mgp 18261 df-ur 18273 df-ring 18320 df-oppr 18394 df-dvdsr 18412 df-unit 18413 df-invr 18443 df-dvr 18454 df-drng 18520 df-lmod 18636 df-lss 18702 df-lsp 18741 df-lvec 18872 df-lsatoms 33064 df-lshyp 33065 df-lcv 33107 df-lfl 33146 df-lkr 33174 df-ldual 33212 df-oposet 33264 df-ol 33266 df-oml 33267 df-covers 33354 df-ats 33355 df-atl 33386 df-cvlat 33410 df-hlat 33439 df-llines 33585 df-lplanes 33586 df-lvols 33587 df-lines 33588 df-psubsp 33590 df-pmap 33591 df-padd 33883 df-lhyp 34075 df-laut 34076 df-ldil 34191 df-ltrn 34192 df-trl 34247 df-tgrp 34832 df-tendo 34844 df-edring 34846 df-dveca 35092 df-disoa 35119 df-dvech 35169 df-dib 35229 df-dic 35263 df-dih 35319 df-doch 35438 df-djh 35485

This theorem is referenced by: lcfrlem36 35668

W3C validator