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 41361

Description: Lemma for lcfr 41369. (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 2729	. . . 4 ⊢ (LSSum‘𝑈) = (LSSum‘𝑈)
15	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14	lcfrlem23 41349	. . 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 41350	. . . . 5 ⊢ (𝜑 → ( ⊥ ‘{𝑋, 𝑌}) = ((𝐿‘(𝐽‘𝑋)) ∩ (𝐿‘(𝐽‘𝑌))))
24		eqid 2729	. . . . . 6 ⊢ (._r‘𝑆) = (._r‘𝑆)
25		lcfrlem29.i	. . . . . 6 ⊢ 𝐹 = (inv_r‘𝑆)
26		eqid 2729	. . . . . 6 ⊢ (LFnl‘𝑈) = (LFnl‘𝑈)
27		lcfrlem25.d	. . . . . 6 ⊢ 𝐷 = (LDual‘𝑈)
28		eqid 2729	. . . . . 6 ⊢ ( ·_𝑠 ‘𝐷) = ( ·_𝑠 ‘𝐷)
29		lcfrlem30.m	. . . . . 6 ⊢ − = (-_g‘𝐷)
30	1, 3, 9	dvhlvec 40893	. . . . . 6 ⊢ (𝜑 → 𝑈 ∈ LVec)
31		eqid 2729	. . . . . . 7 ⊢ (0_g‘𝐷) = (0_g‘𝐷)
32		eqid 2729	. . . . . . 7 ⊢ {𝑓 ∈ (LFnl‘𝑈) ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)} = {𝑓 ∈ (LFnl‘𝑈) ∣ ( ⊥ ‘( ⊥ ‘(𝐿‘𝑓))) = (𝐿‘𝑓)}
33	1, 2, 3, 4, 5, 16, 17, 19, 6, 26, 22, 27, 31, 32, 20, 9, 10	lcfrlem10 41336	. . . . . 6 ⊢ (𝜑 → (𝐽‘𝑋) ∈ (LFnl‘𝑈))
34	1, 2, 3, 4, 5, 16, 17, 19, 6, 26, 22, 27, 31, 32, 20, 9, 11	lcfrlem10 41336	. . . . . 6 ⊢ (𝜑 → (𝐽‘𝑌) ∈ (LFnl‘𝑈))
35		eqid 2729	. . . . . . . 8 ⊢ (LSubSp‘𝑈) = (LSubSp‘𝑈)
36	1, 3, 9	dvhlmod 40894	. . . . . . . 8 ⊢ (𝜑 → 𝑈 ∈ LMod)
37	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13	lcfrlem22 41348	. . . . . . . 8 ⊢ (𝜑 → 𝐵 ∈ 𝐴)
38	35, 8, 36, 37	lsatlssel 38780	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ (LSubSp‘𝑈))
39	4, 35	lssel 20926	. . . . . . 7 ⊢ ((𝐵 ∈ (LSubSp‘𝑈) ∧ 𝐼 ∈ 𝐵) → 𝐼 ∈ 𝑉)
40	38, 21, 39	syl2anc 582	. . . . . 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 41327	. . . . 5 ⊢ (𝜑 → ((𝐿‘(𝐽‘𝑋)) ∩ (𝐿‘(𝐽‘𝑌))) ⊆ (𝐿‘𝐶))
44	23, 43	eqsstrd 4029	. . . 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 41354	. . . . . 6 ⊢ (𝜑 → 𝐼 ≠ 0 )
46	6, 7, 8, 30, 37, 21, 45	lsatel 38788	. . . . 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 41356	. . . . . . 7 ⊢ (𝜑 → 𝐶 ∈ (LFnl‘𝑈))
48	26, 22, 35	lkrlss 38878	. . . . . . 7 ⊢ ((𝑈 ∈ LMod ∧ 𝐶 ∈ (LFnl‘𝑈)) → (𝐿‘𝐶) ∈ (LSubSp‘𝑈))
49	36, 47, 48	syl2anc 582	. . . . . 6 ⊢ (𝜑 → (𝐿‘𝐶) ∈ (LSubSp‘𝑈))
50	4, 17, 24, 18, 25, 26, 27, 28, 29, 30, 33, 34, 40, 41, 42, 22	lcfrlem3 41328	. . . . . 6 ⊢ (𝜑 → 𝐼 ∈ (𝐿‘𝐶))
51	35, 7, 36, 49, 50	ellspsn5 20985	. . . . 5 ⊢ (𝜑 → (𝑁‘{𝐼}) ⊆ (𝐿‘𝐶))
52	46, 51	eqsstrd 4029	. . . 4 ⊢ (𝜑 → 𝐵 ⊆ (𝐿‘𝐶))
53	35	lsssssubg 20947	. . . . . . 7 ⊢ (𝑈 ∈ LMod → (LSubSp‘𝑈) ⊆ (SubGrp‘𝑈))
54	36, 53	syl 17	. . . . . 6 ⊢ (𝜑 → (LSubSp‘𝑈) ⊆ (SubGrp‘𝑈))
55	10	eldifad 3970	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
56	11	eldifad 3970	. . . . . . . 8 ⊢ (𝜑 → 𝑌 ∈ 𝑉)
57		prssi 4831	. . . . . . . 8 ⊢ ((𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → {𝑋, 𝑌} ⊆ 𝑉)
58	55, 56, 57	syl2anc 582	. . . . . . 7 ⊢ (𝜑 → {𝑋, 𝑌} ⊆ 𝑉)
59	1, 3, 4, 35, 2	dochlss 41138	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ {𝑋, 𝑌} ⊆ 𝑉) → ( ⊥ ‘{𝑋, 𝑌}) ∈ (LSubSp‘𝑈))
60	9, 58, 59	syl2anc 582	. . . . . 6 ⊢ (𝜑 → ( ⊥ ‘{𝑋, 𝑌}) ∈ (LSubSp‘𝑈))
61	54, 60	sseldd 3991	. . . . 5 ⊢ (𝜑 → ( ⊥ ‘{𝑋, 𝑌}) ∈ (SubGrp‘𝑈))
62	54, 38	sseldd 3991	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ (SubGrp‘𝑈))
63	54, 49	sseldd 3991	. . . . 5 ⊢ (𝜑 → (𝐿‘𝐶) ∈ (SubGrp‘𝑈))
64	14	lsmlub 19674	. . . . 5 ⊢ ((( ⊥ ‘{𝑋, 𝑌}) ∈ (SubGrp‘𝑈) ∧ 𝐵 ∈ (SubGrp‘𝑈) ∧ (𝐿‘𝐶) ∈ (SubGrp‘𝑈)) → ((( ⊥ ‘{𝑋, 𝑌}) ⊆ (𝐿‘𝐶) ∧ 𝐵 ⊆ (𝐿‘𝐶)) ↔ (( ⊥ ‘{𝑋, 𝑌})(LSSum‘𝑈)𝐵) ⊆ (𝐿‘𝐶)))
65	61, 62, 63, 64	syl3anc 1368	. . . 4 ⊢ (𝜑 → ((( ⊥ ‘{𝑋, 𝑌}) ⊆ (𝐿‘𝐶) ∧ 𝐵 ⊆ (𝐿‘𝐶)) ↔ (( ⊥ ‘{𝑋, 𝑌})(LSSum‘𝑈)𝐵) ⊆ (𝐿‘𝐶)))
66	44, 52, 65	mpbi2and 710	. . 3 ⊢ (𝜑 → (( ⊥ ‘{𝑋, 𝑌})(LSSum‘𝑈)𝐵) ⊆ (𝐿‘𝐶))
67	15, 66	eqsstrrd 4030	. 2 ⊢ (𝜑 → ( ⊥ ‘{(𝑋 + 𝑌)}) ⊆ (𝐿‘𝐶))
68		eqid 2729	. . 3 ⊢ (LSHyp‘𝑈) = (LSHyp‘𝑈)
69	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12	lcfrlem17 41343	. . . 4 ⊢ (𝜑 → (𝑋 + 𝑌) ∈ (𝑉 ∖ { 0 }))
70	1, 2, 3, 4, 6, 68, 9, 69	dochsnshp 41237	. . 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 41360	. . . 4 ⊢ (𝜑 → 𝐶 ≠ (0_g‘𝐷))
72	68, 26, 22, 27, 31, 30, 47	lduallkr3 38945	. . . 4 ⊢ (𝜑 → ((𝐿‘𝐶) ∈ (LSHyp‘𝑈) ↔ 𝐶 ≠ (0_g‘𝐷)))
73	71, 72	mpbird 256	. . 3 ⊢ (𝜑 → (𝐿‘𝐶) ∈ (LSHyp‘𝑈))
74	68, 30, 70, 73	lshpcmp 38771	. 2 ⊢ (𝜑 → (( ⊥ ‘{(𝑋 + 𝑌)}) ⊆ (𝐿‘𝐶) ↔ ( ⊥ ‘{(𝑋 + 𝑌)}) = (𝐿‘𝐶)))
75	67, 74	mpbid 231	1 ⊢ (𝜑 → ( ⊥ ‘{(𝑋 + 𝑌)}) = (𝐿‘𝐶))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 = wceq 1534 ∈ wcel 2100 ≠ wne 2933 ∃wrex 3063 {crab 3428 ∖ cdif 3955 ∩ cin 3957 ⊆ wss 3958 {csn 4634 {cpr 4636 ↦ cmpt 5237 ‘cfv 6556 ℩crio 7382 (class class class)co 7427 Basecbs 17226 +_gcplusg 17279 ._rcmulr 17280 Scalarcsca 17282 ·_𝑠 cvsca 17283 0_gc0g 17467 -_gcsg 18943 SubGrpcsubg 19128 LSSumclsm 19644 inv_rcinvr 20381 LModclmod 20848 LSubSpclss 20920 LSpanclspn 20960 LSAtomsclsa 38757 LSHypclsh 38758 LFnlclfn 38840 LKerclk 38868 LDualcld 38906 HLchlt 39133 LHypclh 39768 DVecHcdvh 40862 ocHcoch 41131

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2102 ax-9 2110 ax-10 2133 ax-11 2150 ax-12 2170 ax-ext 2700 ax-rep 5291 ax-sep 5305 ax-nul 5312 ax-pow 5371 ax-pr 5435 ax-un 7748 ax-cnex 11215 ax-resscn 11216 ax-1cn 11217 ax-icn 11218 ax-addcl 11219 ax-addrcl 11220 ax-mulcl 11221 ax-mulrcl 11222 ax-mulcom 11223 ax-addass 11224 ax-mulass 11225 ax-distr 11226 ax-i2m1 11227 ax-1ne0 11228 ax-1rid 11229 ax-rnegex 11230 ax-rrecex 11231 ax-cnre 11232 ax-pre-lttri 11233 ax-pre-lttrn 11234 ax-pre-ltadd 11235 ax-pre-mulgt0 11236 ax-riotaBAD 38736

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2062 df-mo 2532 df-eu 2561 df-clab 2707 df-cleq 2721 df-clel 2806 df-nfc 2881 df-ne 2934 df-nel 3040 df-ral 3055 df-rex 3064 df-rmo 3373 df-reu 3374 df-rab 3429 df-v 3474 df-sbc 3788 df-csb 3904 df-dif 3961 df-un 3963 df-in 3965 df-ss 3975 df-pss 3978 df-nul 4334 df-if 4535 df-pw 4610 df-sn 4635 df-pr 4637 df-tp 4639 df-op 4641 df-uni 4917 df-int 4958 df-iun 5006 df-iin 5007 df-br 5155 df-opab 5217 df-mpt 5238 df-tr 5272 df-id 5582 df-eprel 5588 df-po 5596 df-so 5597 df-fr 5639 df-we 5641 df-xp 5690 df-rel 5691 df-cnv 5692 df-co 5693 df-dm 5694 df-rn 5695 df-res 5696 df-ima 5697 df-pred 6315 df-ord 6381 df-on 6382 df-lim 6383 df-suc 6384 df-iota 6508 df-fun 6558 df-fn 6559 df-f 6560 df-f1 6561 df-fo 6562 df-f1o 6563 df-fv 6564 df-riota 7383 df-ov 7430 df-oprab 7431 df-mpo 7432 df-of 7692 df-om 7882 df-1st 8008 df-2nd 8009 df-tpos 8245 df-undef 8292 df-frecs 8300 df-wrecs 8331 df-recs 8405 df-rdg 8444 df-1o 8500 df-2o 8501 df-er 8738 df-map 8861 df-en 8979 df-dom 8980 df-sdom 8981 df-fin 8982 df-pnf 11301 df-mnf 11302 df-xr 11303 df-ltxr 11304 df-le 11305 df-sub 11497 df-neg 11498 df-nn 12269 df-2 12331 df-3 12332 df-4 12333 df-5 12334 df-6 12335 df-n0 12529 df-z 12615 df-uz 12879 df-fz 13543 df-struct 17162 df-sets 17179 df-slot 17197 df-ndx 17209 df-base 17227 df-ress 17256 df-plusg 17292 df-mulr 17293 df-sca 17295 df-vsca 17296 df-0g 17469 df-mre 17612 df-mrc 17613 df-acs 17615 df-proset 18333 df-poset 18351 df-plt 18368 df-lub 18384 df-glb 18385 df-join 18386 df-meet 18387 df-p0 18463 df-p1 18464 df-lat 18470 df-clat 18537 df-mgm 18646 df-sgrp 18725 df-mnd 18741 df-submnd 18787 df-grp 18944 df-minusg 18945 df-sbg 18946 df-subg 19131 df-cntz 19325 df-oppg 19354 df-lsm 19646 df-cmn 19792 df-abl 19793 df-mgp 20130 df-rng 20148 df-ur 20177 df-ring 20230 df-oppr 20328 df-dvdsr 20351 df-unit 20352 df-invr 20382 df-dvr 20395 df-nzr 20507 df-rlreg 20684 df-domn 20685 df-drng 20721 df-lmod 20850 df-lss 20921 df-lsp 20961 df-lvec 21093 df-lsatoms 38759 df-lshyp 38760 df-lcv 38802 df-lfl 38841 df-lkr 38869 df-ldual 38907 df-oposet 38959 df-ol 38961 df-oml 38962 df-covers 39049 df-ats 39050 df-atl 39081 df-cvlat 39105 df-hlat 39134 df-llines 39282 df-lplanes 39283 df-lvols 39284 df-lines 39285 df-psubsp 39287 df-pmap 39288 df-padd 39580 df-lhyp 39772 df-laut 39773 df-ldil 39888 df-ltrn 39889 df-trl 39943 df-tgrp 40527 df-tendo 40539 df-edring 40541 df-dveca 40787 df-disoa 40813 df-dvech 40863 df-dib 40923 df-dic 40957 df-dih 41013 df-doch 41132 df-djh 41179

This theorem is referenced by: lcfrlem36 41362

W3C validator