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 41895

Description: Lemma for lclkr 41906. 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 41483	. . . . 5 ⊢ (𝜑 → 𝑈 ∈ LMod)
5		lclkrlem2m.y	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ 𝑉)
6		lclkrlem2m.v	. . . . . 6 ⊢ 𝑉 = (Base‘𝑈)
7		eqid 2737	. . . . . 6 ⊢ (LSubSp‘𝑈) = (LSubSp‘𝑈)
8		lclkrlem2n.n	. . . . . 6 ⊢ 𝑁 = (LSpan‘𝑈)
9	6, 7, 8	lspsncl 20940	. . . . 5 ⊢ ((𝑈 ∈ LMod ∧ 𝑌 ∈ 𝑉) → (𝑁‘{𝑌}) ∈ (LSubSp‘𝑈))
10	4, 5, 9	syl2anc 585	. . . 4 ⊢ (𝜑 → (𝑁‘{𝑌}) ∈ (LSubSp‘𝑈))
11	6, 7	lssss 20899	. . . 4 ⊢ ((𝑁‘{𝑌}) ∈ (LSubSp‘𝑈) → (𝑁‘{𝑌}) ⊆ 𝑉)
12	10, 11	syl 17	. . 3 ⊢ (𝜑 → (𝑁‘{𝑌}) ⊆ 𝑉)
13		lclkrlem2o.b	. . . . . . . 8 ⊢ 𝐵 = (𝑋 − ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌))
14		lclkrlem2p.bn	. . . . . . . 8 ⊢ (𝜑 → 𝐵 = (0_g‘𝑈))
15	13, 14	eqtr3id 2786	. . . . . . 7 ⊢ (𝜑 → (𝑋 − ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌)) = (0_g‘𝑈))
16		lclkrlem2m.x	. . . . . . . 8 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
17		lclkrlem2m.s	. . . . . . . . . . . 12 ⊢ 𝑆 = (Scalar‘𝑈)
18	17	lmodring 20831	. . . . . . . . . . 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 39503	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐸 + 𝐺) ∈ 𝐹)
26		eqid 2737	. . . . . . . . . . . 12 ⊢ (Base‘𝑆) = (Base‘𝑆)
27	17, 26, 6, 20	lflcl 39437	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ LMod ∧ (𝐸 + 𝐺) ∈ 𝐹 ∧ 𝑋 ∈ 𝑉) → ((𝐸 + 𝐺)‘𝑋) ∈ (Base‘𝑆))
28	4, 25, 16, 27	syl3anc 1374	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝑋) ∈ (Base‘𝑆))
29	2, 3, 1	dvhlvec 41482	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑈 ∈ LVec)
30	17	lvecdrng 21069	. . . . . . . . . . . 12 ⊢ (𝑈 ∈ LVec → 𝑆 ∈ DivRing)
31	29, 30	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑆 ∈ DivRing)
32	17, 26, 6, 20	lflcl 39437	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ LMod ∧ (𝐸 + 𝐺) ∈ 𝐹 ∧ 𝑌 ∈ 𝑉) → ((𝐸 + 𝐺)‘𝑌) ∈ (Base‘𝑆))
33	4, 25, 5, 32	syl3anc 1374	. . . . . . . . . . 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 20698	. . . . . . . . . . 11 ⊢ ((𝑆 ∈ DivRing ∧ ((𝐸 + 𝐺)‘𝑌) ∈ (Base‘𝑆) ∧ ((𝐸 + 𝐺)‘𝑌) ≠ 0 ) → (𝐼‘((𝐸 + 𝐺)‘𝑌)) ∈ (Base‘𝑆))
38	31, 33, 34, 37	syl3anc 1374	. . . . . . . . . 10 ⊢ (𝜑 → (𝐼‘((𝐸 + 𝐺)‘𝑌)) ∈ (Base‘𝑆))
39		lclkrlem2m.q	. . . . . . . . . . 11 ⊢ × = (._r‘𝑆)
40	26, 39	ringcl 20197	. . . . . . . . . 10 ⊢ ((𝑆 ∈ Ring ∧ ((𝐸 + 𝐺)‘𝑋) ∈ (Base‘𝑆) ∧ (𝐼‘((𝐸 + 𝐺)‘𝑌)) ∈ (Base‘𝑆)) → (((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) ∈ (Base‘𝑆))
41	19, 28, 38, 40	syl3anc 1374	. . . . . . . . 9 ⊢ (𝜑 → (((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) ∈ (Base‘𝑆))
42		lclkrlem2m.t	. . . . . . . . . 10 ⊢ · = ( ·_𝑠 ‘𝑈)
43	6, 17, 42, 26	lmodvscl 20841	. . . . . . . . 9 ⊢ ((𝑈 ∈ LMod ∧ (((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) ∈ (Base‘𝑆) ∧ 𝑌 ∈ 𝑉) → ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌) ∈ 𝑉)
44	4, 41, 5, 43	syl3anc 1374	. . . . . . . 8 ⊢ (𝜑 → ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌) ∈ 𝑉)
45		eqid 2737	. . . . . . . . 9 ⊢ (0_g‘𝑈) = (0_g‘𝑈)
46		lclkrlem2m.m	. . . . . . . . 9 ⊢ − = (-_g‘𝑈)
47	6, 45, 46	lmodsubeq0 20884	. . . . . . . 8 ⊢ ((𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌) ∈ 𝑉) → ((𝑋 − ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌)) = (0_g‘𝑈) ↔ 𝑋 = ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌)))
48	4, 16, 44, 47	syl3anc 1374	. . . . . . 7 ⊢ (𝜑 → ((𝑋 − ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌)) = (0_g‘𝑈) ↔ 𝑋 = ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌)))
49	15, 48	mpbid 232	. . . . . 6 ⊢ (𝜑 → 𝑋 = ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌))
50	49	sneqd 4594	. . . . 5 ⊢ (𝜑 → {𝑋} = {((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌)})
51	50	fveq2d 6846	. . . 4 ⊢ (𝜑 → (𝑁‘{𝑋}) = (𝑁‘{((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌)}))
52	17, 26, 6, 42, 8	lspsnvsi 20967	. . . . 5 ⊢ ((𝑈 ∈ LMod ∧ (((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) ∈ (Base‘𝑆) ∧ 𝑌 ∈ 𝑉) → (𝑁‘{((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌)}) ⊆ (𝑁‘{𝑌}))
53	4, 41, 5, 52	syl3anc 1374	. . . 4 ⊢ (𝜑 → (𝑁‘{((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌)}) ⊆ (𝑁‘{𝑌}))
54	51, 53	eqsstrd 3970	. . 3 ⊢ (𝜑 → (𝑁‘{𝑋}) ⊆ (𝑁‘{𝑌}))
55		lclkrlem2o.o	. . . 4 ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)
56	2, 3, 6, 55	dochss 41738	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑁‘{𝑌}) ⊆ 𝑉 ∧ (𝑁‘{𝑋}) ⊆ (𝑁‘{𝑌})) → ( ⊥ ‘(𝑁‘{𝑌})) ⊆ ( ⊥ ‘(𝑁‘{𝑋})))
57	1, 12, 54, 56	syl3anc 1374	. 2 ⊢ (𝜑 → ( ⊥ ‘(𝑁‘{𝑌})) ⊆ ( ⊥ ‘(𝑁‘{𝑋})))
58	5	snssd 4767	. . 3 ⊢ (𝜑 → {𝑌} ⊆ 𝑉)
59	2, 3, 55, 6, 8, 1, 58	dochocsp 41752	. 2 ⊢ (𝜑 → ( ⊥ ‘(𝑁‘{𝑌})) = ( ⊥ ‘{𝑌}))
60	16	snssd 4767	. . 3 ⊢ (𝜑 → {𝑋} ⊆ 𝑉)
61	2, 3, 55, 6, 8, 1, 60	dochocsp 41752	. 2 ⊢ (𝜑 → ( ⊥ ‘(𝑁‘{𝑋})) = ( ⊥ ‘{𝑋}))
62	57, 59, 61	3sstr3d 3990	1 ⊢ (𝜑 → ( ⊥ ‘{𝑌}) ⊆ ( ⊥ ‘{𝑋}))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1542 ∈ wcel 2114 ≠ wne 2933 ⊆ wss 3903 {csn 4582 ‘cfv 6500 (class class class)co 7368 Basecbs 17148 +_gcplusg 17189 ._rcmulr 17190 Scalarcsca 17192 ·_𝑠 cvsca 17193 0_gc0g 17371 -_gcsg 18877 LSSumclsm 19575 Ringcrg 20180 inv_rcinvr 20335 DivRingcdr 20674 LModclmod 20823 LSubSpclss 20894 LSpanclspn 20934 LVecclvec 21066 LFnlclfn 39430 LKerclk 39458 LDualcld 39496 HLchlt 39723 LHypclh 40357 DVecHcdvh 41451 ocHcoch 41720

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5226 ax-sep 5243 ax-nul 5253 ax-pow 5312 ax-pr 5379 ax-un 7690 ax-cnex 11094 ax-resscn 11095 ax-1cn 11096 ax-icn 11097 ax-addcl 11098 ax-addrcl 11099 ax-mulcl 11100 ax-mulrcl 11101 ax-mulcom 11102 ax-addass 11103 ax-mulass 11104 ax-distr 11105 ax-i2m1 11106 ax-1ne0 11107 ax-1rid 11108 ax-rnegex 11109 ax-rrecex 11110 ax-cnre 11111 ax-pre-lttri 11112 ax-pre-lttrn 11113 ax-pre-ltadd 11114 ax-pre-mulgt0 11115 ax-riotaBAD 39326

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-nel 3038 df-ral 3053 df-rex 3063 df-rmo 3352 df-reu 3353 df-rab 3402 df-v 3444 df-sbc 3743 df-csb 3852 df-dif 3906 df-un 3908 df-in 3910 df-ss 3920 df-pss 3923 df-nul 4288 df-if 4482 df-pw 4558 df-sn 4583 df-pr 4585 df-tp 4587 df-op 4589 df-uni 4866 df-int 4905 df-iun 4950 df-iin 4951 df-br 5101 df-opab 5163 df-mpt 5182 df-tr 5208 df-id 5527 df-eprel 5532 df-po 5540 df-so 5541 df-fr 5585 df-we 5587 df-xp 5638 df-rel 5639 df-cnv 5640 df-co 5641 df-dm 5642 df-rn 5643 df-res 5644 df-ima 5645 df-pred 6267 df-ord 6328 df-on 6329 df-lim 6330 df-suc 6331 df-iota 6456 df-fun 6502 df-fn 6503 df-f 6504 df-f1 6505 df-fo 6506 df-f1o 6507 df-fv 6508 df-riota 7325 df-ov 7371 df-oprab 7372 df-mpo 7373 df-of 7632 df-om 7819 df-1st 7943 df-2nd 7944 df-tpos 8178 df-undef 8225 df-frecs 8233 df-wrecs 8264 df-recs 8313 df-rdg 8351 df-1o 8407 df-er 8645 df-map 8777 df-en 8896 df-dom 8897 df-sdom 8898 df-fin 8899 df-pnf 11180 df-mnf 11181 df-xr 11182 df-ltxr 11183 df-le 11184 df-sub 11378 df-neg 11379 df-nn 12158 df-2 12220 df-3 12221 df-4 12222 df-5 12223 df-6 12224 df-n0 12414 df-z 12501 df-uz 12764 df-fz 13436 df-struct 17086 df-sets 17103 df-slot 17121 df-ndx 17133 df-base 17149 df-ress 17170 df-plusg 17202 df-mulr 17203 df-sca 17205 df-vsca 17206 df-0g 17373 df-proset 18229 df-poset 18248 df-plt 18263 df-lub 18279 df-glb 18280 df-join 18281 df-meet 18282 df-p0 18358 df-p1 18359 df-lat 18367 df-clat 18434 df-mgm 18577 df-sgrp 18656 df-mnd 18672 df-submnd 18721 df-grp 18878 df-minusg 18879 df-sbg 18880 df-subg 19065 df-cntz 19258 df-lsm 19577 df-cmn 19723 df-abl 19724 df-mgp 20088 df-rng 20100 df-ur 20129 df-ring 20182 df-oppr 20285 df-dvdsr 20305 df-unit 20306 df-invr 20336 df-dvr 20349 df-drng 20676 df-lmod 20825 df-lss 20895 df-lsp 20935 df-lvec 21067 df-lsatoms 39349 df-lfl 39431 df-ldual 39497 df-oposet 39549 df-ol 39551 df-oml 39552 df-covers 39639 df-ats 39640 df-atl 39671 df-cvlat 39695 df-hlat 39724 df-llines 39871 df-lplanes 39872 df-lvols 39873 df-lines 39874 df-psubsp 39876 df-pmap 39877 df-padd 40169 df-lhyp 40361 df-laut 40362 df-ldil 40477 df-ltrn 40478 df-trl 40532 df-tendo 41128 df-edring 41130 df-disoa 41402 df-dvech 41452 df-dib 41512 df-dic 41546 df-dih 41602 df-doch 41721

This theorem is referenced by: lclkrlem2r 41897

W3C validator