lclkrlem2p - Mathbox for Norm Megill

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

Theorem lclkrlem2p 42107

Description: Lemma for lclkr 42118. When 𝐵 is zero, 𝑋 and 𝑌 must colinear, so their orthocomplements must be comparable. (Contributed by NM, 17-Jan-2015.)

**Hypotheses**
Ref	Expression
lclkrlem2m.v	⊢ 𝑉 = (Base‘𝑈)
lclkrlem2m.t	⊢ · = ( ·_𝑠 ‘𝑈)
lclkrlem2m.s	⊢ 𝑆 = (Scalar‘𝑈)
lclkrlem2m.q	⊢ × = (._r‘𝑆)
lclkrlem2m.z	⊢ 0 = (0_g‘𝑆)
lclkrlem2m.i	⊢ 𝐼 = (inv_r‘𝑆)
lclkrlem2m.m	⊢ − = (-_g‘𝑈)
lclkrlem2m.f	⊢ 𝐹 = (LFnl‘𝑈)
lclkrlem2m.d	⊢ 𝐷 = (LDual‘𝑈)
lclkrlem2m.p	⊢ + = (+_g‘𝐷)
lclkrlem2m.x	⊢ (𝜑 → 𝑋 ∈ 𝑉)
lclkrlem2m.y	⊢ (𝜑 → 𝑌 ∈ 𝑉)
lclkrlem2m.e	⊢ (𝜑 → 𝐸 ∈ 𝐹)
lclkrlem2m.g	⊢ (𝜑 → 𝐺 ∈ 𝐹)
lclkrlem2n.n	⊢ 𝑁 = (LSpan‘𝑈)
lclkrlem2n.l	⊢ 𝐿 = (LKer‘𝑈)
lclkrlem2o.h	⊢ 𝐻 = (LHyp‘𝐾)
lclkrlem2o.o	⊢ ⊥ = ((ocH‘𝐾)‘𝑊)
lclkrlem2o.u	⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
lclkrlem2o.a	⊢ ⊕ = (LSSum‘𝑈)
lclkrlem2o.k	⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
lclkrlem2o.b	⊢ 𝐵 = (𝑋 − ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌))
lclkrlem2o.n	⊢ (𝜑 → ((𝐸 + 𝐺)‘𝑌) ≠ 0 )
lclkrlem2p.bn	⊢ (𝜑 → 𝐵 = (0_g‘𝑈))

**Assertion**
Ref	Expression
lclkrlem2p	⊢ (𝜑 → ( ⊥ ‘{𝑌}) ⊆ ( ⊥ ‘{𝑋}))

