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 42098

Description: Lemma for lclkr 42118. 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 42097	. . . 4 ⊢ (𝜑 → (((𝐿‘𝐸) ∩ (𝐿‘𝐺)) ⊕ (𝑁‘{𝐵})) ⊆ (𝐿‘(𝐸 + 𝐺)))
28	1, 3, 15	dvhlvec 41694	. . . . 5 ⊢ (𝜑 → 𝑈 ∈ LVec)
29	19, 20	ineq12d 4171	. . . . . . 7 ⊢ (𝜑 → ((𝐿‘𝐸) ∩ (𝐿‘𝐺)) = (( ⊥ ‘{𝑋}) ∩ ( ⊥ ‘{𝑌})))
30	29	oveq1d 7406	. . . . . 6 ⊢ (𝜑 → (((𝐿‘𝐸) ∩ (𝐿‘𝐺)) ⊕ (𝑁‘{𝐵})) = ((( ⊥ ‘{𝑋}) ∩ ( ⊥ ‘{𝑌})) ⊕ (𝑁‘{𝐵})))
31		eqid 2761	. . . . . . 7 ⊢ (LSAtoms‘𝑈) = (LSAtoms‘𝑈)
32	25, 19, 20	3netr3d 3032	. . . . . . 7 ⊢ (𝜑 → ( ⊥ ‘{𝑋}) ≠ ( ⊥ ‘{𝑌}))
33	1, 2, 3, 4, 7, 8, 9, 31, 15, 16, 23, 24, 32, 22, 11	lclkrlem2c 42094	. . . . . 6 ⊢ (𝜑 → ((( ⊥ ‘{𝑋}) ∩ ( ⊥ ‘{𝑌})) ⊕ (𝑁‘{𝐵})) ∈ 𝐽)
34	30, 33	eqeltrd 2861	. . . . 5 ⊢ (𝜑 → (((𝐿‘𝐸) ∩ (𝐿‘𝐺)) ⊕ (𝑁‘{𝐵})) ∈ 𝐽)
35	11, 28, 34, 26	lshpcmp 39573	. . . 4 ⊢ (𝜑 → ((((𝐿‘𝐸) ∩ (𝐿‘𝐺)) ⊕ (𝑁‘{𝐵})) ⊆ (𝐿‘(𝐸 + 𝐺)) ↔ (((𝐿‘𝐸) ∩ (𝐿‘𝐺)) ⊕ (𝑁‘{𝐵})) = (𝐿‘(𝐸 + 𝐺))))
36	27, 35	mpbid 234	. . 3 ⊢ (𝜑 → (((𝐿‘𝐸) ∩ (𝐿‘𝐺)) ⊕ (𝑁‘{𝐵})) = (𝐿‘(𝐸 + 𝐺)))
37		eqid 2761	. . . . 5 ⊢ ((DIsoH‘𝐾)‘𝑊) = ((DIsoH‘𝐾)‘𝑊)
38	1, 2, 3, 4, 7, 8, 9, 31, 15, 16, 23, 24, 32, 22, 37	lclkrlem2d 42095	. . . 4 ⊢ (𝜑 → ((( ⊥ ‘{𝑋}) ∩ ( ⊥ ‘{𝑌})) ⊕ (𝑁‘{𝐵})) ∈ ran ((DIsoH‘𝐾)‘𝑊))
39	30, 38	eqeltrd 2861	. . 3 ⊢ (𝜑 → (((𝐿‘𝐸) ∩ (𝐿‘𝐺)) ⊕ (𝑁‘{𝐵})) ∈ ran ((DIsoH‘𝐾)‘𝑊))
40	36, 39	eqeltrrd 2862	. 2 ⊢ (𝜑 → (𝐿‘(𝐸 + 𝐺)) ∈ ran ((DIsoH‘𝐾)‘𝑊))
41	1, 3, 37, 4	dihrnss 41863	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐿‘(𝐸 + 𝐺)) ∈ ran ((DIsoH‘𝐾)‘𝑊)) → (𝐿‘(𝐸 + 𝐺)) ⊆ 𝑉)
42	15, 40, 41	syl2anc 593	. . 3 ⊢ (𝜑 → (𝐿‘(𝐸 + 𝐺)) ⊆ 𝑉)
43	1, 37, 3, 4, 2, 15, 42	dochoccl 41954	. 2 ⊢ (𝜑 → ((𝐿‘(𝐸 + 𝐺)) ∈ ran ((DIsoH‘𝐾)‘𝑊) ↔ ( ⊥ ‘( ⊥ ‘(𝐿‘(𝐸 + 𝐺)))) = (𝐿‘(𝐸 + 𝐺))))
44	40, 43	mpbid 234	1 ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘(𝐸 + 𝐺)))) = (𝐿‘(𝐸 + 𝐺)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 399 ∨ wo 858 = wceq 1559 ∈ wcel 2141 ≠ wne 2956 ∖ cdif 3899 ∩ cin 3901 ⊆ wss 3902 {csn 4579 ran crn 5644 ‘cfv 6516 (class class class)co 7391 Basecbs 17236 +_gcplusg 17277 Scalarcsca 17280 0_gc0g 17459 LSSumclsm 19665 LSpanclspn 21026 LSAtomsclsa 39559 LSHypclsh 39560 LFnlclfn 39642 LKerclk 39670 LDualcld 39708 HLchlt 39935 LHypclh 40569 DVecHcdvh 41663 DIsoHcdih 41813 ocHcoch 41932

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-rep 5224 ax-sep 5243 ax-nul 5253 ax-pow 5319 ax-pr 5387 ax-un 7713 ax-cnex 11123 ax-resscn 11124 ax-1cn 11125 ax-icn 11126 ax-addcl 11127 ax-addrcl 11128 ax-mulcl 11129 ax-mulrcl 11130 ax-mulcom 11131 ax-addass 11132 ax-mulass 11133 ax-distr 11134 ax-i2m1 11135 ax-1ne0 11136 ax-1rid 11137 ax-rnegex 11138 ax-rrecex 11139 ax-cnre 11140 ax-pre-lttri 11141 ax-pre-lttrn 11142 ax-pre-ltadd 11143 ax-pre-mulgt0 11144 ax-riotaBAD 39538

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1098 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-nf 1803 df-sb 2090 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3061 df-ral 3076 df-rex 3086 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4284 df-if 4478 df-pw 4554 df-sn 4580 df-pr 4582 df-tp 4584 df-op 4586 df-uni 4863 df-int 4903 df-iun 4948 df-iin 4949 df-br 5098 df-opab 5160 df-mpt 5179 df-tr 5205 df-id 5538 df-eprel 5543 df-po 5551 df-so 5552 df-fr 5596 df-we 5598 df-xp 5649 df-rel 5650 df-cnv 5651 df-co 5652 df-dm 5653 df-rn 5654 df-res 5655 df-ima 5656 df-pred 6283 df-ord 6344 df-on 6345 df-lim 6346 df-suc 6347 df-iota 6472 df-fun 6518 df-fn 6519 df-f 6520 df-f1 6521 df-fo 6522 df-f1o 6523 df-fv 6524 df-riota 7348 df-ov 7394 df-oprab 7395 df-mpo 7396 df-of 7655 df-om 7842 df-1st 7965 df-2nd 7966 df-tpos 8200 df-undef 8247 df-frecs 8256 df-wrecs 8287 df-recs 8336 df-rdg 8375 df-1o 8431 df-2o 8432 df-er 8672 df-map 8804 df-en 8922 df-dom 8923 df-sdom 8924 df-fin 8925 df-pnf 11212 df-mnf 11213 df-xr 11214 df-ltxr 11215 df-le 11216 df-sub 11410 df-neg 11411 df-nn 12205 df-2 12274 df-3 12275 df-4 12276 df-5 12277 df-6 12278 df-n0 12476 df-z 12563 df-uz 12834 df-fz 13507 df-struct 17174 df-sets 17191 df-slot 17209 df-ndx 17221 df-base 17237 df-ress 17258 df-plusg 17290 df-mulr 17291 df-sca 17293 df-vsca 17294 df-0g 17461 df-mre 17605 df-mrc 17606 df-acs 17608 df-proset 18317 df-poset 18336 df-plt 18351 df-lub 18367 df-glb 18368 df-join 18369 df-meet 18370 df-p0 18446 df-p1 18447 df-lat 18455 df-clat 18522 df-mgm 18665 df-sgrp 18744 df-mnd 18760 df-submnd 18809 df-grp 18969 df-minusg 18970 df-sbg 18971 df-subg 19156 df-cntz 19348 df-oppg 19377 df-lsm 19667 df-cmn 19813 df-abl 19814 df-mgp 20178 df-rng 20190 df-ur 20219 df-ring 20272 df-oppr 20373 df-dvdsr 20393 df-unit 20394 df-invr 20424 df-dvr 20437 df-drng 20768 df-lmod 20917 df-lss 20987 df-lsp 21027 df-lvec 21158 df-lsatoms 39561 df-lshyp 39562 df-lcv 39604 df-lfl 39643 df-lkr 39671 df-ldual 39709 df-oposet 39761 df-ol 39763 df-oml 39764 df-covers 39851 df-ats 39852 df-atl 39883 df-cvlat 39907 df-hlat 39936 df-llines 40083 df-lplanes 40084 df-lvols 40085 df-lines 40086 df-psubsp 40088 df-pmap 40089 df-padd 40381 df-lhyp 40573 df-laut 40574 df-ldil 40689 df-ltrn 40690 df-trl 40744 df-tgrp 41328 df-tendo 41340 df-edring 41342 df-dveca 41588 df-disoa 41614 df-dvech 41664 df-dib 41724 df-dic 41758 df-dih 41814 df-doch 41933 df-djh 41980

This theorem is referenced by: lclkrlem2h 42099

W3C validator