dochkrshp - Mathbox for Norm Megill

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

Theorem dochkrshp 35492

Description: The closure of a kernel is a hyperplane iff it doesn't contain all vectors. (Contributed by NM, 1-Nov-2014.)

**Hypotheses**
Ref	Expression
dochkrshp.h	⊢ 𝐻 = (LHyp‘𝐾)
dochkrshp.o	⊢ ⊥ = ((ocH‘𝐾)‘𝑊)
dochkrshp.u	⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
dochkrshp.v	⊢ 𝑉 = (Base‘𝑈)
dochkrshp.y	⊢ 𝑌 = (LSHyp‘𝑈)
dochkrshp.f	⊢ 𝐹 = (LFnl‘𝑈)
dochkrshp.l	⊢ 𝐿 = (LKer‘𝑈)
dochkrshp.k	⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
dochkrshp.g	⊢ (𝜑 → 𝐺 ∈ 𝐹)

**Assertion**
Ref	Expression
dochkrshp	⊢ (𝜑 → (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ≠ 𝑉 ↔ ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ∈ 𝑌))

**Proof of Theorem dochkrshp**
Step	Hyp	Ref	Expression
1		simpr 475	. . . . . . 7 ⊢ ((𝜑 ∧ ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ≠ (𝐿‘𝐺)) → ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ≠ (𝐿‘𝐺))
2		dochkrshp.h	. . . . . . . 8 ⊢ 𝐻 = (LHyp‘𝐾)
3		dochkrshp.o	. . . . . . . 8 ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)
4		dochkrshp.u	. . . . . . . 8 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
5		dochkrshp.v	. . . . . . . 8 ⊢ 𝑉 = (Base‘𝑈)
6		dochkrshp.y	. . . . . . . 8 ⊢ 𝑌 = (LSHyp‘𝑈)
7		dochkrshp.k	. . . . . . . . 9 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
8	7	adantr 479	. . . . . . . 8 ⊢ ((𝜑 ∧ ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ≠ (𝐿‘𝐺)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
9		fveq2 6084	. . . . . . . . . . . . . . 15 ⊢ ((𝐿‘𝐺) = 𝑉 → ( ⊥ ‘(𝐿‘𝐺)) = ( ⊥ ‘𝑉))
10	9	fveq2d 6088	. . . . . . . . . . . . . 14 ⊢ ((𝐿‘𝐺) = 𝑉 → ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = ( ⊥ ‘( ⊥ ‘𝑉)))
11	2, 4, 3, 5, 7	dochoc1 35467	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘𝑉)) = 𝑉)
12	10, 11	sylan9eqr 2661	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐿‘𝐺) = 𝑉) → ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = 𝑉)
13		simpr 475	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝐿‘𝐺) = 𝑉) → (𝐿‘𝐺) = 𝑉)
14	12, 13	eqtr4d 2642	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝐿‘𝐺) = 𝑉) → ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺))
15	14	ex 448	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐿‘𝐺) = 𝑉 → ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺)))
16	15	necon3d 2798	. . . . . . . . . 10 ⊢ (𝜑 → (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ≠ (𝐿‘𝐺) → (𝐿‘𝐺) ≠ 𝑉))
17		df-ne 2777	. . . . . . . . . . 11 ⊢ ((𝐿‘𝐺) ≠ 𝑉 ↔ ¬ (𝐿‘𝐺) = 𝑉)
18		dochkrshp.f	. . . . . . . . . . . . . 14 ⊢ 𝐹 = (LFnl‘𝑈)
19		dochkrshp.l	. . . . . . . . . . . . . 14 ⊢ 𝐿 = (LKer‘𝑈)
20	2, 4, 7	dvhlvec 35215	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝑈 ∈ LVec)
21		dochkrshp.g	. . . . . . . . . . . . . 14 ⊢ (𝜑 → 𝐺 ∈ 𝐹)
22	5, 6, 18, 19, 20, 21	lkrshpor 33211	. . . . . . . . . . . . 13 ⊢ (𝜑 → ((𝐿‘𝐺) ∈ 𝑌 ∨ (𝐿‘𝐺) = 𝑉))
23	22	orcomd 401	. . . . . . . . . . . 12 ⊢ (𝜑 → ((𝐿‘𝐺) = 𝑉 ∨ (𝐿‘𝐺) ∈ 𝑌))
24	23	ord 390	. . . . . . . . . . 11 ⊢ (𝜑 → (¬ (𝐿‘𝐺) = 𝑉 → (𝐿‘𝐺) ∈ 𝑌))
25	17, 24	syl5bi 230	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐿‘𝐺) ≠ 𝑉 → (𝐿‘𝐺) ∈ 𝑌))
26	16, 25	syld 45	. . . . . . . . 9 ⊢ (𝜑 → (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ≠ (𝐿‘𝐺) → (𝐿‘𝐺) ∈ 𝑌))
27	26	imp 443	. . . . . . . 8 ⊢ ((𝜑 ∧ ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ≠ (𝐿‘𝐺)) → (𝐿‘𝐺) ∈ 𝑌)
28	2, 3, 4, 5, 6, 8, 27	dochshpncl 35490	. . . . . . 7 ⊢ ((𝜑 ∧ ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ≠ (𝐿‘𝐺)) → (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ≠ (𝐿‘𝐺) ↔ ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = 𝑉))
29	1, 28	mpbid 220	. . . . . 6 ⊢ ((𝜑 ∧ ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ≠ (𝐿‘𝐺)) → ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = 𝑉)
30	29	ex 448	. . . . 5 ⊢ (𝜑 → (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ≠ (𝐿‘𝐺) → ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = 𝑉))
31	30	necon1d 2799	. . . 4 ⊢ (𝜑 → (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ≠ 𝑉 → ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺)))
32	12	ex 448	. . . . . 6 ⊢ (𝜑 → ((𝐿‘𝐺) = 𝑉 → ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = 𝑉))
33	32	necon3ad 2790	. . . . 5 ⊢ (𝜑 → (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ≠ 𝑉 → ¬ (𝐿‘𝐺) = 𝑉))
34	33, 24	syld 45	. . . 4 ⊢ (𝜑 → (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ≠ 𝑉 → (𝐿‘𝐺) ∈ 𝑌))
35	31, 34	jcad 553	. . 3 ⊢ (𝜑 → (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ≠ 𝑉 → (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺) ∧ (𝐿‘𝐺) ∈ 𝑌)))
36	2, 3, 4, 18, 6, 19, 7, 21	dochlkr 35491	. . 3 ⊢ (𝜑 → (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ∈ 𝑌 ↔ (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) = (𝐿‘𝐺) ∧ (𝐿‘𝐺) ∈ 𝑌)))
37	35, 36	sylibrd 247	. 2 ⊢ (𝜑 → (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ≠ 𝑉 → ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ∈ 𝑌))
38	2, 4, 7	dvhlmod 35216	. . . . 5 ⊢ (𝜑 → 𝑈 ∈ LMod)
39	38	adantr 479	. . . 4 ⊢ ((𝜑 ∧ ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ∈ 𝑌) → 𝑈 ∈ LMod)
40		simpr 475	. . . 4 ⊢ ((𝜑 ∧ ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ∈ 𝑌) → ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ∈ 𝑌)
41	5, 6, 39, 40	lshpne 33086	. . 3 ⊢ ((𝜑 ∧ ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ∈ 𝑌) → ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ≠ 𝑉)
42	41	ex 448	. 2 ⊢ (𝜑 → (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ∈ 𝑌 → ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ≠ 𝑉))
43	37, 42	impbid 200	1 ⊢ (𝜑 → (( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ≠ 𝑉 ↔ ( ⊥ ‘( ⊥ ‘(𝐿‘𝐺))) ∈ 𝑌))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 194 ∧ wa 382 = wceq 1474 ∈ wcel 1975 ≠ wne 2775 ‘cfv 5786 Basecbs 15637 LModclmod 18628 LSHypclsh 33079 LFnlclfn 33161 LKerclk 33189 HLchlt 33454 LHypclh 34087 DVecHcdvh 35184 ocHcoch 35453

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1711 ax-4 1726 ax-5 1825 ax-6 1873 ax-7 1920 ax-8 1977 ax-9 1984 ax-10 2004 ax-11 2019 ax-12 2031 ax-13 2228 ax-ext 2585 ax-rep 4689 ax-sep 4699 ax-nul 4708 ax-pow 4760 ax-pr 4824 ax-un 6820 ax-cnex 9844 ax-resscn 9845 ax-1cn 9846 ax-icn 9847 ax-addcl 9848 ax-addrcl 9849 ax-mulcl 9850 ax-mulrcl 9851 ax-mulcom 9852 ax-addass 9853 ax-mulass 9854 ax-distr 9855 ax-i2m1 9856 ax-1ne0 9857 ax-1rid 9858 ax-rnegex 9859 ax-rrecex 9860 ax-cnre 9861 ax-pre-lttri 9862 ax-pre-lttrn 9863 ax-pre-ltadd 9864 ax-pre-mulgt0 9865 ax-riotaBAD 33056

This theorem depends on definitions: df-bi 195 df-or 383 df-an 384 df-3or 1031 df-3an 1032 df-tru 1477 df-fal 1480 df-ex 1695 df-nf 1700 df-sb 1866 df-eu 2457 df-mo 2458 df-clab 2592 df-cleq 2598 df-clel 2601 df-nfc 2735 df-ne 2777 df-nel 2778 df-ral 2896 df-rex 2897 df-reu 2898 df-rmo 2899 df-rab 2900 df-v 3170 df-sbc 3398 df-csb 3495 df-dif 3538 df-un 3540 df-in 3542 df-ss 3549 df-pss 3551 df-nul 3870 df-if 4032 df-pw 4105 df-sn 4121 df-pr 4123 df-tp 4125 df-op 4127 df-uni 4363 df-int 4401 df-iun 4447 df-iin 4448 df-br 4574 df-opab 4634 df-mpt 4635 df-tr 4671 df-eprel 4935 df-id 4939 df-po 4945 df-so 4946 df-fr 4983 df-we 4985 df-xp 5030 df-rel 5031 df-cnv 5032 df-co 5033 df-dm 5034 df-rn 5035 df-res 5036 df-ima 5037 df-pred 5579 df-ord 5625 df-on 5626 df-lim 5627 df-suc 5628 df-iota 5750 df-fun 5788 df-fn 5789 df-f 5790 df-f1 5791 df-fo 5792 df-f1o 5793 df-fv 5794 df-riota 6485 df-ov 6526 df-oprab 6527 df-mpt2 6528 df-om 6931 df-1st 7032 df-2nd 7033 df-tpos 7212 df-undef 7259 df-wrecs 7267 df-recs 7328 df-rdg 7366 df-1o 7420 df-oadd 7424 df-er 7602 df-map 7719 df-en 7815 df-dom 7816 df-sdom 7817 df-fin 7818 df-pnf 9928 df-mnf 9929 df-xr 9930 df-ltxr 9931 df-le 9932 df-sub 10115 df-neg 10116 df-nn 10864 df-2 10922 df-3 10923 df-4 10924 df-5 10925 df-6 10926 df-n0 11136 df-z 11207 df-uz 11516 df-fz 12149 df-struct 15639 df-ndx 15640 df-slot 15641 df-base 15642 df-sets 15643 df-ress 15644 df-plusg 15723 df-mulr 15724 df-sca 15726 df-vsca 15727 df-0g 15867 df-preset 16693 df-poset 16711 df-plt 16723 df-lub 16739 df-glb 16740 df-join 16741 df-meet 16742 df-p0 16804 df-p1 16805 df-lat 16811 df-clat 16873 df-mgm 17007 df-sgrp 17049 df-mnd 17060 df-submnd 17101 df-grp 17190 df-minusg 17191 df-sbg 17192 df-subg 17356 df-cntz 17515 df-lsm 17816 df-cmn 17960 df-abl 17961 df-mgp 18255 df-ur 18267 df-ring 18314 df-oppr 18388 df-dvdsr 18406 df-unit 18407 df-invr 18437 df-dvr 18448 df-drng 18514 df-lmod 18630 df-lss 18696 df-lsp 18735 df-lvec 18866 df-lsatoms 33080 df-lshyp 33081 df-lfl 33162 df-lkr 33190 df-oposet 33280 df-ol 33282 df-oml 33283 df-covers 33370 df-ats 33371 df-atl 33402 df-cvlat 33426 df-hlat 33455 df-llines 33601 df-lplanes 33602 df-lvols 33603 df-lines 33604 df-psubsp 33606 df-pmap 33607 df-padd 33899 df-lhyp 34091 df-laut 34092 df-ldil 34207 df-ltrn 34208 df-trl 34263 df-tendo 34860 df-edring 34862 df-disoa 35135 df-dvech 35185 df-dib 35245 df-dic 35279 df-dih 35335 df-doch 35454

This theorem is referenced by: dochkrshp2 35493 dochkrsat 35561

W3C validator