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 38158

Description: Lemma for lcfr 38166. (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 2772	. . . 4 ⊢ (LSSum‘𝑈) = (LSSum‘𝑈)
15	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14	lcfrlem23 38146	. . 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 38147	. . . . 5 ⊢ (𝜑 → ( ⊥ ‘{𝑋, 𝑌}) = ((𝐿‘(𝐽‘𝑋)) ∩ (𝐿‘(𝐽‘𝑌))))
24		eqid 2772	. . . . . 6 ⊢ (._r‘𝑆) = (._r‘𝑆)
25		lcfrlem29.i	. . . . . 6 ⊢ 𝐹 = (inv_r‘𝑆)
26		eqid 2772	. . . . . 6 ⊢ (LFnl‘𝑈) = (LFnl‘𝑈)
27		lcfrlem25.d	. . . . . 6 ⊢ 𝐷 = (LDual‘𝑈)
28		eqid 2772	. . . . . 6 ⊢ ( ·_𝑠 ‘𝐷) = ( ·_𝑠 ‘𝐷)
29		lcfrlem30.m	. . . . . 6 ⊢ − = (-_g‘𝐷)
30	1, 3, 9	dvhlvec 37690	. . . . . 6 ⊢ (𝜑 → 𝑈 ∈ LVec)
31		eqid 2772	. . . . . . 7 ⊢ (0_g‘𝐷) = (0_g‘𝐷)
32		eqid 2772	. . . . . . 7 ⊢ {𝑓 ∈ (LFnl‘𝑈) ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} = {𝑓 ∈ (LFnl‘𝑈) ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)}
33	1, 2, 3, 4, 5, 16, 17, 19, 6, 26, 22, 27, 31, 32, 20, 9, 10	lcfrlem10 38133	. . . . . 6 ⊢ (𝜑 → (𝐽‘𝑋) ∈ (LFnl‘𝑈))
34	1, 2, 3, 4, 5, 16, 17, 19, 6, 26, 22, 27, 31, 32, 20, 9, 11	lcfrlem10 38133	. . . . . 6 ⊢ (𝜑 → (𝐽‘𝑌) ∈ (LFnl‘𝑈))
35		eqid 2772	. . . . . . . 8 ⊢ (LSubSp‘𝑈) = (LSubSp‘𝑈)
36	1, 3, 9	dvhlmod 37691	. . . . . . . 8 ⊢ (𝜑 → 𝑈 ∈ LMod)
37	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13	lcfrlem22 38145	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ∈ 𝐴)
38	35, 8, 36, 37	lsatlssel 35578	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ (LSubSp‘𝑈))
39	4, 35	lssel 19425	. . . . . . 7 ⊢ ((𝐵 ∈ (LSubSp‘𝑈) ∧ 𝐼 ∈ 𝐵) → 𝐼 ∈ 𝑉)
40	38, 21, 39	syl2anc 576	. . . . . 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 38124	. . . . 5 ⊢ (𝜑 → ((𝐿‘(𝐽‘𝑋)) ∩ (𝐿‘(𝐽‘𝑌))) ⊆ (𝐿‘𝐶))
44	23, 43	eqsstrd 3889	. . . 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 38151	. . . . . 6 ⊢ (𝜑 → 𝐼 ≠ 0 )
46	6, 7, 8, 30, 37, 21, 45	lsatel 35586	. . . . 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 38153	. . . . . . 7 ⊢ (𝜑 → 𝐶 ∈ (LFnl‘𝑈))
48	26, 22, 35	lkrlss 35676	. . . . . . 7 ⊢ ((𝑈 ∈ LMod ∧ 𝐶 ∈ (LFnl‘𝑈)) → (𝐿‘𝐶) ∈ (LSubSp‘𝑈))
49	36, 47, 48	syl2anc 576	. . . . . 6 ⊢ (𝜑 → (𝐿‘𝐶) ∈ (LSubSp‘𝑈))
50	4, 17, 24, 18, 25, 26, 27, 28, 29, 30, 33, 34, 40, 41, 42, 22	lcfrlem3 38125	. . . . . 6 ⊢ (𝜑 → 𝐼 ∈ (𝐿‘𝐶))
51	35, 7, 36, 49, 50	lspsnel5a 19484	. . . . 5 ⊢ (𝜑 → (𝑁‘{𝐼}) ⊆ (𝐿‘𝐶))
52	46, 51	eqsstrd 3889	. . . 4 ⊢ (𝜑 → 𝐵 ⊆ (𝐿‘𝐶))
53	35	lsssssubg 19446	. . . . . . 7 ⊢ (𝑈 ∈ LMod → (LSubSp‘𝑈) ⊆ (SubGrp‘𝑈))
54	36, 53	syl 17	. . . . . 6 ⊢ (𝜑 → (LSubSp‘𝑈) ⊆ (SubGrp‘𝑈))
55	10	eldifad 3835	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
56	11	eldifad 3835	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ∈ 𝑉)
57		prssi 4622	. . . . . . . 8 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → {𝑋, 𝑌} ⊆ 𝑉)
58	55, 56, 57	syl2anc 576	. . . . . . 7 ⊢ (𝜑 → {𝑋, 𝑌} ⊆ 𝑉)
59	1, 3, 4, 35, 2	dochlss 37935	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ {𝑋, 𝑌} ⊆ 𝑉) → ( ⊥ ‘{𝑋, 𝑌}) ∈ (LSubSp‘𝑈))
60	9, 58, 59	syl2anc 576	. . . . . 6 ⊢ (𝜑 → ( ⊥ ‘{𝑋, 𝑌}) ∈ (LSubSp‘𝑈))
61	54, 60	sseldd 3853	. . . . 5 ⊢ (𝜑 → ( ⊥ ‘{𝑋, 𝑌}) ∈ (SubGrp‘𝑈))
62	54, 38	sseldd 3853	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ (SubGrp‘𝑈))
63	54, 49	sseldd 3853	. . . . 5 ⊢ (𝜑 → (𝐿‘𝐶) ∈ (SubGrp‘𝑈))
64	14	lsmlub 18543	. . . . 5 ⊢ ((( ⊥ ‘{𝑋, 𝑌}) ∈ (SubGrp‘𝑈) ∧ 𝐵 ∈ (SubGrp‘𝑈) ∧ (𝐿‘𝐶) ∈ (SubGrp‘𝑈)) → ((( ⊥ ‘{𝑋, 𝑌}) ⊆ (𝐿‘𝐶) ∧ 𝐵 ⊆ (𝐿‘𝐶)) ↔ (( ⊥ ‘{𝑋, 𝑌})(LSSum‘𝑈)𝐵) ⊆ (𝐿‘𝐶)))
65	61, 62, 63, 64	syl3anc 1351	. . . 4 ⊢ (𝜑 → ((( ⊥ ‘{𝑋, 𝑌}) ⊆ (𝐿‘𝐶) ∧ 𝐵 ⊆ (𝐿‘𝐶)) ↔ (( ⊥ ‘{𝑋, 𝑌})(LSSum‘𝑈)𝐵) ⊆ (𝐿‘𝐶)))
66	44, 52, 65	mpbi2and 699	. . 3 ⊢ (𝜑 → (( ⊥ ‘{𝑋, 𝑌})(LSSum‘𝑈)𝐵) ⊆ (𝐿‘𝐶))
67	15, 66	eqsstr3d 3890	. 2 ⊢ (𝜑 → ( ⊥ ‘{(𝑋 + 𝑌)}) ⊆ (𝐿‘𝐶))
68		eqid 2772	. . 3 ⊢ (LSHyp‘𝑈) = (LSHyp‘𝑈)
69	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12	lcfrlem17 38140	. . . 4 ⊢ (𝜑 → (𝑋 + 𝑌) ∈ (𝑉 ∖ { 0 }))
70	1, 2, 3, 4, 6, 68, 9, 69	dochsnshp 38034	. . 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 38157	. . . 4 ⊢ (𝜑 → 𝐶 ≠ (0_g‘𝐷))
72	68, 26, 22, 27, 31, 30, 47	lduallkr3 35743	. . . 4 ⊢ (𝜑 → ((𝐿‘𝐶) ∈ (LSHyp‘𝑈) ↔ 𝐶 ≠ (0_g‘𝐷)))
73	71, 72	mpbird 249	. . 3 ⊢ (𝜑 → (𝐿‘𝐶) ∈ (LSHyp‘𝑈))
74	68, 30, 70, 73	lshpcmp 35569	. 2 ⊢ (𝜑 → (( ⊥ ‘{(𝑋 + 𝑌)}) ⊆ (𝐿‘𝐶) ↔ ( ⊥ ‘{(𝑋 + 𝑌)}) = (𝐿‘𝐶)))
75	67, 74	mpbid 224	1 ⊢ (𝜑 → ( ⊥ ‘{(𝑋 + 𝑌)}) = (𝐿‘𝐶))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 198 ∧ wa 387 = wceq 1507 ∈ wcel 2050 ≠ wne 2961 ∃wrex 3083 {crab 3086 ∖ cdif 3820 ∩ cin 3822 ⊆ wss 3823 {csn 4435 {cpr 4437 ↦ cmpt 5002 ‘cfv 6182 ℩crio 6930 (class class class)co 6970 Basecbs 16333 +_gcplusg 16415 ._rcmulr 16416 Scalarcsca 16418 ·_𝑠 cvsca 16419 0_gc0g 16563 -_gcsg 17887 SubGrpcsubg 18051 LSSumclsm 18514 inv_rcinvr 19138 LModclmod 19350 LSubSpclss 19419 LSpanclspn 19459 LSAtomsclsa 35555 LSHypclsh 35556 LFnlclfn 35638 LKerclk 35666 LDualcld 35704 HLchlt 35931 LHypclh 36565 DVecHcdvh 37659 ocHcoch 37928

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1758 ax-4 1772 ax-5 1869 ax-6 1928 ax-7 1965 ax-8 2052 ax-9 2059 ax-10 2079 ax-11 2093 ax-12 2106 ax-13 2301 ax-ext 2744 ax-rep 5043 ax-sep 5054 ax-nul 5061 ax-pow 5113 ax-pr 5180 ax-un 7273 ax-cnex 10385 ax-resscn 10386 ax-1cn 10387 ax-icn 10388 ax-addcl 10389 ax-addrcl 10390 ax-mulcl 10391 ax-mulrcl 10392 ax-mulcom 10393 ax-addass 10394 ax-mulass 10395 ax-distr 10396 ax-i2m1 10397 ax-1ne0 10398 ax-1rid 10399 ax-rnegex 10400 ax-rrecex 10401 ax-cnre 10402 ax-pre-lttri 10403 ax-pre-lttrn 10404 ax-pre-ltadd 10405 ax-pre-mulgt0 10406 ax-riotaBAD 35534

This theorem depends on definitions: df-bi 199 df-an 388 df-or 834 df-3or 1069 df-3an 1070 df-tru 1510 df-fal 1520 df-ex 1743 df-nf 1747 df-sb 2016 df-mo 2547 df-eu 2584 df-clab 2753 df-cleq 2765 df-clel 2840 df-nfc 2912 df-ne 2962 df-nel 3068 df-ral 3087 df-rex 3088 df-reu 3089 df-rmo 3090 df-rab 3091 df-v 3411 df-sbc 3676 df-csb 3781 df-dif 3826 df-un 3828 df-in 3830 df-ss 3837 df-pss 3839 df-nul 4173 df-if 4345 df-pw 4418 df-sn 4436 df-pr 4438 df-tp 4440 df-op 4442 df-uni 4707 df-int 4744 df-iun 4788 df-iin 4789 df-br 4924 df-opab 4986 df-mpt 5003 df-tr 5025 df-id 5306 df-eprel 5311 df-po 5320 df-so 5321 df-fr 5360 df-we 5362 df-xp 5407 df-rel 5408 df-cnv 5409 df-co 5410 df-dm 5411 df-rn 5412 df-res 5413 df-ima 5414 df-pred 5980 df-ord 6026 df-on 6027 df-lim 6028 df-suc 6029 df-iota 6146 df-fun 6184 df-fn 6185 df-f 6186 df-f1 6187 df-fo 6188 df-f1o 6189 df-fv 6190 df-riota 6931 df-ov 6973 df-oprab 6974 df-mpo 6975 df-of 7221 df-om 7391 df-1st 7495 df-2nd 7496 df-tpos 7689 df-undef 7736 df-wrecs 7744 df-recs 7806 df-rdg 7844 df-1o 7899 df-oadd 7903 df-er 8083 df-map 8202 df-en 8301 df-dom 8302 df-sdom 8303 df-fin 8304 df-pnf 10470 df-mnf 10471 df-xr 10472 df-ltxr 10473 df-le 10474 df-sub 10666 df-neg 10667 df-nn 11434 df-2 11497 df-3 11498 df-4 11499 df-5 11500 df-6 11501 df-n0 11702 df-z 11788 df-uz 12053 df-fz 12703 df-struct 16335 df-ndx 16336 df-slot 16337 df-base 16339 df-sets 16340 df-ress 16341 df-plusg 16428 df-mulr 16429 df-sca 16431 df-vsca 16432 df-0g 16565 df-mre 16709 df-mrc 16710 df-acs 16712 df-proset 17390 df-poset 17408 df-plt 17420 df-lub 17436 df-glb 17437 df-join 17438 df-meet 17439 df-p0 17501 df-p1 17502 df-lat 17508 df-clat 17570 df-mgm 17704 df-sgrp 17746 df-mnd 17757 df-submnd 17798 df-grp 17888 df-minusg 17889 df-sbg 17890 df-subg 18054 df-cntz 18212 df-oppg 18239 df-lsm 18516 df-cmn 18662 df-abl 18663 df-mgp 18957 df-ur 18969 df-ring 19016 df-oppr 19090 df-dvdsr 19108 df-unit 19109 df-invr 19139 df-dvr 19150 df-drng 19221 df-lmod 19352 df-lss 19420 df-lsp 19460 df-lvec 19591 df-lsatoms 35557 df-lshyp 35558 df-lcv 35600 df-lfl 35639 df-lkr 35667 df-ldual 35705 df-oposet 35757 df-ol 35759 df-oml 35760 df-covers 35847 df-ats 35848 df-atl 35879 df-cvlat 35903 df-hlat 35932 df-llines 36079 df-lplanes 36080 df-lvols 36081 df-lines 36082 df-psubsp 36084 df-pmap 36085 df-padd 36377 df-lhyp 36569 df-laut 36570 df-ldil 36685 df-ltrn 36686 df-trl 36740 df-tgrp 37324 df-tendo 37336 df-edring 37338 df-dveca 37584 df-disoa 37610 df-dvech 37660 df-dib 37720 df-dic 37754 df-dih 37810 df-doch 37929 df-djh 37976

This theorem is referenced by: lcfrlem36 38159

W3C validator