lclkrlem2g - Mathbox for Norm Megill

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

Theorem lclkrlem2g 42172

Description: Lemma for lclkr 42192. Comparable hyperplanes are equal, so the kernel of the sum is closed. (Contributed by NM, 16-Jan-2015.)

**Hypotheses**
Ref	Expression
lclkrlem2f.h	⊢ 𝐻 = (LHyp‘𝐾)
lclkrlem2f.o	⊢ ⊥ = ((ocH‘𝐾)‘𝑊)
lclkrlem2f.u	⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
lclkrlem2f.v	⊢ 𝑉 = (Base‘𝑈)
lclkrlem2f.s	⊢ 𝑆 = (Scalar‘𝑈)
lclkrlem2f.q	⊢ 𝑄 = (0_g‘𝑆)
lclkrlem2f.z	⊢ 0 = (0_g‘𝑈)
lclkrlem2f.a	⊢ ⊕ = (LSSum‘𝑈)
lclkrlem2f.n	⊢ 𝑁 = (LSpan‘𝑈)
lclkrlem2f.f	⊢ 𝐹 = (LFnl‘𝑈)
lclkrlem2f.j	⊢ 𝐽 = (LSHyp‘𝑈)
lclkrlem2f.l	⊢ 𝐿 = (LKer‘𝑈)
lclkrlem2f.d	⊢ 𝐷 = (LDual‘𝑈)
lclkrlem2f.p	⊢ + = (+_g‘𝐷)
lclkrlem2f.k	⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
lclkrlem2f.b	⊢ (𝜑 → 𝐵 ∈ (𝑉 ∖ { 0 }))
lclkrlem2f.e	⊢ (𝜑 → 𝐸 ∈ 𝐹)
lclkrlem2f.g	⊢ (𝜑 → 𝐺 ∈ 𝐹)
lclkrlem2f.le	⊢ (𝜑 → (𝐿‘𝐸) = ( ⊥ ‘{𝑋}))
lclkrlem2f.lg	⊢ (𝜑 → (𝐿‘𝐺) = ( ⊥ ‘{𝑌}))
lclkrlem2f.kb	⊢ (𝜑 → ((𝐸 + 𝐺)‘𝐵) = 𝑄)
lclkrlem2f.nx	⊢ (𝜑 → (¬ 𝑋 ∈ ( ⊥ ‘{𝐵}) ∨ ¬ 𝑌 ∈ ( ⊥ ‘{𝐵})))
lclkrlem2f.x	⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))
lclkrlem2f.y	⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))
lclkrlem2f.ne	⊢ (𝜑 → (𝐿‘𝐸) ≠ (𝐿‘𝐺))
lclkrlem2f.lp	⊢ (𝜑 → (𝐿‘(𝐸 + 𝐺)) ∈ 𝐽)

**Assertion**
Ref	Expression
lclkrlem2g	⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘(𝐸 + 𝐺)))) = (𝐿‘(𝐸 + 𝐺)))

