lclkrlem2i - Mathbox for Norm Megill

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

Theorem lclkrlem2i 42213

Description: Lemma for lclkr 42231. Eliminate the (𝐿‘𝐸) ≠ (𝐿‘𝐺) hypothesis. (Contributed by NM, 17-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	⊢ (𝜑 → (¬ 𝑋 ∈ ( ⊥ ‘{𝐵}) ∨ ¬ 𝑌 ∈ ( ⊥ ‘{𝐵})))
lclkrlem2i.x	⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))
lclkrlem2i.y	⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))

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

**Proof of Theorem lclkrlem2i**
Step	Hyp	Ref	Expression
1		lclkrlem2f.h	. . 3 ⊢ 𝐻 = (LHyp‘𝐾)
2		lclkrlem2f.o	. . 3 ⊢ ⊥ = ((ocH‘𝐾)‘𝑊)
3		lclkrlem2f.u	. . 3 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
4		lclkrlem2f.v	. . 3 ⊢ 𝑉 = (Base‘𝑈)
5		lclkrlem2f.z	. . 3 ⊢ 0 = (0_g‘𝑈)
6		lclkrlem2f.f	. . 3 ⊢ 𝐹 = (LFnl‘𝑈)
7		lclkrlem2f.l	. . 3 ⊢ 𝐿 = (LKer‘𝑈)
8		lclkrlem2f.d	. . 3 ⊢ 𝐷 = (LDual‘𝑈)
9		lclkrlem2f.p	. . 3 ⊢ + = (+_g‘𝐷)
10		lclkrlem2f.k	. . . 4 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
11	10	adantr 485	. . 3 ⊢ ((𝜑 ∧ (𝐿‘𝐸) = (𝐿‘𝐺)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
12		lclkrlem2i.x	. . . 4 ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))
13	12	adantr 485	. . 3 ⊢ ((𝜑 ∧ (𝐿‘𝐸) = (𝐿‘𝐺)) → 𝑋 ∈ (𝑉 ∖ { 0 }))
14		lclkrlem2f.e	. . . 4 ⊢ (𝜑 → 𝐸 ∈ 𝐹)
15	14	adantr 485	. . 3 ⊢ ((𝜑 ∧ (𝐿‘𝐸) = (𝐿‘𝐺)) → 𝐸 ∈ 𝐹)
16		lclkrlem2f.g	. . . 4 ⊢ (𝜑 → 𝐺 ∈ 𝐹)
17	16	adantr 485	. . 3 ⊢ ((𝜑 ∧ (𝐿‘𝐸) = (𝐿‘𝐺)) → 𝐺 ∈ 𝐹)
18		lclkrlem2f.le	. . . 4 ⊢ (𝜑 → (𝐿‘𝐸) = ( ⊥ ‘{𝑋}))
19	18	adantr 485	. . 3 ⊢ ((𝜑 ∧ (𝐿‘𝐸) = (𝐿‘𝐺)) → (𝐿‘𝐸) = ( ⊥ ‘{𝑋}))
20		simpr 489	. . 3 ⊢ ((𝜑 ∧ (𝐿‘𝐸) = (𝐿‘𝐺)) → (𝐿‘𝐸) = (𝐿‘𝐺))
21	1, 2, 3, 4, 5, 6, 7, 8, 9, 11, 13, 15, 17, 19, 20	lclkrlem2e 42209	. 2 ⊢ ((𝜑 ∧ (𝐿‘𝐸) = (𝐿‘𝐺)) → ( ⊥ ‘( ⊥ ‘(𝐿‘(𝐸 + 𝐺)))) = (𝐿‘(𝐸 + 𝐺)))
22		lclkrlem2f.s	. . 3 ⊢ 𝑆 = (Scalar‘𝑈)
23		lclkrlem2f.q	. . 3 ⊢ 𝑄 = (0_g‘𝑆)
24		lclkrlem2f.a	. . 3 ⊢ ⊕ = (LSSum‘𝑈)
25		lclkrlem2f.n	. . 3 ⊢ 𝑁 = (LSpan‘𝑈)
26		lclkrlem2f.j	. . 3 ⊢ 𝐽 = (LSHyp‘𝑈)
27	10	adantr 485	. . 3 ⊢ ((𝜑 ∧ (𝐿‘𝐸) ≠ (𝐿‘𝐺)) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
28		lclkrlem2f.b	. . . 4 ⊢ (𝜑 → 𝐵 ∈ (𝑉 ∖ { 0 }))
29	28	adantr 485	. . 3 ⊢ ((𝜑 ∧ (𝐿‘𝐸) ≠ (𝐿‘𝐺)) → 𝐵 ∈ (𝑉 ∖ { 0 }))
30	14	adantr 485	. . 3 ⊢ ((𝜑 ∧ (𝐿‘𝐸) ≠ (𝐿‘𝐺)) → 𝐸 ∈ 𝐹)
31	16	adantr 485	. . 3 ⊢ ((𝜑 ∧ (𝐿‘𝐸) ≠ (𝐿‘𝐺)) → 𝐺 ∈ 𝐹)
32	18	adantr 485	. . 3 ⊢ ((𝜑 ∧ (𝐿‘𝐸) ≠ (𝐿‘𝐺)) → (𝐿‘𝐸) = ( ⊥ ‘{𝑋}))
33		lclkrlem2f.lg	. . . 4 ⊢ (𝜑 → (𝐿‘𝐺) = ( ⊥ ‘{𝑌}))
34	33	adantr 485	. . 3 ⊢ ((𝜑 ∧ (𝐿‘𝐸) ≠ (𝐿‘𝐺)) → (𝐿‘𝐺) = ( ⊥ ‘{𝑌}))
35		lclkrlem2f.kb	. . . 4 ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝐵) = 𝑄)
36	35	adantr 485	. . 3 ⊢ ((𝜑 ∧ (𝐿‘𝐸) ≠ (𝐿‘𝐺)) → ((𝐸 + 𝐺)‘𝐵) = 𝑄)
37		lclkrlem2f.nx	. . . 4 ⊢ (𝜑 → (¬ 𝑋 ∈ ( ⊥ ‘{𝐵}) ∨ ¬ 𝑌 ∈ ( ⊥ ‘{𝐵})))
38	37	adantr 485	. . 3 ⊢ ((𝜑 ∧ (𝐿‘𝐸) ≠ (𝐿‘𝐺)) → (¬ 𝑋 ∈ ( ⊥ ‘{𝐵}) ∨ ¬ 𝑌 ∈ ( ⊥ ‘{𝐵})))
39	12	adantr 485	. . 3 ⊢ ((𝜑 ∧ (𝐿‘𝐸) ≠ (𝐿‘𝐺)) → 𝑋 ∈ (𝑉 ∖ { 0 }))
40		lclkrlem2i.y	. . . 4 ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))
41	40	adantr 485	. . 3 ⊢ ((𝜑 ∧ (𝐿‘𝐸) ≠ (𝐿‘𝐺)) → 𝑌 ∈ (𝑉 ∖ { 0 }))
42		simpr 489	. . 3 ⊢ ((𝜑 ∧ (𝐿‘𝐸) ≠ (𝐿‘𝐺)) → (𝐿‘𝐸) ≠ (𝐿‘𝐺))
43	1, 2, 3, 4, 22, 23, 5, 24, 25, 6, 26, 7, 8, 9, 27, 29, 30, 31, 32, 34, 36, 38, 39, 41, 42	lclkrlem2h 42212	. 2 ⊢ ((𝜑 ∧ (𝐿‘𝐸) ≠ (𝐿‘𝐺)) → ( ⊥ ‘( ⊥ ‘(𝐿‘(𝐸 + 𝐺)))) = (𝐿‘(𝐸 + 𝐺)))
44	21, 43	pm2.61dane 3051	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 {csn 4594 ‘cfv 6537 (class class class)co 7411 Basecbs 17269 +_gcplusg 17310 Scalarcsca 17313 0_gc0g 17492 LSSumclsm 19704 LSpanclspn 21070 LSHypclsh 39673 LFnlclfn 39755 LKerclk 39783 LDualcld 39821 HLchlt 40048 LHypclh 40682 DVecHcdvh 41776 ocHcoch 42045

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 5242 ax-sep 5261 ax-nul 5271 ax-pow 5337 ax-pr 5405 ax-un 7733 ax-cnex 11156 ax-resscn 11157 ax-1cn 11158 ax-icn 11159 ax-addcl 11160 ax-addrcl 11161 ax-mulcl 11162 ax-mulrcl 11163 ax-mulcom 11164 ax-addass 11165 ax-mulass 11166 ax-distr 11167 ax-i2m1 11168 ax-1ne0 11169 ax-1rid 11170 ax-rnegex 11171 ax-rrecex 11172 ax-cnre 11173 ax-pre-lttri 11174 ax-pre-lttrn 11175 ax-pre-ltadd 11176 ax-pre-mulgt0 11177 ax-riotaBAD 39651

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 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-tp 4599 df-op 4601 df-uni 4877 df-int 4917 df-iun 4962 df-iin 4963 df-br 5114 df-opab 5178 df-mpt 5197 df-tr 5223 df-id 5557 df-eprel 5562 df-po 5570 df-so 5571 df-fr 5615 df-we 5617 df-xp 5668 df-rel 5669 df-cnv 5670 df-co 5671 df-dm 5672 df-rn 5673 df-res 5674 df-ima 5675 df-pred 6303 df-ord 6364 df-on 6365 df-lim 6366 df-suc 6367 df-iota 6493 df-fun 6539 df-fn 6540 df-f 6541 df-f1 6542 df-fo 6543 df-f1o 6544 df-fv 6545 df-riota 7368 df-ov 7414 df-oprab 7415 df-mpo 7416 df-of 7675 df-om 7863 df-1st 7986 df-2nd 7987 df-tpos 8222 df-undef 8269 df-frecs 8278 df-wrecs 8309 df-recs 8358 df-rdg 8397 df-1o 8453 df-2o 8454 df-er 8694 df-map 8826 df-en 8944 df-dom 8945 df-sdom 8946 df-fin 8947 df-pnf 11245 df-mnf 11246 df-xr 11247 df-ltxr 11248 df-le 11249 df-sub 11443 df-neg 11444 df-nn 12234 df-2 12303 df-3 12304 df-4 12305 df-5 12306 df-6 12307 df-n0 12505 df-z 12592 df-uz 12863 df-fz 13536 df-struct 17207 df-sets 17224 df-slot 17242 df-ndx 17254 df-base 17270 df-ress 17291 df-plusg 17323 df-mulr 17324 df-sca 17326 df-vsca 17327 df-0g 17494 df-mre 17638 df-mrc 17639 df-acs 17641 df-proset 18350 df-poset 18369 df-plt 18384 df-lub 18400 df-glb 18401 df-join 18402 df-meet 18403 df-p0 18479 df-p1 18480 df-lat 18488 df-clat 18555 df-mgm 18698 df-sgrp 18777 df-mnd 18793 df-submnd 18842 df-grp 19003 df-minusg 19004 df-sbg 19005 df-subg 19189 df-cntz 19387 df-oppg 19416 df-lsm 19706 df-cmn 19852 df-abl 19853 df-mgp 20217 df-rng 20231 df-ur 20264 df-ring 20317 df-oppr 20419 df-dvdsr 20439 df-unit 20440 df-invr 20470 df-dvr 20483 df-drng 20815 df-lmod 20961 df-lss 21031 df-lsp 21071 df-lvec 21202 df-lsatoms 39674 df-lshyp 39675 df-lcv 39717 df-lfl 39756 df-lkr 39784 df-ldual 39822 df-oposet 39874 df-ol 39876 df-oml 39877 df-covers 39964 df-ats 39965 df-atl 39996 df-cvlat 40020 df-hlat 40049 df-llines 40196 df-lplanes 40197 df-lvols 40198 df-lines 40199 df-psubsp 40201 df-pmap 40202 df-padd 40494 df-lhyp 40686 df-laut 40687 df-ldil 40802 df-ltrn 40803 df-trl 40857 df-tgrp 41441 df-tendo 41453 df-edring 41455 df-dveca 41701 df-disoa 41727 df-dvech 41777 df-dib 41837 df-dic 41871 df-dih 41927 df-doch 42046 df-djh 42093

This theorem is referenced by: lclkrlem2l 42216

W3C validator