lclkrlem2l - Mathbox for Norm Megill

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

Theorem lclkrlem2l 42177

Description: Lemma for lclkr 42192. Eliminate the 𝑋 ≠ 0, 𝑌 ≠ 0 hypotheses. (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	⊢ (𝜑 → (¬ 𝑋 ∈ ( ⊥ ‘{𝐵}) ∨ ¬ 𝑌 ∈ ( ⊥ ‘{𝐵})))
lclkrlem2l.x	⊢ (𝜑 → 𝑋 ∈ 𝑉)
lclkrlem2l.y	⊢ (𝜑 → 𝑌 ∈ 𝑉)

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

**Proof of Theorem lclkrlem2l**
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.s	. . 3 ⊢ 𝑆 = (Scalar‘𝑈)
6		lclkrlem2f.q	. . 3 ⊢ 𝑄 = (0_g‘𝑆)
7		lclkrlem2f.z	. . 3 ⊢ 0 = (0_g‘𝑈)
8		lclkrlem2f.a	. . 3 ⊢ ⊕ = (LSSum‘𝑈)
9		lclkrlem2f.n	. . 3 ⊢ 𝑁 = (LSpan‘𝑈)
10		lclkrlem2f.f	. . 3 ⊢ 𝐹 = (LFnl‘𝑈)
11		lclkrlem2f.j	. . 3 ⊢ 𝐽 = (LSHyp‘𝑈)
12		lclkrlem2f.l	. . 3 ⊢ 𝐿 = (LKer‘𝑈)
13		lclkrlem2f.d	. . 3 ⊢ 𝐷 = (LDual‘𝑈)
14		lclkrlem2f.p	. . 3 ⊢ + = (+_g‘𝐷)
15		lclkrlem2f.k	. . . 4 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
16	15	adantr 485	. . 3 ⊢ ((𝜑 ∧ 𝑋 = 0 ) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
17		lclkrlem2f.b	. . . 4 ⊢ (𝜑 → 𝐵 ∈ (𝑉 ∖ { 0 }))
18	17	adantr 485	. . 3 ⊢ ((𝜑 ∧ 𝑋 = 0 ) → 𝐵 ∈ (𝑉 ∖ { 0 }))
19		lclkrlem2f.e	. . . 4 ⊢ (𝜑 → 𝐸 ∈ 𝐹)
20	19	adantr 485	. . 3 ⊢ ((𝜑 ∧ 𝑋 = 0 ) → 𝐸 ∈ 𝐹)
21		lclkrlem2f.g	. . . 4 ⊢ (𝜑 → 𝐺 ∈ 𝐹)
22	21	adantr 485	. . 3 ⊢ ((𝜑 ∧ 𝑋 = 0 ) → 𝐺 ∈ 𝐹)
23		lclkrlem2f.le	. . . 4 ⊢ (𝜑 → (𝐿‘𝐸) = ( ⊥ ‘{𝑋}))
24	23	adantr 485	. . 3 ⊢ ((𝜑 ∧ 𝑋 = 0 ) → (𝐿‘𝐸) = ( ⊥ ‘{𝑋}))
25		lclkrlem2f.lg	. . . 4 ⊢ (𝜑 → (𝐿‘𝐺) = ( ⊥ ‘{𝑌}))
26	25	adantr 485	. . 3 ⊢ ((𝜑 ∧ 𝑋 = 0 ) → (𝐿‘𝐺) = ( ⊥ ‘{𝑌}))
27		lclkrlem2f.kb	. . . 4 ⊢ (𝜑 → ((𝐸 + 𝐺)‘𝐵) = 𝑄)
28	27	adantr 485	. . 3 ⊢ ((𝜑 ∧ 𝑋 = 0 ) → ((𝐸 + 𝐺)‘𝐵) = 𝑄)
29		lclkrlem2f.nx	. . . 4 ⊢ (𝜑 → (¬ 𝑋 ∈ ( ⊥ ‘{𝐵}) ∨ ¬ 𝑌 ∈ ( ⊥ ‘{𝐵})))
30	29	adantr 485	. . 3 ⊢ ((𝜑 ∧ 𝑋 = 0 ) → (¬ 𝑋 ∈ ( ⊥ ‘{𝐵}) ∨ ¬ 𝑌 ∈ ( ⊥ ‘{𝐵})))
31		simpr 489	. . 3 ⊢ ((𝜑 ∧ 𝑋 = 0 ) → 𝑋 = 0 )
32		lclkrlem2l.y	. . . 4 ⊢ (𝜑 → 𝑌 ∈ 𝑉)
33	32	adantr 485	. . 3 ⊢ ((𝜑 ∧ 𝑋 = 0 ) → 𝑌 ∈ 𝑉)
34	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 16, 18, 20, 22, 24, 26, 28, 30, 31, 33	lclkrlem2k 42176	. 2 ⊢ ((𝜑 ∧ 𝑋 = 0 ) → ( ⊥ ‘( ⊥ ‘(𝐿‘(𝐸 + 𝐺)))) = (𝐿‘(𝐸 + 𝐺)))
35	15	adantr 485	. . 3 ⊢ ((𝜑 ∧ 𝑌 = 0 ) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
36	17	adantr 485	. . 3 ⊢ ((𝜑 ∧ 𝑌 = 0 ) → 𝐵 ∈ (𝑉 ∖ { 0 }))
37	19	adantr 485	. . 3 ⊢ ((𝜑 ∧ 𝑌 = 0 ) → 𝐸 ∈ 𝐹)
38	21	adantr 485	. . 3 ⊢ ((𝜑 ∧ 𝑌 = 0 ) → 𝐺 ∈ 𝐹)
39	23	adantr 485	. . 3 ⊢ ((𝜑 ∧ 𝑌 = 0 ) → (𝐿‘𝐸) = ( ⊥ ‘{𝑋}))
40	25	adantr 485	. . 3 ⊢ ((𝜑 ∧ 𝑌 = 0 ) → (𝐿‘𝐺) = ( ⊥ ‘{𝑌}))
41	27	adantr 485	. . 3 ⊢ ((𝜑 ∧ 𝑌 = 0 ) → ((𝐸 + 𝐺)‘𝐵) = 𝑄)
42	29	adantr 485	. . 3 ⊢ ((𝜑 ∧ 𝑌 = 0 ) → (¬ 𝑋 ∈ ( ⊥ ‘{𝐵}) ∨ ¬ 𝑌 ∈ ( ⊥ ‘{𝐵})))
43		lclkrlem2l.x	. . . 4 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
44	43	adantr 485	. . 3 ⊢ ((𝜑 ∧ 𝑌 = 0 ) → 𝑋 ∈ 𝑉)
45		simpr 489	. . 3 ⊢ ((𝜑 ∧ 𝑌 = 0 ) → 𝑌 = 0 )
46	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 35, 36, 37, 38, 39, 40, 41, 42, 44, 45	lclkrlem2j 42175	. 2 ⊢ ((𝜑 ∧ 𝑌 = 0 ) → ( ⊥ ‘( ⊥ ‘(𝐿‘(𝐸 + 𝐺)))) = (𝐿‘(𝐸 + 𝐺)))
47	15	adantr 485	. . 3 ⊢ ((𝜑 ∧ (𝑋 ≠ 0 ∧ 𝑌 ≠ 0 )) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
48	17	adantr 485	. . 3 ⊢ ((𝜑 ∧ (𝑋 ≠ 0 ∧ 𝑌 ≠ 0 )) → 𝐵 ∈ (𝑉 ∖ { 0 }))
49	19	adantr 485	. . 3 ⊢ ((𝜑 ∧ (𝑋 ≠ 0 ∧ 𝑌 ≠ 0 )) → 𝐸 ∈ 𝐹)
50	21	adantr 485	. . 3 ⊢ ((𝜑 ∧ (𝑋 ≠ 0 ∧ 𝑌 ≠ 0 )) → 𝐺 ∈ 𝐹)
51	23	adantr 485	. . 3 ⊢ ((𝜑 ∧ (𝑋 ≠ 0 ∧ 𝑌 ≠ 0 )) → (𝐿‘𝐸) = ( ⊥ ‘{𝑋}))
52	25	adantr 485	. . 3 ⊢ ((𝜑 ∧ (𝑋 ≠ 0 ∧ 𝑌 ≠ 0 )) → (𝐿‘𝐺) = ( ⊥ ‘{𝑌}))
53	27	adantr 485	. . 3 ⊢ ((𝜑 ∧ (𝑋 ≠ 0 ∧ 𝑌 ≠ 0 )) → ((𝐸 + 𝐺)‘𝐵) = 𝑄)
54	29	adantr 485	. . 3 ⊢ ((𝜑 ∧ (𝑋 ≠ 0 ∧ 𝑌 ≠ 0 )) → (¬ 𝑋 ∈ ( ⊥ ‘{𝐵}) ∨ ¬ 𝑌 ∈ ( ⊥ ‘{𝐵})))
55	43	adantr 485	. . . 4 ⊢ ((𝜑 ∧ (𝑋 ≠ 0 ∧ 𝑌 ≠ 0 )) → 𝑋 ∈ 𝑉)
56		simprl 782	. . . 4 ⊢ ((𝜑 ∧ (𝑋 ≠ 0 ∧ 𝑌 ≠ 0 )) → 𝑋 ≠ 0 )
57		eldifsn 4755	. . . 4 ⊢ (𝑋 ∈ (𝑉 ∖ { 0 }) ↔ (𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ))
58	55, 56, 57	sylanbrc 594	. . 3 ⊢ ((𝜑 ∧ (𝑋 ≠ 0 ∧ 𝑌 ≠ 0 )) → 𝑋 ∈ (𝑉 ∖ { 0 }))
59	32	adantr 485	. . . 4 ⊢ ((𝜑 ∧ (𝑋 ≠ 0 ∧ 𝑌 ≠ 0 )) → 𝑌 ∈ 𝑉)
60		simprr 784	. . . 4 ⊢ ((𝜑 ∧ (𝑋 ≠ 0 ∧ 𝑌 ≠ 0 )) → 𝑌 ≠ 0 )
61		eldifsn 4755	. . . 4 ⊢ (𝑌 ∈ (𝑉 ∖ { 0 }) ↔ (𝑌 ∈ 𝑉 ∧ 𝑌 ≠ 0 ))
62	59, 60, 61	sylanbrc 594	. . 3 ⊢ ((𝜑 ∧ (𝑋 ≠ 0 ∧ 𝑌 ≠ 0 )) → 𝑌 ∈ (𝑉 ∖ { 0 }))
63	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 47, 48, 49, 50, 51, 52, 53, 54, 58, 62	lclkrlem2i 42174	. 2 ⊢ ((𝜑 ∧ (𝑋 ≠ 0 ∧ 𝑌 ≠ 0 )) → ( ⊥ ‘( ⊥ ‘(𝐿‘(𝐸 + 𝐺)))) = (𝐿‘(𝐸 + 𝐺)))
64	34, 46, 63	pm2.61da2ne 3052	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 4591 ‘cfv 6533 (class class class)co 7408 Basecbs 17265 +_gcplusg 17306 Scalarcsca 17309 0_gc0g 17488 LSSumclsm 19700 LSpanclspn 21066 LSHypclsh 39634 LFnlclfn 39716 LKerclk 39744 LDualcld 39782 HLchlt 40009 LHypclh 40643 DVecHcdvh 41737 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: lclkrlem2q 42182

W3C validator