**Proof of Theorem lclkrlem2g**
Step	Hyp	Ref	Expression
1		lclkrlem2f.h	. . . . 5 ⊢ 𝐻 = (LHyp‘𝐾)
2		lclkrlem2f.o	. . . . 5 ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)
3		lclkrlem2f.u	. . . . 5 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
4		lclkrlem2f.v	. . . . 5 ⊢ 𝑉 = (Base‘𝑈)
5		lclkrlem2f.s	. . . . 5 ⊢ 𝑆 = (Scalar‘𝑈)
6		lclkrlem2f.q	. . . . 5 ⊢ 𝑄 = (0_g‘𝑆)
7		lclkrlem2f.z	. . . . 5 ⊢ 0 = (0_g‘𝑈)
8		lclkrlem2f.a	. . . . 5 ⊢ ⊕ = (LSSum‘𝑈)
9		lclkrlem2f.n	. . . . 5 ⊢ 𝑁 = (LSpan‘𝑈)
10		lclkrlem2f.f	. . . . 5 ⊢ 𝐹 = (LFnl‘𝑈)
11		lclkrlem2f.j	. . . . 5 ⊢ 𝐽 = (LSHyp‘𝑈)
12		lclkrlem2f.l	. . . . 5 ⊢ 𝐿 = (LKer‘𝑈)
13		lclkrlem2f.d	. . . . 5 ⊢ 𝐷 = (LDual‘𝑈)
14		lclkrlem2f.p	. . . . 5 ⊢ + = (+_g‘𝐷)
15		lclkrlem2f.k	. . . . 5 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
16		lclkrlem2f.b	. . . . 5 ⊢ (𝜑 → 𝐵 ∈ (𝑉 ∖ { 0 }))
17		lclkrlem2f.e	. . . . 5 ⊢ (𝜑 → 𝐸 ∈ 𝐹)
18		lclkrlem2f.g	. . . . 5 ⊢ (𝜑 → 𝐺 ∈ 𝐹)
19		lclkrlem2f.le	. . . . 5 ⊢ (𝜑 → (𝐿‘𝐸) = ( ⊥ ‘{𝑋}))
20		lclkrlem2f.lg	. . . . 5 ⊢ (𝜑 → (𝐿‘𝐺) = ( ⊥ ‘{𝑌}))
21		lclkrlem2f.kb	. . . . 5 ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝐵) = 𝑄)
22		lclkrlem2f.nx	. . . . 5 ⊢ (𝜑 → (¬ 𝑋 ∈ ( ⊥ ‘{𝐵}) ∨ ¬ 𝑌 ∈ ( ⊥ ‘{𝐵})))
23		lclkrlem2f.x	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))
24		lclkrlem2f.y	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))
25		lclkrlem2f.ne	. . . . 5 ⊢ (𝜑 → (𝐿‘𝐸) ≠ (𝐿‘𝐺))
26		lclkrlem2f.lp	. . . . 5 ⊢ (𝜑 → (𝐿‘(𝐸 + 𝐺)) ∈ 𝐽)
27	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26	lclkrlem2f 42171	. . . 4 ⊢ (𝜑 → (((𝐿‘𝐸) ∩ (𝐿‘𝐺)) ⊕ (𝑁‘{𝐵})) ⊆ (𝐿‘(𝐸 + 𝐺)))
28	1, 3, 15	dvhlvec 41768	. . . . 5 ⊢ (𝜑 → 𝑈 ∈ LVec)
29	19, 20	ineq12d 4182	. . . . . . 7 ⊢ (𝜑 → ((𝐿‘𝐸) ∩ (𝐿‘𝐺)) = (( ⊥ ‘{𝑋}) ∩ ( ⊥ ‘{𝑌})))
30	29	oveq1d 7423	. . . . . 6 ⊢ (𝜑 → (((𝐿‘𝐸) ∩ (𝐿‘𝐺)) ⊕ (𝑁‘{𝐵})) = ((( ⊥ ‘{𝑋}) ∩ ( ⊥ ‘{𝑌})) ⊕ (𝑁‘{𝐵})))
31		eqid 2769	. . . . . . 7 ⊢ (LSAtoms‘𝑈) = (LSAtoms‘𝑈)
32	25, 19, 20	3netr3d 3040	. . . . . . 7 ⊢ (𝜑 → ( ⊥ ‘{𝑋}) ≠ ( ⊥ ‘{𝑌}))
33	1, 2, 3, 4, 7, 8, 9, 31, 15, 16, 23, 24, 32, 22, 11	lclkrlem2c 42168	. . . . . 6 ⊢ (𝜑 → ((( ⊥ ‘{𝑋}) ∩ ( ⊥ ‘{𝑌})) ⊕ (𝑁‘{𝐵})) ∈ 𝐽)
34	30, 33	eqeltrd 2869	. . . . 5 ⊢ (𝜑 → (((𝐿‘𝐸) ∩ (𝐿‘𝐺)) ⊕ (𝑁‘{𝐵})) ∈ 𝐽)
35	11, 28, 34, 26	lshpcmp 39647	. . . 4 ⊢ (𝜑 → ((((𝐿‘𝐸) ∩ (𝐿‘𝐺)) ⊕ (𝑁‘{𝐵})) ⊆ (𝐿‘(𝐸 + 𝐺)) ↔ (((𝐿‘𝐸) ∩ (𝐿‘𝐺)) ⊕ (𝑁‘{𝐵})) = (𝐿‘(𝐸 + 𝐺))))
36	27, 35	mpbid 235	. . 3 ⊢ (𝜑 → (((𝐿‘𝐸) ∩ (𝐿‘𝐺)) ⊕ (𝑁‘{𝐵})) = (𝐿‘(𝐸 + 𝐺)))
37		eqid 2769	. . . . 5 ⊢ ((DIsoH‘𝐾)‘𝑊) = ((DIsoH‘𝐾)‘𝑊)
38	1, 2, 3, 4, 7, 8, 9, 31, 15, 16, 23, 24, 32, 22, 37	lclkrlem2d 42169	. . . 4 ⊢ (𝜑 → ((( ⊥ ‘{𝑋}) ∩ ( ⊥ ‘{𝑌})) ⊕ (𝑁‘{𝐵})) ∈ ran ((DIsoH‘𝐾)‘𝑊))
39	30, 38	eqeltrd 2869	. . 3 ⊢ (𝜑 → (((𝐿‘𝐸) ∩ (𝐿‘𝐺)) ⊕ (𝑁‘{𝐵})) ∈ ran ((DIsoH‘𝐾)‘𝑊))
40	36, 39	eqeltrrd 2870	. 2 ⊢ (𝜑 → (𝐿‘(𝐸 + 𝐺)) ∈ ran ((DIsoH‘𝐾)‘𝑊))
41	1, 3, 37, 4	dihrnss 41937	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐿‘(𝐸 + 𝐺)) ∈ ran ((DIsoH‘𝐾)‘𝑊)) → (𝐿‘(𝐸 + 𝐺)) ⊆ 𝑉)
42	15, 40, 41	syl2anc 595	. . 3 ⊢ (𝜑 → (𝐿‘(𝐸 + 𝐺)) ⊆ 𝑉)
43	1, 37, 3, 4, 2, 15, 42	dochoccl 42028	. 2 ⊢ (𝜑 → ((𝐿‘(𝐸 + 𝐺)) ∈ ran ((DIsoH‘𝐾)‘𝑊) ↔ ( ⊥ ‘( ⊥ ‘(𝐿‘(𝐸 + 𝐺)))) = (𝐿‘(𝐸 + 𝐺))))
44	40, 43	mpbid 235	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 ∩ cin 3912 ⊆ wss 3913 {csn 4591 ran crn 5660 ‘cfv 6533 (class class class)co 7408 Basecbs 17265 +_gcplusg 17306 Scalarcsca 17309 0_gc0g 17488 LSSumclsm 19700 LSpanclspn 21066 LSAtomsclsa 39633 LSHypclsh 39634 LFnlclfn 39716 LKerclk 39744 LDualcld 39782 HLchlt 40009 LHypclh 40643 DVecHcdvh 41737 DIsoHcdih 41887 ocHcoch 42006

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 5239 ax-sep 5258 ax-nul 5268 ax-pow 5334 ax-pr 5402 ax-un 7730 ax-cnex 11152 ax-resscn 11153 ax-1cn 11154 ax-icn 11155 ax-addcl 11156 ax-addrcl 11157 ax-mulcl 11158 ax-mulrcl 11159 ax-mulcom 11160 ax-addass 11161 ax-mulass 11162 ax-distr 11163 ax-i2m1 11164 ax-1ne0 11165 ax-1rid 11166 ax-rnegex 11167 ax-rrecex 11168 ax-cnre 11169 ax-pre-lttri 11170 ax-pre-lttrn 11171 ax-pre-ltadd 11172 ax-pre-mulgt0 11173 ax-riotaBAD 39612

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 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-tp 4596 df-op 4598 df-uni 4874 df-int 4914 df-iun 4959 df-iin 4960 df-br 5111 df-opab 5175 df-mpt 5194 df-tr 5220 df-id 5554 df-eprel 5559 df-po 5567 df-so 5568 df-fr 5612 df-we 5614 df-xp 5665 df-rel 5666 df-cnv 5667 df-co 5668 df-dm 5669 df-rn 5670 df-res 5671 df-ima 5672 df-pred 6299 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-riota 7365 df-ov 7411 df-oprab 7412 df-mpo 7413 df-of 7672 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-2o 8450 df-er 8690 df-map 8822 df-en 8940 df-dom 8941 df-sdom 8942 df-fin 8943 df-pnf 11241 df-mnf 11242 df-xr 11243 df-ltxr 11244 df-le 11245 df-sub 11439 df-neg 11440 df-nn 12230 df-2 12299 df-3 12300 df-4 12301 df-5 12302 df-6 12303 df-n0 12501 df-z 12588 df-uz 12859 df-fz 13532 df-struct 17203 df-sets 17220 df-slot 17238 df-ndx 17250 df-base 17266 df-ress 17287 df-plusg 17319 df-mulr 17320 df-sca 17322 df-vsca 17323 df-0g 17490 df-mre 17634 df-mrc 17635 df-acs 17637 df-proset 18346 df-poset 18365 df-plt 18380 df-lub 18396 df-glb 18397 df-join 18398 df-meet 18399 df-p0 18475 df-p1 18476 df-lat 18484 df-clat 18551 df-mgm 18694 df-sgrp 18773 df-mnd 18789 df-submnd 18838 df-grp 18999 df-minusg 19000 df-sbg 19001 df-subg 19185 df-cntz 19383 df-oppg 19412 df-lsm 19702 df-cmn 19848 df-abl 19849 df-mgp 20213 df-rng 20227 df-ur 20260 df-ring 20313 df-oppr 20415 df-dvdsr 20435 df-unit 20436 df-invr 20466 df-dvr 20479 df-drng 20811 df-lmod 20957 df-lss 21027 df-lsp 21067 df-lvec 21198 df-lsatoms 39635 df-lshyp 39636 df-lcv 39678 df-lfl 39717 df-lkr 39745 df-ldual 39783 df-oposet 39835 df-ol 39837 df-oml 39838 df-covers 39925 df-ats 39926 df-atl 39957 df-cvlat 39981 df-hlat 40010 df-llines 40157 df-lplanes 40158 df-lvols 40159 df-lines 40160 df-psubsp 40162 df-pmap 40163 df-padd 40455 df-lhyp 40647 df-laut 40648 df-ldil 40763 df-ltrn 40764 df-trl 40818 df-tgrp 41402 df-tendo 41414 df-edring 41416 df-dveca 41662 df-disoa 41688 df-dvech 41738 df-dib 41798 df-dic 41832 df-dih 41888 df-doch 42007 df-djh 42054

This theorem is referenced by: lclkrlem2h 42173

W3C validator