lclkrlem2j - Mathbox for Norm Megill

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

Theorem lclkrlem2j 42008

Description: Lemma for lclkr 42025. Kernel closure when 𝑌 is zero. (Contributed by NM, 18-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	⊢ (𝜑 → (¬ 𝑋 ∈ ( ⊥ ‘{𝐵}) ∨ ¬ 𝑌 ∈ ( ⊥ ‘{𝐵})))
lclkrlem2j.x	⊢ (𝜑 → 𝑋 ∈ 𝑉)
lclkrlem2j.y	⊢ (𝜑 → 𝑌 = 0 )

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

**Proof of Theorem lclkrlem2j**
Step	Hyp	Ref	Expression
1		lclkrlem2f.k	. . 3 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
2		lclkrlem2j.x	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
3	2	snssd 4718	. . . 4 ⊢ (𝜑 → {𝑋} ⊆ 𝑉)
4		lclkrlem2f.h	. . . . 5 ⊢ 𝐻 = (LHyp‘𝐾)
5		eqid 2739	. . . . 5 ⊢ ((DIsoH‘𝐾)‘𝑊) = ((DIsoH‘𝐾)‘𝑊)
6		lclkrlem2f.u	. . . . 5 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
7		lclkrlem2f.v	. . . . 5 ⊢ 𝑉 = (Base‘𝑈)
8		lclkrlem2f.o	. . . . 5 ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)
9	4, 5, 6, 7, 8	dochcl 41845	. . . 4 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ {𝑋} ⊆ 𝑉) → ( ⊥ ‘{𝑋}) ∈ ran ((DIsoH‘𝐾)‘𝑊))
10	1, 3, 9	syl2anc 590	. . 3 ⊢ (𝜑 → ( ⊥ ‘{𝑋}) ∈ ran ((DIsoH‘𝐾)‘𝑊))
11	4, 5, 8	dochoc 41859	. . 3 ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ( ⊥ ‘{𝑋}) ∈ ran ((DIsoH‘𝐾)‘𝑊)) → ( ⊥ ‘( ⊥ ‘( ⊥ ‘{𝑋}))) = ( ⊥ ‘{𝑋}))
12	1, 10, 11	syl2anc 590	. 2 ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘( ⊥ ‘{𝑋}))) = ( ⊥ ‘{𝑋}))
13		lclkrlem2f.lg	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐿‘𝐺) = ( ⊥ ‘{𝑌}))
14		lclkrlem2j.y	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑌 = 0 )
15	14	sneqd 4567	. . . . . . . . . . . 12 ⊢ (𝜑 → {𝑌} = { 0 })
16	15	fveq2d 6831	. . . . . . . . . . 11 ⊢ (𝜑 → ( ⊥ ‘{𝑌}) = ( ⊥ ‘{ 0 }))
17		eqid 2739	. . . . . . . . . . . . 13 ⊢ (Base‘𝑈) = (Base‘𝑈)
18		lclkrlem2f.z	. . . . . . . . . . . . 13 ⊢ 0 = (0_g‘𝑈)
19	4, 6, 8, 17, 18	doch0 41850	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ( ⊥ ‘{ 0 }) = (Base‘𝑈))
20	1, 19	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → ( ⊥ ‘{ 0 }) = (Base‘𝑈))
21	13, 16, 20	3eqtrd 2778	. . . . . . . . . 10 ⊢ (𝜑 → (𝐿‘𝐺) = (Base‘𝑈))
22	4, 6, 1	dvhlmod 41602	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑈 ∈ LMod)
23		lclkrlem2f.g	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐺 ∈ 𝐹)
24		lclkrlem2f.s	. . . . . . . . . . . 12 ⊢ 𝑆 = (Scalar‘𝑈)
25		lclkrlem2f.q	. . . . . . . . . . . 12 ⊢ 𝑄 = (0_g‘𝑆)
26		lclkrlem2f.f	. . . . . . . . . . . 12 ⊢ 𝐹 = (LFnl‘𝑈)
27		lclkrlem2f.l	. . . . . . . . . . . 12 ⊢ 𝐿 = (LKer‘𝑈)
28	24, 25, 17, 26, 27	lkr0f 39586	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ LMod ∧ 𝐺 ∈ 𝐹) → ((𝐿‘𝐺) = (Base‘𝑈) ↔ 𝐺 = ((Base‘𝑈) × {𝑄})))
29	22, 23, 28	syl2anc 590	. . . . . . . . . 10 ⊢ (𝜑 → ((𝐿‘𝐺) = (Base‘𝑈) ↔ 𝐺 = ((Base‘𝑈) × {𝑄})))
30	21, 29	mpbid 233	. . . . . . . . 9 ⊢ (𝜑 → 𝐺 = ((Base‘𝑈) × {𝑄}))
31		lclkrlem2f.d	. . . . . . . . . 10 ⊢ 𝐷 = (LDual‘𝑈)
32		eqid 2739	. . . . . . . . . 10 ⊢ (0_g‘𝐷) = (0_g‘𝐷)
33	17, 24, 25, 31, 32, 22	ldual0v 39642	. . . . . . . . 9 ⊢ (𝜑 → (0_g‘𝐷) = ((Base‘𝑈) × {𝑄}))
34	30, 33	eqtr4d 2777	. . . . . . . 8 ⊢ (𝜑 → 𝐺 = (0_g‘𝐷))
35	34	oveq2d 7372	. . . . . . 7 ⊢ (𝜑 → (𝐸 + 𝐺) = (𝐸 + (0_g‘𝐷)))
36	31, 22	lduallmod 39645	. . . . . . . 8 ⊢ (𝜑 → 𝐷 ∈ LMod)
37		eqid 2739	. . . . . . . . 9 ⊢ (Base‘𝐷) = (Base‘𝐷)
38		lclkrlem2f.e	. . . . . . . . 9 ⊢ (𝜑 → 𝐸 ∈ 𝐹)
39	26, 31, 37, 22, 38	ldualelvbase 39619	. . . . . . . 8 ⊢ (𝜑 → 𝐸 ∈ (Base‘𝐷))
40		lclkrlem2f.p	. . . . . . . . 9 ⊢ + = (+_g‘𝐷)
41	37, 40, 32	lmod0vrid 20883	. . . . . . . 8 ⊢ ((𝐷 ∈ LMod ∧ 𝐸 ∈ (Base‘𝐷)) → (𝐸 + (0_g‘𝐷)) = 𝐸)
42	36, 39, 41	syl2anc 590	. . . . . . 7 ⊢ (𝜑 → (𝐸 + (0_g‘𝐷)) = 𝐸)
43	35, 42	eqtrd 2774	. . . . . 6 ⊢ (𝜑 → (𝐸 + 𝐺) = 𝐸)
44	43	fveq2d 6831	. . . . 5 ⊢ (𝜑 → (𝐿‘(𝐸 + 𝐺)) = (𝐿‘𝐸))
45		lclkrlem2f.le	. . . . 5 ⊢ (𝜑 → (𝐿‘𝐸) = ( ⊥ ‘{𝑋}))
46	44, 45	eqtr2d 2775	. . . 4 ⊢ (𝜑 → ( ⊥ ‘{𝑋}) = (𝐿‘(𝐸 + 𝐺)))
47	46	fveq2d 6831	. . 3 ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘{𝑋})) = ( ⊥ ‘(𝐿‘(𝐸 + 𝐺))))
48	47	fveq2d 6831	. 2 ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘( ⊥ ‘{𝑋}))) = ( ⊥ ‘( ⊥ ‘(𝐿‘(𝐸 + 𝐺)))))
49	12, 48, 46	3eqtr3d 2782	1 ⊢ (𝜑 → ( ⊥ ‘( ⊥ ‘(𝐿‘(𝐸 + 𝐺)))) = (𝐿‘(𝐸 + 𝐺)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 ∧ wa 396 ∨ wo 853 = wceq 1547 ∈ wcel 2119 ∖ cdif 3880 ⊆ wss 3883 {csn 4555 × cxp 5616 ran crn 5619 ‘cfv 6485 (class class class)co 7356 Basecbs 17170 +_gcplusg 17211 Scalarcsca 17214 0_gc0g 17393 LSSumclsm 19600 LModclmod 20850 LSpanclspn 20961 LSHypclsh 39467 LFnlclfn 39549 LKerclk 39577 LDualcld 39615 HLchlt 39842 LHypclh 40476 DVecHcdvh 41570 DIsoHcdih 41720 ocHcoch 41839

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2711 ax-rep 5199 ax-sep 5218 ax-nul 5228 ax-pow 5294 ax-pr 5362 ax-un 7678 ax-cnex 11085 ax-resscn 11086 ax-1cn 11087 ax-icn 11088 ax-addcl 11089 ax-addrcl 11090 ax-mulcl 11091 ax-mulrcl 11092 ax-mulcom 11093 ax-addass 11094 ax-mulass 11095 ax-distr 11096 ax-i2m1 11097 ax-1ne0 11098 ax-1rid 11099 ax-rnegex 11100 ax-rrecex 11101 ax-cnre 11102 ax-pre-lttri 11103 ax-pre-lttrn 11104 ax-pre-ltadd 11105 ax-pre-mulgt0 11106 ax-riotaBAD 39445

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3or 1093 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2718 df-cleq 2731 df-clel 2814 df-nfc 2888 df-ne 2935 df-nel 3039 df-ral 3054 df-rex 3064 df-rmo 3344 df-reu 3345 df-rab 3392 df-v 3433 df-sbc 3724 df-csb 3832 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3903 df-nul 4262 df-if 4455 df-pw 4531 df-sn 4556 df-pr 4558 df-tp 4560 df-op 4562 df-uni 4839 df-int 4878 df-iun 4923 df-iin 4924 df-br 5073 df-opab 5135 df-mpt 5154 df-tr 5180 df-id 5513 df-eprel 5518 df-po 5526 df-so 5527 df-fr 5571 df-we 5573 df-xp 5624 df-rel 5625 df-cnv 5626 df-co 5627 df-dm 5628 df-rn 5629 df-res 5630 df-ima 5631 df-pred 6252 df-ord 6313 df-on 6314 df-lim 6315 df-suc 6316 df-iota 6441 df-fun 6487 df-fn 6488 df-f 6489 df-f1 6490 df-fo 6491 df-f1o 6492 df-fv 6493 df-riota 7313 df-ov 7359 df-oprab 7360 df-mpo 7361 df-of 7620 df-om 7807 df-1st 7931 df-2nd 7932 df-tpos 8166 df-undef 8213 df-frecs 8221 df-wrecs 8252 df-recs 8301 df-rdg 8339 df-1o 8395 df-er 8633 df-map 8765 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-pnf 11172 df-mnf 11173 df-xr 11174 df-ltxr 11175 df-le 11176 df-sub 11370 df-neg 11371 df-nn 12166 df-2 12235 df-3 12236 df-4 12237 df-5 12238 df-6 12239 df-n0 12429 df-z 12516 df-uz 12780 df-fz 13453 df-struct 17108 df-sets 17125 df-slot 17143 df-ndx 17155 df-base 17171 df-ress 17192 df-plusg 17224 df-mulr 17225 df-sca 17227 df-vsca 17228 df-0g 17395 df-proset 18251 df-poset 18270 df-plt 18285 df-lub 18301 df-glb 18302 df-join 18303 df-meet 18304 df-p0 18380 df-p1 18381 df-lat 18389 df-clat 18456 df-mgm 18599 df-sgrp 18678 df-mnd 18694 df-submnd 18743 df-grp 18903 df-minusg 18904 df-sbg 18905 df-subg 19090 df-cntz 19283 df-lsm 19602 df-cmn 19748 df-abl 19749 df-mgp 20113 df-rng 20125 df-ur 20154 df-ring 20207 df-oppr 20308 df-dvdsr 20328 df-unit 20329 df-invr 20359 df-dvr 20372 df-drng 20703 df-lmod 20852 df-lss 20922 df-lsp 20962 df-lvec 21093 df-lfl 39550 df-lkr 39578 df-ldual 39616 df-oposet 39668 df-ol 39670 df-oml 39671 df-covers 39758 df-ats 39759 df-atl 39790 df-cvlat 39814 df-hlat 39843 df-llines 39990 df-lplanes 39991 df-lvols 39992 df-lines 39993 df-psubsp 39995 df-pmap 39996 df-padd 40288 df-lhyp 40480 df-laut 40481 df-ldil 40596 df-ltrn 40597 df-trl 40651 df-tendo 41247 df-edring 41249 df-disoa 41521 df-dvech 41571 df-dib 41631 df-dic 41665 df-dih 41721 df-doch 41840

This theorem is referenced by: lclkrlem2k 42009 lclkrlem2l 42010

W3C validator