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 41561

Description: Lemma for lclkr 41572. 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 41149	. . . . 5 ⊢ (𝜑 → 𝑈 ∈ LMod)
5		lclkrlem2m.y	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ 𝑉)
6		lclkrlem2m.v	. . . . . 6 ⊢ 𝑉 = (Base‘𝑈)
7		eqid 2731	. . . . . 6 ⊢ (LSubSp‘𝑈) = (LSubSp‘𝑈)
8		lclkrlem2n.n	. . . . . 6 ⊢ 𝑁 = (LSpan‘𝑈)
9	6, 7, 8	lspsncl 20905	. . . . 5 ⊢ ((𝑈 ∈ LMod ∧ 𝑌 ∈ 𝑉) → (𝑁‘{𝑌}) ∈ (LSubSp‘𝑈))
10	4, 5, 9	syl2anc 584	. . . 4 ⊢ (𝜑 → (𝑁‘{𝑌}) ∈ (LSubSp‘𝑈))
11	6, 7	lssss 20864	. . . 4 ⊢ ((𝑁‘{𝑌}) ∈ (LSubSp‘𝑈) → (𝑁‘{𝑌}) ⊆ 𝑉)
12	10, 11	syl 17	. . 3 ⊢ (𝜑 → (𝑁‘{𝑌}) ⊆ 𝑉)
13		lclkrlem2o.b	. . . . . . . 8 ⊢ 𝐵 = (𝑋 − ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌))
14		lclkrlem2p.bn	. . . . . . . 8 ⊢ (𝜑 → 𝐵 = (0_g‘𝑈))
15	13, 14	eqtr3id 2780	. . . . . . 7 ⊢ (𝜑 → (𝑋 − ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌)) = (0_g‘𝑈))
16		lclkrlem2m.x	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
17		lclkrlem2m.s	. . . . . . . . . . . 12 ⊢ 𝑆 = (Scalar‘𝑈)
18	17	lmodring 20796	. . . . . . . . . . 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 39169	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸 + 𝐺) ∈ 𝐹)
26		eqid 2731	. . . . . . . . . . . 12 ⊢ (Base‘𝑆) = (Base‘𝑆)
27	17, 26, 6, 20	lflcl 39103	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ LMod ∧ (𝐸 + 𝐺) ∈ 𝐹 ∧ 𝑋 ∈ 𝑉) → ((𝐸 + 𝐺)‘𝑋) ∈ (Base‘𝑆))
28	4, 25, 16, 27	syl3anc 1373	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝑋) ∈ (Base‘𝑆))
29	2, 3, 1	dvhlvec 41148	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑈 ∈ LVec)
30	17	lvecdrng 21034	. . . . . . . . . . . 12 ⊢ (𝑈 ∈ LVec → 𝑆 ∈ DivRing)
31	29, 30	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 ∈ DivRing)
32	17, 26, 6, 20	lflcl 39103	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ LMod ∧ (𝐸 + 𝐺) ∈ 𝐹 ∧ 𝑌 ∈ 𝑉) → ((𝐸 + 𝐺)‘𝑌) ∈ (Base‘𝑆))
33	4, 25, 5, 32	syl3anc 1373	. . . . . . . . . . 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 20663	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ DivRing ∧ ((𝐸 + 𝐺)‘𝑌) ∈ (Base‘𝑆) ∧ ((𝐸 + 𝐺)‘𝑌) ≠ 0 ) → (𝐼‘((𝐸 + 𝐺)‘𝑌)) ∈ (Base‘𝑆))
38	31, 33, 34, 37	syl3anc 1373	. . . . . . . . . 10 ⊢ (𝜑 → (𝐼‘((𝐸 + 𝐺)‘𝑌)) ∈ (Base‘𝑆))
39		lclkrlem2m.q	. . . . . . . . . . 11 ⊢ × = (._r‘𝑆)
40	26, 39	ringcl 20163	. . . . . . . . . 10 ⊢ ((𝑆 ∈ Ring ∧ ((𝐸 + 𝐺)‘𝑋) ∈ (Base‘𝑆) ∧ (𝐼‘((𝐸 + 𝐺)‘𝑌)) ∈ (Base‘𝑆)) → (((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) ∈ (Base‘𝑆))
41	19, 28, 38, 40	syl3anc 1373	. . . . . . . . 9 ⊢ (𝜑 → (((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) ∈ (Base‘𝑆))
42		lclkrlem2m.t	. . . . . . . . . 10 ⊢ · = ( ·_𝑠 ‘𝑈)
43	6, 17, 42, 26	lmodvscl 20806	. . . . . . . . 9 ⊢ ((𝑈 ∈ LMod ∧ (((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) ∈ (Base‘𝑆) ∧ 𝑌 ∈ 𝑉) → ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌) ∈ 𝑉)
44	4, 41, 5, 43	syl3anc 1373	. . . . . . . 8 ⊢ (𝜑 → ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌) ∈ 𝑉)
45		eqid 2731	. . . . . . . . 9 ⊢ (0_g‘𝑈) = (0_g‘𝑈)
46		lclkrlem2m.m	. . . . . . . . 9 ⊢ − = (-_g‘𝑈)
47	6, 45, 46	lmodsubeq0 20849	. . . . . . . 8 ⊢ ((𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌) ∈ 𝑉) → ((𝑋 − ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌)) = (0_g‘𝑈) ↔ 𝑋 = ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌)))
48	4, 16, 44, 47	syl3anc 1373	. . . . . . 7 ⊢ (𝜑 → ((𝑋 − ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌)) = (0_g‘𝑈) ↔ 𝑋 = ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌)))
49	15, 48	mpbid 232	. . . . . 6 ⊢ (𝜑 → 𝑋 = ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌))
50	49	sneqd 4583	. . . . 5 ⊢ (𝜑 → {𝑋} = {((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌)})
51	50	fveq2d 6821	. . . 4 ⊢ (𝜑 → (𝑁‘{𝑋}) = (𝑁‘{((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌)}))
52	17, 26, 6, 42, 8	lspsnvsi 20932	. . . . 5 ⊢ ((𝑈 ∈ LMod ∧ (((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) ∈ (Base‘𝑆) ∧ 𝑌 ∈ 𝑉) → (𝑁‘{((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌)}) ⊆ (𝑁‘{𝑌}))
53	4, 41, 5, 52	syl3anc 1373	. . . 4 ⊢ (𝜑 → (𝑁‘{((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌)}) ⊆ (𝑁‘{𝑌}))
54	51, 53	eqsstrd 3964	. . 3 ⊢ (𝜑 → (𝑁‘{𝑋}) ⊆ (𝑁‘{𝑌}))
55		lclkrlem2o.o	. . . 4 ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)
56	2, 3, 6, 55	dochss 41404	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑁‘{𝑌}) ⊆ 𝑉 ∧ (𝑁‘{𝑋}) ⊆ (𝑁‘{𝑌})) → ( ⊥ ‘(𝑁‘{𝑌})) ⊆ ( ⊥ ‘(𝑁‘{𝑋})))
57	1, 12, 54, 56	syl3anc 1373	. 2 ⊢ (𝜑 → ( ⊥ ‘(𝑁‘{𝑌})) ⊆ ( ⊥ ‘(𝑁‘{𝑋})))
58	5	snssd 4756	. . 3 ⊢ (𝜑 → {𝑌} ⊆ 𝑉)
59	2, 3, 55, 6, 8, 1, 58	dochocsp 41418	. 2 ⊢ (𝜑 → ( ⊥ ‘(𝑁‘{𝑌})) = ( ⊥ ‘{𝑌}))
60	16	snssd 4756	. . 3 ⊢ (𝜑 → {𝑋} ⊆ 𝑉)
61	2, 3, 55, 6, 8, 1, 60	dochocsp 41418	. 2 ⊢ (𝜑 → ( ⊥ ‘(𝑁‘{𝑋})) = ( ⊥ ‘{𝑋}))
62	57, 59, 61	3sstr3d 3984	1 ⊢ (𝜑 → ( ⊥ ‘{𝑌}) ⊆ ( ⊥ ‘{𝑋}))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1541 ∈ wcel 2111 ≠ wne 2928 ⊆ wss 3897 {csn 4571 ‘cfv 6476 (class class class)co 7341 Basecbs 17115 +_gcplusg 17156 ._rcmulr 17157 Scalarcsca 17159 ·_𝑠 cvsca 17160 0_gc0g 17338 -_gcsg 18843 LSSumclsm 19541 Ringcrg 20146 inv_rcinvr 20300 DivRingcdr 20639 LModclmod 20788 LSubSpclss 20859 LSpanclspn 20899 LVecclvec 21031 LFnlclfn 39096 LKerclk 39124 LDualcld 39162 HLchlt 39389 LHypclh 40023 DVecHcdvh 41117 ocHcoch 41386

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2113 ax-9 2121 ax-10 2144 ax-11 2160 ax-12 2180 ax-ext 2703 ax-rep 5212 ax-sep 5229 ax-nul 5239 ax-pow 5298 ax-pr 5365 ax-un 7663 ax-cnex 11057 ax-resscn 11058 ax-1cn 11059 ax-icn 11060 ax-addcl 11061 ax-addrcl 11062 ax-mulcl 11063 ax-mulrcl 11064 ax-mulcom 11065 ax-addass 11066 ax-mulass 11067 ax-distr 11068 ax-i2m1 11069 ax-1ne0 11070 ax-1rid 11071 ax-rnegex 11072 ax-rrecex 11073 ax-cnre 11074 ax-pre-lttri 11075 ax-pre-lttrn 11076 ax-pre-ltadd 11077 ax-pre-mulgt0 11078 ax-riotaBAD 38992

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2535 df-eu 2564 df-clab 2710 df-cleq 2723 df-clel 2806 df-nfc 2881 df-ne 2929 df-nel 3033 df-ral 3048 df-rex 3057 df-rmo 3346 df-reu 3347 df-rab 3396 df-v 3438 df-sbc 3737 df-csb 3846 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3917 df-nul 4279 df-if 4471 df-pw 4547 df-sn 4572 df-pr 4574 df-tp 4576 df-op 4578 df-uni 4855 df-int 4893 df-iun 4938 df-iin 4939 df-br 5087 df-opab 5149 df-mpt 5168 df-tr 5194 df-id 5506 df-eprel 5511 df-po 5519 df-so 5520 df-fr 5564 df-we 5566 df-xp 5617 df-rel 5618 df-cnv 5619 df-co 5620 df-dm 5621 df-rn 5622 df-res 5623 df-ima 5624 df-pred 6243 df-ord 6304 df-on 6305 df-lim 6306 df-suc 6307 df-iota 6432 df-fun 6478 df-fn 6479 df-f 6480 df-f1 6481 df-fo 6482 df-f1o 6483 df-fv 6484 df-riota 7298 df-ov 7344 df-oprab 7345 df-mpo 7346 df-of 7605 df-om 7792 df-1st 7916 df-2nd 7917 df-tpos 8151 df-undef 8198 df-frecs 8206 df-wrecs 8237 df-recs 8286 df-rdg 8324 df-1o 8380 df-er 8617 df-map 8747 df-en 8865 df-dom 8866 df-sdom 8867 df-fin 8868 df-pnf 11143 df-mnf 11144 df-xr 11145 df-ltxr 11146 df-le 11147 df-sub 11341 df-neg 11342 df-nn 12121 df-2 12183 df-3 12184 df-4 12185 df-5 12186 df-6 12187 df-n0 12377 df-z 12464 df-uz 12728 df-fz 13403 df-struct 17053 df-sets 17070 df-slot 17088 df-ndx 17100 df-base 17116 df-ress 17137 df-plusg 17169 df-mulr 17170 df-sca 17172 df-vsca 17173 df-0g 17340 df-proset 18195 df-poset 18214 df-plt 18229 df-lub 18245 df-glb 18246 df-join 18247 df-meet 18248 df-p0 18324 df-p1 18325 df-lat 18333 df-clat 18400 df-mgm 18543 df-sgrp 18622 df-mnd 18638 df-submnd 18687 df-grp 18844 df-minusg 18845 df-sbg 18846 df-subg 19031 df-cntz 19224 df-lsm 19543 df-cmn 19689 df-abl 19690 df-mgp 20054 df-rng 20066 df-ur 20095 df-ring 20148 df-oppr 20250 df-dvdsr 20270 df-unit 20271 df-invr 20301 df-dvr 20314 df-drng 20641 df-lmod 20790 df-lss 20860 df-lsp 20900 df-lvec 21032 df-lsatoms 39015 df-lfl 39097 df-ldual 39163 df-oposet 39215 df-ol 39217 df-oml 39218 df-covers 39305 df-ats 39306 df-atl 39337 df-cvlat 39361 df-hlat 39390 df-llines 39537 df-lplanes 39538 df-lvols 39539 df-lines 39540 df-psubsp 39542 df-pmap 39543 df-padd 39835 df-lhyp 40027 df-laut 40028 df-ldil 40143 df-ltrn 40144 df-trl 40198 df-tendo 40794 df-edring 40796 df-disoa 41068 df-dvech 41118 df-dib 41178 df-dic 41212 df-dih 41268 df-doch 41387

This theorem is referenced by: lclkrlem2r 41563

W3C validator