**Proof of Theorem lclkrlem2p**
Step	Hyp	Ref	Expression
1		lclkrlem2o.k	. . 3 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
2		lclkrlem2o.h	. . . . . 6 ⊢ 𝐻 = (LHyp‘𝐾)
3		lclkrlem2o.u	. . . . . 6 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
4	2, 3, 1	dvhlmod 41695	. . . . 5 ⊢ (𝜑 → 𝑈 ∈ LMod)
5		lclkrlem2m.y	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ 𝑉)
6		lclkrlem2m.v	. . . . . 6 ⊢ 𝑉 = (Base‘𝑈)
7		eqid 2761	. . . . . 6 ⊢ (LSubSp‘𝑈) = (LSubSp‘𝑈)
8		lclkrlem2n.n	. . . . . 6 ⊢ 𝑁 = (LSpan‘𝑈)
9	6, 7, 8	lspsncl 21032	. . . . 5 ⊢ ((𝑈 ∈ LMod ∧ 𝑌 ∈ 𝑉) → (𝑁‘{𝑌}) ∈ (LSubSp‘𝑈))
10	4, 5, 9	syl2anc 593	. . . 4 ⊢ (𝜑 → (𝑁‘{𝑌}) ∈ (LSubSp‘𝑈))
11	6, 7	lssss 20991	. . . 4 ⊢ ((𝑁‘{𝑌}) ∈ (LSubSp‘𝑈) → (𝑁‘{𝑌}) ⊆ 𝑉)
12	10, 11	syl 17	. . 3 ⊢ (𝜑 → (𝑁‘{𝑌}) ⊆ 𝑉)
13		lclkrlem2o.b	. . . . . . . 8 ⊢ 𝐵 = (𝑋 − ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌))
14		lclkrlem2p.bn	. . . . . . . 8 ⊢ (𝜑 → 𝐵 = (0_g‘𝑈))
15	13, 14	eqtr3id 2810	. . . . . . 7 ⊢ (𝜑 → (𝑋 − ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌)) = (0_g‘𝑈))
16		lclkrlem2m.x	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
17		lclkrlem2m.s	. . . . . . . . . . . 12 ⊢ 𝑆 = (Scalar‘𝑈)
18	17	lmodring 20923	. . . . . . . . . . 11 ⊢ (𝑈 ∈ LMod → 𝑆 ∈ Ring)
19	4, 18	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑆 ∈ Ring)
20		lclkrlem2m.f	. . . . . . . . . . . 12 ⊢ 𝐹 = (LFnl‘𝑈)
21		lclkrlem2m.d	. . . . . . . . . . . 12 ⊢ 𝐷 = (LDual‘𝑈)
22		lclkrlem2m.p	. . . . . . . . . . . 12 ⊢ + = (+_g‘𝐷)
23		lclkrlem2m.e	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐸 ∈ 𝐹)
24		lclkrlem2m.g	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐺 ∈ 𝐹)
25	20, 21, 22, 4, 23, 24	ldualvaddcl 39715	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸 + 𝐺) ∈ 𝐹)
26		eqid 2761	. . . . . . . . . . . 12 ⊢ (Base‘𝑆) = (Base‘𝑆)
27	17, 26, 6, 20	lflcl 39649	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ LMod ∧ (𝐸 + 𝐺) ∈ 𝐹 ∧ 𝑋 ∈ 𝑉) → ((𝐸 + 𝐺)‘𝑋) ∈ (Base‘𝑆))
28	4, 25, 16, 27	syl3anc 1389	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝑋) ∈ (Base‘𝑆))
29	2, 3, 1	dvhlvec 41694	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑈 ∈ LVec)
30	17	lvecdrng 21160	. . . . . . . . . . . 12 ⊢ (𝑈 ∈ LVec → 𝑆 ∈ DivRing)
31	29, 30	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 ∈ DivRing)
32	17, 26, 6, 20	lflcl 39649	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ LMod ∧ (𝐸 + 𝐺) ∈ 𝐹 ∧ 𝑌 ∈ 𝑉) → ((𝐸 + 𝐺)‘𝑌) ∈ (Base‘𝑆))
33	4, 25, 5, 32	syl3anc 1389	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝑌) ∈ (Base‘𝑆))
34		lclkrlem2o.n	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝑌) ≠ 0 )
35		lclkrlem2m.z	. . . . . . . . . . . 12 ⊢ 0 = (0_g‘𝑆)
36		lclkrlem2m.i	. . . . . . . . . . . 12 ⊢ 𝐼 = (inv_r‘𝑆)
37	26, 35, 36	drnginvrcl 20790	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ DivRing ∧ ((𝐸 + 𝐺)‘𝑌) ∈ (Base‘𝑆) ∧ ((𝐸 + 𝐺)‘𝑌) ≠ 0 ) → (𝐼‘((𝐸 + 𝐺)‘𝑌)) ∈ (Base‘𝑆))
38	31, 33, 34, 37	syl3anc 1389	. . . . . . . . . 10 ⊢ (𝜑 → (𝐼‘((𝐸 + 𝐺)‘𝑌)) ∈ (Base‘𝑆))
39		lclkrlem2m.q	. . . . . . . . . . 11 ⊢ × = (._r‘𝑆)
40	26, 39	ringcl 20287	. . . . . . . . . 10 ⊢ ((𝑆 ∈ Ring ∧ ((𝐸 + 𝐺)‘𝑋) ∈ (Base‘𝑆) ∧ (𝐼‘((𝐸 + 𝐺)‘𝑌)) ∈ (Base‘𝑆)) → (((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) ∈ (Base‘𝑆))
41	19, 28, 38, 40	syl3anc 1389	. . . . . . . . 9 ⊢ (𝜑 → (((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) ∈ (Base‘𝑆))
42		lclkrlem2m.t	. . . . . . . . . 10 ⊢ · = ( ·_𝑠 ‘𝑈)
43	6, 17, 42, 26	lmodvscl 20933	. . . . . . . . 9 ⊢ ((𝑈 ∈ LMod ∧ (((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) ∈ (Base‘𝑆) ∧ 𝑌 ∈ 𝑉) → ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌) ∈ 𝑉)
44	4, 41, 5, 43	syl3anc 1389	. . . . . . . 8 ⊢ (𝜑 → ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌) ∈ 𝑉)
45		eqid 2761	. . . . . . . . 9 ⊢ (0_g‘𝑈) = (0_g‘𝑈)
46		lclkrlem2m.m	. . . . . . . . 9 ⊢ − = (-_g‘𝑈)
47	6, 45, 46	lmodsubeq0 20976	. . . . . . . 8 ⊢ ((𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌) ∈ 𝑉) → ((𝑋 − ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌)) = (0_g‘𝑈) ↔ 𝑋 = ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌)))
48	4, 16, 44, 47	syl3anc 1389	. . . . . . 7 ⊢ (𝜑 → ((𝑋 − ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌)) = (0_g‘𝑈) ↔ 𝑋 = ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌)))
49	15, 48	mpbid 234	. . . . . 6 ⊢ (𝜑 → 𝑋 = ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌))
50	49	sneqd 4591	. . . . 5 ⊢ (𝜑 → {𝑋} = {((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌)})
51	50	fveq2d 6866	. . . 4 ⊢ (𝜑 → (𝑁‘{𝑋}) = (𝑁‘{((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌)}))
52	17, 26, 6, 42, 8	lspsnvsi 21059	. . . . 5 ⊢ ((𝑈 ∈ LMod ∧ (((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) ∈ (Base‘𝑆) ∧ 𝑌 ∈ 𝑉) → (𝑁‘{((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌)}) ⊆ (𝑁‘{𝑌}))
53	4, 41, 5, 52	syl3anc 1389	. . . 4 ⊢ (𝜑 → (𝑁‘{((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌)}) ⊆ (𝑁‘{𝑌}))
54	51, 53	eqsstrd 3968	. . 3 ⊢ (𝜑 → (𝑁‘{𝑋}) ⊆ (𝑁‘{𝑌}))
55		lclkrlem2o.o	. . . 4 ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)
56	2, 3, 6, 55	dochss 41950	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑁‘{𝑌}) ⊆ 𝑉 ∧ (𝑁‘{𝑋}) ⊆ (𝑁‘{𝑌})) → ( ⊥ ‘(𝑁‘{𝑌})) ⊆ ( ⊥ ‘(𝑁‘{𝑋})))
57	1, 12, 54, 56	syl3anc 1389	. 2 ⊢ (𝜑 → ( ⊥ ‘(𝑁‘{𝑌})) ⊆ ( ⊥ ‘(𝑁‘{𝑋})))
58	5	snssd 4742	. . 3 ⊢ (𝜑 → {𝑌} ⊆ 𝑉)
59	2, 3, 55, 6, 8, 1, 58	dochocsp 41964	. 2 ⊢ (𝜑 → ( ⊥ ‘(𝑁‘{𝑌})) = ( ⊥ ‘{𝑌}))
60	16	snssd 4742	. . 3 ⊢ (𝜑 → {𝑋} ⊆ 𝑉)
61	2, 3, 55, 6, 8, 1, 60	dochocsp 41964	. 2 ⊢ (𝜑 → ( ⊥ ‘(𝑁‘{𝑋})) = ( ⊥ ‘{𝑋}))
62	57, 59, 61	3sstr3d 3988	1 ⊢ (𝜑 → ( ⊥ ‘{𝑌}) ⊆ ( ⊥ ‘{𝑋}))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 399 = wceq 1559 ∈ wcel 2141 ≠ wne 2956 ⊆ wss 3902 {csn 4579 ‘cfv 6516 (class class class)co 7391 Basecbs 17236 +_gcplusg 17277 ._rcmulr 17278 Scalarcsca 17280 ·_𝑠 cvsca 17281 0_gc0g 17459 -_gcsg 18968 LSSumclsm 19665 Ringcrg 20270 inv_rcinvr 20423 DivRingcdr 20766 LModclmod 20915 LSubSpclss 20986 LSpanclspn 21026 LVecclvec 21157 LFnlclfn 39642 LKerclk 39670 LDualcld 39708 HLchlt 39935 LHypclh 40569 DVecHcdvh 41663 ocHcoch 41932

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-rep 5224 ax-sep 5243 ax-nul 5253 ax-pow 5319 ax-pr 5387 ax-un 7713 ax-cnex 11123 ax-resscn 11124 ax-1cn 11125 ax-icn 11126 ax-addcl 11127 ax-addrcl 11128 ax-mulcl 11129 ax-mulrcl 11130 ax-mulcom 11131 ax-addass 11132 ax-mulass 11133 ax-distr 11134 ax-i2m1 11135 ax-1ne0 11136 ax-1rid 11137 ax-rnegex 11138 ax-rrecex 11139 ax-cnre 11140 ax-pre-lttri 11141 ax-pre-lttrn 11142 ax-pre-ltadd 11143 ax-pre-mulgt0 11144 ax-riotaBAD 39538

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1098 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-nf 1803 df-sb 2090 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3061 df-ral 3076 df-rex 3086 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4284 df-if 4478 df-pw 4554 df-sn 4580 df-pr 4582 df-tp 4584 df-op 4586 df-uni 4863 df-int 4903 df-iun 4948 df-iin 4949 df-br 5098 df-opab 5160 df-mpt 5179 df-tr 5205 df-id 5538 df-eprel 5543 df-po 5551 df-so 5552 df-fr 5596 df-we 5598 df-xp 5649 df-rel 5650 df-cnv 5651 df-co 5652 df-dm 5653 df-rn 5654 df-res 5655 df-ima 5656 df-pred 6283 df-ord 6344 df-on 6345 df-lim 6346 df-suc 6347 df-iota 6472 df-fun 6518 df-fn 6519 df-f 6520 df-f1 6521 df-fo 6522 df-f1o 6523 df-fv 6524 df-riota 7348 df-ov 7394 df-oprab 7395 df-mpo 7396 df-of 7655 df-om 7842 df-1st 7965 df-2nd 7966 df-tpos 8200 df-undef 8247 df-frecs 8256 df-wrecs 8287 df-recs 8336 df-rdg 8375 df-1o 8431 df-er 8672 df-map 8804 df-en 8922 df-dom 8923 df-sdom 8924 df-fin 8925 df-pnf 11212 df-mnf 11213 df-xr 11214 df-ltxr 11215 df-le 11216 df-sub 11410 df-neg 11411 df-nn 12205 df-2 12274 df-3 12275 df-4 12276 df-5 12277 df-6 12278 df-n0 12476 df-z 12563 df-uz 12834 df-fz 13507 df-struct 17174 df-sets 17191 df-slot 17209 df-ndx 17221 df-base 17237 df-ress 17258 df-plusg 17290 df-mulr 17291 df-sca 17293 df-vsca 17294 df-0g 17461 df-proset 18317 df-poset 18336 df-plt 18351 df-lub 18367 df-glb 18368 df-join 18369 df-meet 18370 df-p0 18446 df-p1 18447 df-lat 18455 df-clat 18522 df-mgm 18665 df-sgrp 18744 df-mnd 18760 df-submnd 18809 df-grp 18969 df-minusg 18970 df-sbg 18971 df-subg 19156 df-cntz 19348 df-lsm 19667 df-cmn 19813 df-abl 19814 df-mgp 20178 df-rng 20190 df-ur 20219 df-ring 20272 df-oppr 20373 df-dvdsr 20393 df-unit 20394 df-invr 20424 df-dvr 20437 df-drng 20768 df-lmod 20917 df-lss 20987 df-lsp 21027 df-lvec 21158 df-lsatoms 39561 df-lfl 39643 df-ldual 39709 df-oposet 39761 df-ol 39763 df-oml 39764 df-covers 39851 df-ats 39852 df-atl 39883 df-cvlat 39907 df-hlat 39936 df-llines 40083 df-lplanes 40084 df-lvols 40085 df-lines 40086 df-psubsp 40088 df-pmap 40089 df-padd 40381 df-lhyp 40573 df-laut 40574 df-ldil 40689 df-ltrn 40690 df-trl 40744 df-tendo 41340 df-edring 41342 df-disoa 41614 df-dvech 41664 df-dib 41724 df-dic 41758 df-dih 41814 df-doch 41933

This theorem is referenced by: lclkrlem2r 42109

W3C validator