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 37526

Description: Lemma for lclkr 37546. 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 37525	. . . 4 ⊢ (𝜑 → (((𝐿‘𝐸) ∩ (𝐿‘𝐺)) ⊕ (𝑁‘{𝐵})) ⊆ (𝐿‘(𝐸 + 𝐺)))
28	1, 3, 15	dvhlvec 37122	. . . . 5 ⊢ (𝜑 → 𝑈 ∈ LVec)
29	19, 20	ineq12d 4011	. . . . . . 7 ⊢ (𝜑 → ((𝐿‘𝐸) ∩ (𝐿‘𝐺)) = (( ⊥ ‘{𝑋}) ∩ ( ⊥ ‘{𝑌})))
30	29	oveq1d 6891	. . . . . 6 ⊢ (𝜑 → (((𝐿‘𝐸) ∩ (𝐿‘𝐺)) ⊕ (𝑁‘{𝐵})) = ((( ⊥ ‘{𝑋}) ∩ ( ⊥ ‘{𝑌})) ⊕ (𝑁‘{𝐵})))
31		eqid 2797	. . . . . . 7 ⊢ (LSAtoms‘𝑈) = (LSAtoms‘𝑈)
32	25, 19, 20	3netr3d 3045	. . . . . . 7 ⊢ (𝜑 → ( ⊥ ‘{𝑋}) ≠ ( ⊥ ‘{𝑌}))
33	1, 2, 3, 4, 7, 8, 9, 31, 15, 16, 23, 24, 32, 22, 11	lclkrlem2c 37522	. . . . . 6 ⊢ (𝜑 → ((( ⊥ ‘{𝑋}) ∩ ( ⊥ ‘{𝑌})) ⊕ (𝑁‘{𝐵})) ∈ 𝐽)
34	30, 33	eqeltrd 2876	. . . . 5 ⊢ (𝜑 → (((𝐿‘𝐸) ∩ (𝐿‘𝐺)) ⊕ (𝑁‘{𝐵})) ∈ 𝐽)
35	11, 28, 34, 26	lshpcmp 35001	. . . 4 ⊢ (𝜑 → ((((𝐿‘𝐸) ∩ (𝐿‘𝐺)) ⊕ (𝑁‘{𝐵})) ⊆ (𝐿‘(𝐸 + 𝐺)) ↔ (((𝐿‘𝐸) ∩ (𝐿‘𝐺)) ⊕ (𝑁‘{𝐵})) = (𝐿‘(𝐸 + 𝐺))))
36	27, 35	mpbid 224	. . 3 ⊢ (𝜑 → (((𝐿‘𝐸) ∩ (𝐿‘𝐺)) ⊕ (𝑁‘{𝐵})) = (𝐿‘(𝐸 + 𝐺)))
37		eqid 2797	. . . . 5 ⊢ ((DIsoH‘𝐾)‘𝑊) = ((DIsoH‘𝐾)‘𝑊)
38	1, 2, 3, 4, 7, 8, 9, 31, 15, 16, 23, 24, 32, 22, 37	lclkrlem2d 37523	. . . 4 ⊢ (𝜑 → ((( ⊥ ‘{𝑋}) ∩ ( ⊥ ‘{𝑌})) ⊕ (𝑁‘{𝐵})) ∈ ran ((DIsoH‘𝐾)‘𝑊))
39	30, 38	eqeltrd 2876	. . 3 ⊢ (𝜑 → (((𝐿‘𝐸) ∩ (𝐿‘𝐺)) ⊕ (𝑁‘{𝐵})) ∈ ran ((DIsoH‘𝐾)‘𝑊))
40	36, 39	eqeltrrd 2877	. 2 ⊢ (𝜑 → (𝐿‘(𝐸 + 𝐺)) ∈ ran ((DIsoH‘𝐾)‘𝑊))
41	1, 3, 37, 4	dihrnss 37291	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐿‘(𝐸 + 𝐺)) ∈ ran ((DIsoH‘𝐾)‘𝑊)) → (𝐿‘(𝐸 + 𝐺)) ⊆ 𝑉)
42	15, 40, 41	syl2anc 580	. . 3 ⊢ (𝜑 → (𝐿‘(𝐸 + 𝐺)) ⊆ 𝑉)
43	1, 37, 3, 4, 2, 15, 42	dochoccl 37382	. 2 ⊢ (𝜑 → ((𝐿‘(𝐸 + 𝐺)) ∈ ran ((DIsoH‘𝐾)‘𝑊) ↔ ( ⊥ ‘( ⊥ ‘(𝐿‘(𝐸 + 𝐺)))) = (𝐿‘(𝐸 + 𝐺))))
44	40, 43	mpbid 224	1 ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘(𝐸 + 𝐺)))) = (𝐿‘(𝐸 + 𝐺)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 385 ∨ wo 874 = wceq 1653 ∈ wcel 2157 ≠ wne 2969 ∖ cdif 3764 ∩ cin 3766 ⊆ wss 3767 {csn 4366 ran crn 5311 ‘cfv 6099 (class class class)co 6876 Basecbs 16181 +_gcplusg 16264 Scalarcsca 16267 0_gc0g 16412 LSSumclsm 18359 LSpanclspn 19289 LSAtomsclsa 34987 LSHypclsh 34988 LFnlclfn 35070 LKerclk 35098 LDualcld 35136 HLchlt 35363 LHypclh 35997 DVecHcdvh 37091 DIsoHcdih 37241 ocHcoch 37360

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1891 ax-4 1905 ax-5 2006 ax-6 2072 ax-7 2107 ax-8 2159 ax-9 2166 ax-10 2185 ax-11 2200 ax-12 2213 ax-13 2354 ax-ext 2775 ax-rep 4962 ax-sep 4973 ax-nul 4981 ax-pow 5033 ax-pr 5095 ax-un 7181 ax-cnex 10278 ax-resscn 10279 ax-1cn 10280 ax-icn 10281 ax-addcl 10282 ax-addrcl 10283 ax-mulcl 10284 ax-mulrcl 10285 ax-mulcom 10286 ax-addass 10287 ax-mulass 10288 ax-distr 10289 ax-i2m1 10290 ax-1ne0 10291 ax-1rid 10292 ax-rnegex 10293 ax-rrecex 10294 ax-cnre 10295 ax-pre-lttri 10296 ax-pre-lttrn 10297 ax-pre-ltadd 10298 ax-pre-mulgt0 10299 ax-riotaBAD 34966

This theorem depends on definitions: df-bi 199 df-an 386 df-or 875 df-3or 1109 df-3an 1110 df-tru 1657 df-fal 1667 df-ex 1876 df-nf 1880 df-sb 2065 df-mo 2590 df-eu 2607 df-clab 2784 df-cleq 2790 df-clel 2793 df-nfc 2928 df-ne 2970 df-nel 3073 df-ral 3092 df-rex 3093 df-reu 3094 df-rmo 3095 df-rab 3096 df-v 3385 df-sbc 3632 df-csb 3727 df-dif 3770 df-un 3772 df-in 3774 df-ss 3781 df-pss 3783 df-nul 4114 df-if 4276 df-pw 4349 df-sn 4367 df-pr 4369 df-tp 4371 df-op 4373 df-uni 4627 df-int 4666 df-iun 4710 df-iin 4711 df-br 4842 df-opab 4904 df-mpt 4921 df-tr 4944 df-id 5218 df-eprel 5223 df-po 5231 df-so 5232 df-fr 5269 df-we 5271 df-xp 5316 df-rel 5317 df-cnv 5318 df-co 5319 df-dm 5320 df-rn 5321 df-res 5322 df-ima 5323 df-pred 5896 df-ord 5942 df-on 5943 df-lim 5944 df-suc 5945 df-iota 6062 df-fun 6101 df-fn 6102 df-f 6103 df-f1 6104 df-fo 6105 df-f1o 6106 df-fv 6107 df-riota 6837 df-ov 6879 df-oprab 6880 df-mpt2 6881 df-of 7129 df-om 7298 df-1st 7399 df-2nd 7400 df-tpos 7588 df-undef 7635 df-wrecs 7643 df-recs 7705 df-rdg 7743 df-1o 7797 df-oadd 7801 df-er 7980 df-map 8095 df-en 8194 df-dom 8195 df-sdom 8196 df-fin 8197 df-pnf 10363 df-mnf 10364 df-xr 10365 df-ltxr 10366 df-le 10367 df-sub 10556 df-neg 10557 df-nn 11311 df-2 11372 df-3 11373 df-4 11374 df-5 11375 df-6 11376 df-n0 11577 df-z 11663 df-uz 11927 df-fz 12577 df-struct 16183 df-ndx 16184 df-slot 16185 df-base 16187 df-sets 16188 df-ress 16189 df-plusg 16277 df-mulr 16278 df-sca 16280 df-vsca 16281 df-0g 16414 df-mre 16558 df-mrc 16559 df-acs 16561 df-proset 17240 df-poset 17258 df-plt 17270 df-lub 17286 df-glb 17287 df-join 17288 df-meet 17289 df-p0 17351 df-p1 17352 df-lat 17358 df-clat 17420 df-mgm 17554 df-sgrp 17596 df-mnd 17607 df-submnd 17648 df-grp 17738 df-minusg 17739 df-sbg 17740 df-subg 17901 df-cntz 18059 df-oppg 18085 df-lsm 18361 df-cmn 18507 df-abl 18508 df-mgp 18803 df-ur 18815 df-ring 18862 df-oppr 18936 df-dvdsr 18954 df-unit 18955 df-invr 18985 df-dvr 18996 df-drng 19064 df-lmod 19180 df-lss 19248 df-lsp 19290 df-lvec 19421 df-lsatoms 34989 df-lshyp 34990 df-lcv 35032 df-lfl 35071 df-lkr 35099 df-ldual 35137 df-oposet 35189 df-ol 35191 df-oml 35192 df-covers 35279 df-ats 35280 df-atl 35311 df-cvlat 35335 df-hlat 35364 df-llines 35511 df-lplanes 35512 df-lvols 35513 df-lines 35514 df-psubsp 35516 df-pmap 35517 df-padd 35809 df-lhyp 36001 df-laut 36002 df-ldil 36117 df-ltrn 36118 df-trl 36172 df-tgrp 36756 df-tendo 36768 df-edring 36770 df-dveca 37016 df-disoa 37042 df-dvech 37092 df-dib 37152 df-dic 37186 df-dih 37242 df-doch 37361 df-djh 37408

This theorem is referenced by: lclkrlem2h 37527

W3C validator