lclkrlem2o - Mathbox for Norm Megill

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

Theorem lclkrlem2o 42315

Description: Lemma for lclkr 42327. When 𝐵 is nonzero, the vectors 𝑋 and 𝑌 can't both belong to the hyperplane generated by 𝐵. (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 )
lclkrlem2o.bn	⊢ (𝜑 → 𝐵 ≠ (0_g‘𝑈))

**Assertion**
Ref	Expression
lclkrlem2o	⊢ (𝜑 → (¬ 𝑋 ∈ ( ⊥ ‘{𝐵}) ∨ ¬ 𝑌 ∈ ( ⊥ ‘{𝐵})))

**Proof of Theorem lclkrlem2o**
Step	Hyp	Ref	Expression
1		lclkrlem2o.h	. . . 4 ⊢ 𝐻 = (LHyp‘𝐾)
2		lclkrlem2o.o	. . . 4 ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)
3		lclkrlem2o.u	. . . 4 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
4		lclkrlem2m.v	. . . 4 ⊢ 𝑉 = (Base‘𝑈)
5		eqid 2763	. . . 4 ⊢ (0_g‘𝑈) = (0_g‘𝑈)
6		lclkrlem2o.k	. . . 4 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
7		lclkrlem2m.t	. . . . . . 7 ⊢ · = ( ·_𝑠 ‘𝑈)
8		lclkrlem2m.s	. . . . . . 7 ⊢ 𝑆 = (Scalar‘𝑈)
9		lclkrlem2m.q	. . . . . . 7 ⊢ × = (._r‘𝑆)
10		lclkrlem2m.z	. . . . . . 7 ⊢ 0 = (0_g‘𝑆)
11		lclkrlem2m.i	. . . . . . 7 ⊢ 𝐼 = (inv_r‘𝑆)
12		lclkrlem2m.m	. . . . . . 7 ⊢ − = (-_g‘𝑈)
13		lclkrlem2m.f	. . . . . . 7 ⊢ 𝐹 = (LFnl‘𝑈)
14		lclkrlem2m.d	. . . . . . 7 ⊢ 𝐷 = (LDual‘𝑈)
15		lclkrlem2m.p	. . . . . . 7 ⊢ + = (+_g‘𝐷)
16		lclkrlem2m.x	. . . . . . 7 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
17		lclkrlem2m.y	. . . . . . 7 ⊢ (𝜑 → 𝑌 ∈ 𝑉)
18		lclkrlem2m.e	. . . . . . 7 ⊢ (𝜑 → 𝐸 ∈ 𝐹)
19		lclkrlem2m.g	. . . . . . 7 ⊢ (𝜑 → 𝐺 ∈ 𝐹)
20	1, 3, 6	dvhlvec 41903	. . . . . . 7 ⊢ (𝜑 → 𝑈 ∈ LVec)
21		lclkrlem2o.b	. . . . . . 7 ⊢ 𝐵 = (𝑋 − ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌))
22		lclkrlem2o.n	. . . . . . 7 ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝑌) ≠ 0 )
23	4, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22	lclkrlem2m 42313	. . . . . 6 ⊢ (𝜑 → (𝐵 ∈ 𝑉 ∧ ((𝐸 + 𝐺)‘𝐵) = 0 ))
24	23	simpld 499	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ 𝑉)
25		lclkrlem2o.bn	. . . . 5 ⊢ (𝜑 → 𝐵 ≠ (0_g‘𝑈))
26		eldifsn 4753	. . . . 5 ⊢ (𝐵 ∈ (𝑉 ∖ {(0_g‘𝑈)}) ↔ (𝐵 ∈ 𝑉 ∧ 𝐵 ≠ (0_g‘𝑈)))
27	24, 25, 26	sylanbrc 594	. . . 4 ⊢ (𝜑 → 𝐵 ∈ (𝑉 ∖ {(0_g‘𝑈)}))
28	1, 2, 3, 4, 5, 6, 27	dochnel 42187	. . 3 ⊢ (𝜑 → ¬ 𝐵 ∈ ( ⊥ ‘{𝐵}))
29	1, 3, 6	dvhlmod 41904	. . . . . 6 ⊢ (𝜑 → 𝑈 ∈ LMod)
30	29	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ (𝑋 ∈ ( ⊥ ‘{𝐵}) ∧ 𝑌 ∈ ( ⊥ ‘{𝐵}))) → 𝑈 ∈ LMod)
31	24	snssd 4752	. . . . . . 7 ⊢ (𝜑 → {𝐵} ⊆ 𝑉)
32		eqid 2763	. . . . . . . 8 ⊢ (LSubSp‘𝑈) = (LSubSp‘𝑈)
33	1, 3, 4, 32, 2	dochlss 42148	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ {𝐵} ⊆ 𝑉) → ( ⊥ ‘{𝐵}) ∈ (LSubSp‘𝑈))
34	6, 31, 33	syl2anc 595	. . . . . 6 ⊢ (𝜑 → ( ⊥ ‘{𝐵}) ∈ (LSubSp‘𝑈))
35	34	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ (𝑋 ∈ ( ⊥ ‘{𝐵}) ∧ 𝑌 ∈ ( ⊥ ‘{𝐵}))) → ( ⊥ ‘{𝐵}) ∈ (LSubSp‘𝑈))
36		simprl 782	. . . . 5 ⊢ ((𝜑 ∧ (𝑋 ∈ ( ⊥ ‘{𝐵}) ∧ 𝑌 ∈ ( ⊥ ‘{𝐵}))) → 𝑋 ∈ ( ⊥ ‘{𝐵}))
37	8	lmodring 20989	. . . . . . . . 9 ⊢ (𝑈 ∈ LMod → 𝑆 ∈ Ring)
38	29, 37	syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝑆 ∈ Ring)
39	13, 14, 15, 29, 18, 19	ldualvaddcl 39924	. . . . . . . . 9 ⊢ (𝜑 → (𝐸 + 𝐺) ∈ 𝐹)
40		eqid 2763	. . . . . . . . . 10 ⊢ (Base‘𝑆) = (Base‘𝑆)
41	8, 40, 4, 13	lflcl 39858	. . . . . . . . 9 ⊢ ((𝑈 ∈ LMod ∧ (𝐸 + 𝐺) ∈ 𝐹 ∧ 𝑋 ∈ 𝑉) → ((𝐸 + 𝐺)‘𝑋) ∈ (Base‘𝑆))
42	29, 39, 16, 41	syl3anc 1398	. . . . . . . 8 ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝑋) ∈ (Base‘𝑆))
43	8	lvecdrng 21226	. . . . . . . . . 10 ⊢ (𝑈 ∈ LVec → 𝑆 ∈ DivRing)
44	20, 43	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ∈ DivRing)
45	8, 40, 4, 13	lflcl 39858	. . . . . . . . . 10 ⊢ ((𝑈 ∈ LMod ∧ (𝐸 + 𝐺) ∈ 𝐹 ∧ 𝑌 ∈ 𝑉) → ((𝐸 + 𝐺)‘𝑌) ∈ (Base‘𝑆))
46	29, 39, 17, 45	syl3anc 1398	. . . . . . . . 9 ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝑌) ∈ (Base‘𝑆))
47	40, 10, 11	drnginvrcl 20857	. . . . . . . . 9 ⊢ ((𝑆 ∈ DivRing ∧ ((𝐸 + 𝐺)‘𝑌) ∈ (Base‘𝑆) ∧ ((𝐸 + 𝐺)‘𝑌) ≠ 0 ) → (𝐼‘((𝐸 + 𝐺)‘𝑌)) ∈ (Base‘𝑆))
48	44, 46, 22, 47	syl3anc 1398	. . . . . . . 8 ⊢ (𝜑 → (𝐼‘((𝐸 + 𝐺)‘𝑌)) ∈ (Base‘𝑆))
49	40, 9	ringcl 20327	. . . . . . . 8 ⊢ ((𝑆 ∈ Ring ∧ ((𝐸 + 𝐺)‘𝑋) ∈ (Base‘𝑆) ∧ (𝐼‘((𝐸 + 𝐺)‘𝑌)) ∈ (Base‘𝑆)) → (((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) ∈ (Base‘𝑆))
50	38, 42, 48, 49	syl3anc 1398	. . . . . . 7 ⊢ (𝜑 → (((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) ∈ (Base‘𝑆))
51	50	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ (𝑋 ∈ ( ⊥ ‘{𝐵}) ∧ 𝑌 ∈ ( ⊥ ‘{𝐵}))) → (((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) ∈ (Base‘𝑆))
52		simprr 784	. . . . . 6 ⊢ ((𝜑 ∧ (𝑋 ∈ ( ⊥ ‘{𝐵}) ∧ 𝑌 ∈ ( ⊥ ‘{𝐵}))) → 𝑌 ∈ ( ⊥ ‘{𝐵}))
53	8, 7, 40, 32	lssvscl 21076	. . . . . 6 ⊢ (((𝑈 ∈ LMod ∧ ( ⊥ ‘{𝐵}) ∈ (LSubSp‘𝑈)) ∧ ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) ∈ (Base‘𝑆) ∧ 𝑌 ∈ ( ⊥ ‘{𝐵}))) → ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌) ∈ ( ⊥ ‘{𝐵}))
54	30, 35, 51, 52, 53	syl22anc 851	. . . . 5 ⊢ ((𝜑 ∧ (𝑋 ∈ ( ⊥ ‘{𝐵}) ∧ 𝑌 ∈ ( ⊥ ‘{𝐵}))) → ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌) ∈ ( ⊥ ‘{𝐵}))
55	12, 32	lssvsubcl 21065	. . . . 5 ⊢ (((𝑈 ∈ LMod ∧ ( ⊥ ‘{𝐵}) ∈ (LSubSp‘𝑈)) ∧ (𝑋 ∈ ( ⊥ ‘{𝐵}) ∧ ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌) ∈ ( ⊥ ‘{𝐵}))) → (𝑋 − ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌)) ∈ ( ⊥ ‘{𝐵}))
56	30, 35, 36, 54, 55	syl22anc 851	. . . 4 ⊢ ((𝜑 ∧ (𝑋 ∈ ( ⊥ ‘{𝐵}) ∧ 𝑌 ∈ ( ⊥ ‘{𝐵}))) → (𝑋 − ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌)) ∈ ( ⊥ ‘{𝐵}))
57	21, 56	eqeltrid 2867	. . 3 ⊢ ((𝜑 ∧ (𝑋 ∈ ( ⊥ ‘{𝐵}) ∧ 𝑌 ∈ ( ⊥ ‘{𝐵}))) → 𝐵 ∈ ( ⊥ ‘{𝐵}))
58	28, 57	mtand 827	. 2 ⊢ (𝜑 → ¬ (𝑋 ∈ ( ⊥ ‘{𝐵}) ∧ 𝑌 ∈ ( ⊥ ‘{𝐵})))
59		ianor 997	. 2 ⊢ (¬ (𝑋 ∈ ( ⊥ ‘{𝐵}) ∧ 𝑌 ∈ ( ⊥ ‘{𝐵})) ↔ (¬ 𝑋 ∈ ( ⊥ ‘{𝐵}) ∨ ¬ 𝑌 ∈ ( ⊥ ‘{𝐵})))
60	58, 59	sylib 221	1 ⊢ (𝜑 → (¬ 𝑋 ∈ ( ⊥ ‘{𝐵}) ∨ ¬ 𝑌 ∈ ( ⊥ ‘{𝐵})))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 400 ∨ wo 860 = wceq 1570 ∈ wcel 2143 ≠ wne 2958 ∖ cdif 3902 ⊆ wss 3905 {csn 4589 ‘cfv 6536 (class class class)co 7410 Basecbs 17264 +_gcplusg 17305 ._rcmulr 17306 Scalarcsca 17308 ·_𝑠 cvsca 17309 0_gc0g 17487 -_gcsg 18997 LSSumclsm 19699 Ringcrg 20310 inv_rcinvr 20465 DivRingcdr 20827 LModclmod 20981 LSubSpclss 21052 LSpanclspn 21092 LVecclvec 21223 LFnlclfn 39851 LKerclk 39879 LDualcld 39917 HLchlt 40144 LHypclh 40778 DVecHcdvh 41872 ocHcoch 42141

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-rep 5238 ax-sep 5257 ax-nul 5269 ax-pow 5336 ax-pr 5404 ax-un 7732 ax-cnex 11151 ax-resscn 11152 ax-1cn 11153 ax-icn 11154 ax-addcl 11155 ax-addrcl 11156 ax-mulcl 11157 ax-mulrcl 11158 ax-mulcom 11159 ax-addass 11160 ax-mulass 11161 ax-distr 11162 ax-i2m1 11163 ax-1ne0 11164 ax-1rid 11165 ax-rnegex 11166 ax-rrecex 11167 ax-cnre 11168 ax-pre-lttri 11169 ax-pre-lttrn 11170 ax-pre-ltadd 11171 ax-pre-mulgt0 11172 ax-riotaBAD 39747

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-nel 3065 df-ral 3080 df-rex 3090 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4488 df-pw 4564 df-sn 4590 df-pr 4592 df-tp 4594 df-op 4596 df-uni 4873 df-int 4913 df-iun 4958 df-iin 4959 df-br 5110 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5556 df-eprel 5561 df-po 5569 df-so 5570 df-fr 5614 df-we 5616 df-xp 5667 df-rel 5668 df-cnv 5669 df-co 5670 df-dm 5671 df-rn 5672 df-res 5673 df-ima 5674 df-pred 6302 df-ord 6363 df-on 6364 df-lim 6365 df-suc 6366 df-iota 6492 df-fun 6538 df-fn 6539 df-f 6540 df-f1 6541 df-fo 6542 df-f1o 6543 df-fv 6544 df-riota 7367 df-ov 7413 df-oprab 7414 df-mpo 7415 df-of 7674 df-om 7859 df-1st 7982 df-2nd 7983 df-tpos 8218 df-undef 8265 df-frecs 8274 df-wrecs 8305 df-recs 8354 df-rdg 8393 df-1o 8449 df-er 8690 df-map 8822 df-en 8940 df-dom 8941 df-sdom 8942 df-fin 8943 df-pnf 11240 df-mnf 11241 df-xr 11242 df-ltxr 11243 df-le 11244 df-sub 11438 df-neg 11439 df-nn 12229 df-2 12298 df-3 12299 df-4 12300 df-5 12301 df-6 12302 df-n0 12500 df-z 12587 df-uz 12858 df-fz 13531 df-struct 17202 df-sets 17219 df-slot 17237 df-ndx 17249 df-base 17265 df-ress 17286 df-plusg 17318 df-mulr 17319 df-sca 17321 df-vsca 17322 df-0g 17489 df-proset 18345 df-poset 18364 df-plt 18379 df-lub 18395 df-glb 18396 df-join 18397 df-meet 18398 df-p0 18474 df-p1 18475 df-lat 18483 df-clat 18550 df-mgm 18693 df-sgrp 18772 df-mnd 18788 df-submnd 18837 df-grp 18998 df-minusg 18999 df-sbg 19000 df-subg 19184 df-cntz 19382 df-lsm 19701 df-cmn 19847 df-abl 19848 df-mgp 20212 df-rng 20226 df-ur 20259 df-ring 20312 df-oppr 20415 df-dvdsr 20435 df-unit 20436 df-invr 20466 df-dvr 20479 df-drng 20829 df-lmod 20983 df-lss 21053 df-lsp 21093 df-lvec 21224 df-lsatoms 39770 df-lfl 39852 df-ldual 39918 df-oposet 39970 df-ol 39972 df-oml 39973 df-covers 40060 df-ats 40061 df-atl 40092 df-cvlat 40116 df-hlat 40145 df-llines 40292 df-lplanes 40293 df-lvols 40294 df-lines 40295 df-psubsp 40297 df-pmap 40298 df-padd 40590 df-lhyp 40782 df-laut 40783 df-ldil 40898 df-ltrn 40899 df-trl 40953 df-tendo 41549 df-edring 41551 df-disoa 41823 df-dvech 41873 df-dib 41933 df-dic 41967 df-dih 42023 df-doch 42142

This theorem is referenced by: lclkrlem2q 42317

W3C validator