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 42185

Description: Lemma for lclkr 42197. 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 2769	. . . 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 41773	. . . . . . 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 42183	. . . . . 6 ⊢ (𝜑 → (𝐵 ∈ 𝑉 ∧ ((𝐸 + 𝐺)‘𝐵) = 0 ))
24	23	simpld 499	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ 𝑉)
25		lclkrlem2o.bn	. . . . 5 ⊢ (𝜑 → 𝐵 ≠ (0_g‘𝑈))
26		eldifsn 4758	. . . . 5 ⊢ (𝐵 ∈ (𝑉 ∖ {(0_g‘𝑈)}) ↔ (𝐵 ∈ 𝑉 ∧ 𝐵 ≠ (0_g‘𝑈)))
27	24, 25, 26	sylanbrc 594	. . . 4 ⊢ (𝜑 → 𝐵 ∈ (𝑉 ∖ {(0_g‘𝑈)}))
28	1, 2, 3, 4, 5, 6, 27	dochnel 42057	. . 3 ⊢ (𝜑 → ¬ 𝐵 ∈ ( ⊥ ‘{𝐵}))
29	1, 3, 6	dvhlmod 41774	. . . . . 6 ⊢ (𝜑 → 𝑈 ∈ LMod)
30	29	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ (𝑋 ∈ ( ⊥ ‘{𝐵}) ∧ 𝑌 ∈ ( ⊥ ‘{𝐵}))) → 𝑈 ∈ LMod)
31	24	snssd 4757	. . . . . . 7 ⊢ (𝜑 → {𝐵} ⊆ 𝑉)
32		eqid 2769	. . . . . . . 8 ⊢ (LSubSp‘𝑈) = (LSubSp‘𝑈)
33	1, 3, 4, 32, 2	dochlss 42018	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ {𝐵} ⊆ 𝑉) → ( ⊥ ‘{𝐵}) ∈ (LSubSp‘𝑈))
34	6, 31, 33	syl2anc 595	. . . . . 6 ⊢ (𝜑 → ( ⊥ ‘{𝐵}) ∈ (LSubSp‘𝑈))
35	34	adantr 485	. . . . 5 ⊢ ((𝜑 ∧ (𝑋 ∈ ( ⊥ ‘{𝐵}) ∧ 𝑌 ∈ ( ⊥ ‘{𝐵}))) → ( ⊥ ‘{𝐵}) ∈ (LSubSp‘𝑈))
36		simprl 782	. . . . 5 ⊢ ((𝜑 ∧ (𝑋 ∈ ( ⊥ ‘{𝐵}) ∧ 𝑌 ∈ ( ⊥ ‘{𝐵}))) → 𝑋 ∈ ( ⊥ ‘{𝐵}))
37	8	lmodring 20967	. . . . . . . . 9 ⊢ (𝑈 ∈ LMod → 𝑆 ∈ Ring)
38	29, 37	syl 18	. . . . . . . 8 ⊢ (𝜑 → 𝑆 ∈ Ring)
39	13, 14, 15, 29, 18, 19	ldualvaddcl 39794	. . . . . . . . 9 ⊢ (𝜑 → (𝐸 + 𝐺) ∈ 𝐹)
40		eqid 2769	. . . . . . . . . 10 ⊢ (Base‘𝑆) = (Base‘𝑆)
41	8, 40, 4, 13	lflcl 39728	. . . . . . . . 9 ⊢ ((𝑈 ∈ LMod ∧ (𝐸 + 𝐺) ∈ 𝐹 ∧ 𝑋 ∈ 𝑉) → ((𝐸 + 𝐺)‘𝑋) ∈ (Base‘𝑆))
42	29, 39, 16, 41	syl3anc 1396	. . . . . . . 8 ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝑋) ∈ (Base‘𝑆))
43	8	lvecdrng 21204	. . . . . . . . . 10 ⊢ (𝑈 ∈ LVec → 𝑆 ∈ DivRing)
44	20, 43	syl 18	. . . . . . . . 9 ⊢ (𝜑 → 𝑆 ∈ DivRing)
45	8, 40, 4, 13	lflcl 39728	. . . . . . . . . 10 ⊢ ((𝑈 ∈ LMod ∧ (𝐸 + 𝐺) ∈ 𝐹 ∧ 𝑌 ∈ 𝑉) → ((𝐸 + 𝐺)‘𝑌) ∈ (Base‘𝑆))
46	29, 39, 17, 45	syl3anc 1396	. . . . . . . . 9 ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝑌) ∈ (Base‘𝑆))
47	40, 10, 11	drnginvrcl 20836	. . . . . . . . 9 ⊢ ((𝑆 ∈ DivRing ∧ ((𝐸 + 𝐺)‘𝑌) ∈ (Base‘𝑆) ∧ ((𝐸 + 𝐺)‘𝑌) ≠ 0 ) → (𝐼‘((𝐸 + 𝐺)‘𝑌)) ∈ (Base‘𝑆))
48	44, 46, 22, 47	syl3anc 1396	. . . . . . . 8 ⊢ (𝜑 → (𝐼‘((𝐸 + 𝐺)‘𝑌)) ∈ (Base‘𝑆))
49	40, 9	ringcl 20332	. . . . . . . 8 ⊢ ((𝑆 ∈ Ring ∧ ((𝐸 + 𝐺)‘𝑋) ∈ (Base‘𝑆) ∧ (𝐼‘((𝐸 + 𝐺)‘𝑌)) ∈ (Base‘𝑆)) → (((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) ∈ (Base‘𝑆))
50	38, 42, 48, 49	syl3anc 1396	. . . . . . 7 ⊢ (𝜑 → (((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) ∈ (Base‘𝑆))
51	50	adantr 485	. . . . . 6 ⊢ ((𝜑 ∧ (𝑋 ∈ ( ⊥ ‘{𝐵}) ∧ 𝑌 ∈ ( ⊥ ‘{𝐵}))) → (((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) ∈ (Base‘𝑆))
52		simprr 784	. . . . . 6 ⊢ ((𝜑 ∧ (𝑋 ∈ ( ⊥ ‘{𝐵}) ∧ 𝑌 ∈ ( ⊥ ‘{𝐵}))) → 𝑌 ∈ ( ⊥ ‘{𝐵}))
53	8, 7, 40, 32	lssvscl 21054	. . . . . 6 ⊢ (((𝑈 ∈ LMod ∧ ( ⊥ ‘{𝐵}) ∈ (LSubSp‘𝑈)) ∧ ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) ∈ (Base‘𝑆) ∧ 𝑌 ∈ ( ⊥ ‘{𝐵}))) → ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌) ∈ ( ⊥ ‘{𝐵}))
54	30, 35, 51, 52, 53	syl22anc 851	. . . . 5 ⊢ ((𝜑 ∧ (𝑋 ∈ ( ⊥ ‘{𝐵}) ∧ 𝑌 ∈ ( ⊥ ‘{𝐵}))) → ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌) ∈ ( ⊥ ‘{𝐵}))
55	12, 32	lssvsubcl 21043	. . . . 5 ⊢ (((𝑈 ∈ LMod ∧ ( ⊥ ‘{𝐵}) ∈ (LSubSp‘𝑈)) ∧ (𝑋 ∈ ( ⊥ ‘{𝐵}) ∧ ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌) ∈ ( ⊥ ‘{𝐵}))) → (𝑋 − ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌)) ∈ ( ⊥ ‘{𝐵}))
56	30, 35, 36, 54, 55	syl22anc 851	. . . 4 ⊢ ((𝜑 ∧ (𝑋 ∈ ( ⊥ ‘{𝐵}) ∧ 𝑌 ∈ ( ⊥ ‘{𝐵}))) → (𝑋 − ((((𝐸 + 𝐺)‘𝑋) × (𝐼‘((𝐸 + 𝐺)‘𝑌))) · 𝑌)) ∈ ( ⊥ ‘{𝐵}))
57	21, 56	eqeltrid 2873	. . 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 1567 ∈ wcel 2149 ≠ wne 2964 ∖ cdif 3910 ⊆ wss 3913 {csn 4594 ‘cfv 6537 (class class class)co 7411 Basecbs 17269 +_gcplusg 17310 ._rcmulr 17311 Scalarcsca 17313 ·_𝑠 cvsca 17314 0_gc0g 17492 -_gcsg 19002 LSSumclsm 19704 Ringcrg 20315 inv_rcinvr 20469 DivRingcdr 20813 LModclmod 20959 LSubSpclss 21030 LSpanclspn 21070 LVecclvec 21201 LFnlclfn 39721 LKerclk 39749 LDualcld 39787 HLchlt 40014 LHypclh 40648 DVecHcdvh 41742 ocHcoch 42011

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1822 ax-4 1836 ax-5 1937 ax-6 1994 ax-7 2035 ax-8 2151 ax-9 2159 ax-10 2182 ax-11 2198 ax-12 2219 ax-ext 2741 ax-rep 5242 ax-sep 5261 ax-nul 5271 ax-pow 5337 ax-pr 5405 ax-un 7733 ax-cnex 11156 ax-resscn 11157 ax-1cn 11158 ax-icn 11159 ax-addcl 11160 ax-addrcl 11161 ax-mulcl 11162 ax-mulrcl 11163 ax-mulcom 11164 ax-addass 11165 ax-mulass 11166 ax-distr 11167 ax-i2m1 11168 ax-1ne0 11169 ax-1rid 11170 ax-rnegex 11171 ax-rrecex 11172 ax-cnre 11173 ax-pre-lttri 11174 ax-pre-lttrn 11175 ax-pre-ltadd 11176 ax-pre-mulgt0 11177 ax-riotaBAD 39617

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1102 df-3an 1103 df-tru 1570 df-fal 1580 df-ex 1807 df-nf 1811 df-sb 2098 df-mo 2573 df-eu 2603 df-clab 2748 df-cleq 2761 df-clel 2844 df-nfc 2918 df-ne 2965 df-nel 3071 df-ral 3086 df-rex 3096 df-rmo 3376 df-reu 3377 df-rab 3424 df-v 3465 df-sbc 3754 df-csb 3862 df-dif 3916 df-un 3918 df-in 3920 df-ss 3930 df-pss 3933 df-nul 4295 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-tp 4599 df-op 4601 df-uni 4877 df-int 4917 df-iun 4962 df-iin 4963 df-br 5114 df-opab 5178 df-mpt 5197 df-tr 5223 df-id 5557 df-eprel 5562 df-po 5570 df-so 5571 df-fr 5615 df-we 5617 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-res 5674 df-ima 5675 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7368 df-ov 7414 df-oprab 7415 df-mpo 7416 df-of 7675 df-om 7863 df-1st 7986 df-2nd 7987 df-tpos 8222 df-undef 8269 df-frecs 8278 df-wrecs 8309 df-recs 8358 df-rdg 8397 df-1o 8453 df-er 8694 df-map 8826 df-en 8944 df-dom 8945 df-sdom 8946 df-fin 8947 df-pnf 11245 df-mnf 11246 df-xr 11247 df-ltxr 11248 df-le 11249 df-sub 11443 df-neg 11444 df-nn 12234 df-2 12303 df-3 12304 df-4 12305 df-5 12306 df-6 12307 df-n0 12505 df-z 12592 df-uz 12863 df-fz 13536 df-struct 17207 df-sets 17224 df-slot 17242 df-ndx 17254 df-base 17270 df-ress 17291 df-plusg 17323 df-mulr 17324 df-sca 17326 df-vsca 17327 df-0g 17494 df-proset 18350 df-poset 18369 df-plt 18384 df-lub 18400 df-glb 18401 df-join 18402 df-meet 18403 df-p0 18479 df-p1 18480 df-lat 18488 df-clat 18555 df-mgm 18698 df-sgrp 18777 df-mnd 18793 df-submnd 18842 df-grp 19003 df-minusg 19004 df-sbg 19005 df-subg 19189 df-cntz 19387 df-lsm 19706 df-cmn 19852 df-abl 19853 df-mgp 20217 df-rng 20231 df-ur 20264 df-ring 20317 df-oppr 20419 df-dvdsr 20439 df-unit 20440 df-invr 20470 df-dvr 20483 df-drng 20815 df-lmod 20961 df-lss 21031 df-lsp 21071 df-lvec 21202 df-lsatoms 39640 df-lfl 39722 df-ldual 39788 df-oposet 39840 df-ol 39842 df-oml 39843 df-covers 39930 df-ats 39931 df-atl 39962 df-cvlat 39986 df-hlat 40015 df-llines 40162 df-lplanes 40163 df-lvols 40164 df-lines 40165 df-psubsp 40167 df-pmap 40168 df-padd 40460 df-lhyp 40652 df-laut 40653 df-ldil 40768 df-ltrn 40769 df-trl 40823 df-tendo 41419 df-edring 41421 df-disoa 41693 df-dvech 41743 df-dib 41803 df-dic 41837 df-dih 41893 df-doch 42012

This theorem is referenced by: lclkrlem2q 42187

W3C validator