hdmap11lem1 - Mathbox for Norm Megill

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

Theorem hdmap11lem1 42504

Description: Lemma for hdmapadd 42506. (Contributed by NM, 26-May-2015.)

**Hypotheses**
Ref	Expression
hdmap11.h	⊢ 𝐻 = (LHyp‘𝐾)
hdmap11.u	⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
hdmap11.v	⊢ 𝑉 = (Base‘𝑈)
hdmap11.p	⊢ + = (+_g‘𝑈)
hdmap11.c	⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)
hdmap11.a	⊢ ✚ = (+_g‘𝐶)
hdmap11.s	⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)
hdmap11.k	⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
hdmap11.x	⊢ (𝜑 → 𝑋 ∈ 𝑉)
hdmap11.y	⊢ (𝜑 → 𝑌 ∈ 𝑉)
hdmap11.e	⊢ 𝐸 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩
hdmap11.o	⊢ 0 = (0_g‘𝑈)
hdmap11.n	⊢ 𝑁 = (LSpan‘𝑈)
hdmap11.d	⊢ 𝐷 = (Base‘𝐶)
hdmap11.l	⊢ 𝐿 = (LSpan‘𝐶)
hdmap11.m	⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)
hdmap11.j	⊢ 𝐽 = ((HVMap‘𝐾)‘𝑊)
hdmap11.i	⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊)
hdmap11lem0.1a	⊢ (𝜑 → 𝑧 ∈ 𝑉)
hdmap11lem0.6	⊢ (𝜑 → ¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}))
hdmap11lem0.2a	⊢ (𝜑 → (𝑁‘{𝑧}) ≠ (𝑁‘{𝐸}))

**Assertion**
Ref	Expression
hdmap11lem1	⊢ (𝜑 → (𝑆‘(𝑋 + 𝑌)) = ((𝑆‘𝑋) ✚ (𝑆‘𝑌)))

**Proof of Theorem hdmap11lem1**
Step	Hyp	Ref	Expression
1		hdmap11.h	. . 3 ⊢ 𝐻 = (LHyp‘𝐾)
2		hdmap11.u	. . 3 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
3		hdmap11.v	. . 3 ⊢ 𝑉 = (Base‘𝑈)
4		hdmap11.p	. . 3 ⊢ + = (+_g‘𝑈)
5		hdmap11.o	. . 3 ⊢ 0 = (0_g‘𝑈)
6		hdmap11.n	. . 3 ⊢ 𝑁 = (LSpan‘𝑈)
7		hdmap11.c	. . 3 ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)
8		hdmap11.d	. . 3 ⊢ 𝐷 = (Base‘𝐶)
9		hdmap11.a	. . 3 ⊢ ✚ = (+_g‘𝐶)
10		hdmap11.l	. . 3 ⊢ 𝐿 = (LSpan‘𝐶)
11		hdmap11.m	. . 3 ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)
12		hdmap11.i	. . 3 ⊢ 𝐼 = ((HDMap1‘𝐾)‘𝑊)
13		hdmap11.k	. . 3 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
14		eqid 2769	. . . . . 6 ⊢ (0_g‘𝐶) = (0_g‘𝐶)
15		hdmap11.j	. . . . . 6 ⊢ 𝐽 = ((HVMap‘𝐾)‘𝑊)
16		eqid 2769	. . . . . . 7 ⊢ (Base‘𝐾) = (Base‘𝐾)
17		eqid 2769	. . . . . . 7 ⊢ ((LTrn‘𝐾)‘𝑊) = ((LTrn‘𝐾)‘𝑊)
18		hdmap11.e	. . . . . . 7 ⊢ 𝐸 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩
19	1, 16, 17, 2, 3, 5, 18, 13	dvheveccl 41775	. . . . . 6 ⊢ (𝜑 → 𝐸 ∈ (𝑉 ∖ { 0 }))
20	1, 2, 3, 5, 7, 8, 14, 15, 13, 19	hvmapcl2 42429	. . . . 5 ⊢ (𝜑 → (𝐽‘𝐸) ∈ (𝐷 ∖ {(0_g‘𝐶)}))
21	20	eldifad 3925	. . . 4 ⊢ (𝜑 → (𝐽‘𝐸) ∈ 𝐷)
22	1, 2, 3, 5, 6, 7, 10, 11, 15, 13, 19	mapdhvmap 42432	. . . 4 ⊢ (𝜑 → (𝑀‘(𝑁‘{𝐸})) = (𝐿‘{(𝐽‘𝐸)}))
23		hdmap11lem0.2a	. . . . 5 ⊢ (𝜑 → (𝑁‘{𝑧}) ≠ (𝑁‘{𝐸}))
24	23	necomd 3019	. . . 4 ⊢ (𝜑 → (𝑁‘{𝐸}) ≠ (𝑁‘{𝑧}))
25		hdmap11lem0.1a	. . . 4 ⊢ (𝜑 → 𝑧 ∈ 𝑉)
26	1, 2, 3, 5, 6, 7, 8, 10, 11, 12, 13, 21, 22, 24, 19, 25	hdmap1cl 42467	. . 3 ⊢ (𝜑 → (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩) ∈ 𝐷)
27		eqid 2769	. . . 4 ⊢ (LSubSp‘𝑈) = (LSubSp‘𝑈)
28	1, 2, 13	dvhlmod 41773	. . . 4 ⊢ (𝜑 → 𝑈 ∈ LMod)
29		hdmap11.x	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
30		hdmap11.y	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ 𝑉)
31	3, 27, 6, 28, 29, 30	lspprcl 21076	. . . 4 ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) ∈ (LSubSp‘𝑈))
32		hdmap11lem0.6	. . . 4 ⊢ (𝜑 → ¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}))
33	5, 27, 28, 31, 25, 32	lssneln0 21051	. . 3 ⊢ (𝜑 → 𝑧 ∈ (𝑉 ∖ { 0 }))
34		eqidd 2770	. . . . 5 ⊢ (𝜑 → (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩) = (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩))
35		eqid 2769	. . . . . 6 ⊢ (-_g‘𝑈) = (-_g‘𝑈)
36		eqid 2769	. . . . . 6 ⊢ (-_g‘𝐶) = (-_g‘𝐶)
37	1, 2, 3, 35, 5, 6, 7, 8, 36, 10, 11, 12, 13, 19, 21, 33, 26, 24, 22	hdmap1eq 42464	. . . . 5 ⊢ (𝜑 → ((𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩) = (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩) ↔ ((𝑀‘(𝑁‘{𝑧})) = (𝐿‘{(𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩)}) ∧ (𝑀‘(𝑁‘{(𝐸(-_g‘𝑈)𝑧)})) = (𝐿‘{((𝐽‘𝐸)(-_g‘𝐶)(𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩))}))))
38	34, 37	mpbid 235	. . . 4 ⊢ (𝜑 → ((𝑀‘(𝑁‘{𝑧})) = (𝐿‘{(𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩)}) ∧ (𝑀‘(𝑁‘{(𝐸(-_g‘𝑈)𝑧)})) = (𝐿‘{((𝐽‘𝐸)(-_g‘𝐶)(𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩))})))
39	38	simpld 499	. . 3 ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑧})) = (𝐿‘{(𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩)}))
40	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 26, 33, 29, 30, 32, 39	hdmap1l6 42484	. 2 ⊢ (𝜑 → (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), (𝑋 + 𝑌)⟩) = ((𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), 𝑋⟩) ✚ (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), 𝑌⟩)))
41		hdmap11.s	. . 3 ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)
42	3, 4	lmodvacl 20973	. . . 4 ⊢ ((𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 + 𝑌) ∈ 𝑉)
43	28, 29, 30, 42	syl3anc 1396	. . 3 ⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝑉)
44	1, 2, 13	dvhlvec 41772	. . . 4 ⊢ (𝜑 → 𝑈 ∈ LVec)
45	19	eldifad 3925	. . . 4 ⊢ (𝜑 → 𝐸 ∈ 𝑉)
46	3, 4, 6, 28, 29, 30	lspprvacl 21097	. . . . . . 7 ⊢ (𝜑 → (𝑋 + 𝑌) ∈ (𝑁‘{𝑋, 𝑌}))
47	27, 6, 28, 31, 46	ellspsn5 21094	. . . . . 6 ⊢ (𝜑 → (𝑁‘{(𝑋 + 𝑌)}) ⊆ (𝑁‘{𝑋, 𝑌}))
48	47, 32	ssneldd 3948	. . . . 5 ⊢ (𝜑 → ¬ 𝑧 ∈ (𝑁‘{(𝑋 + 𝑌)}))
49	3, 6, 28, 25, 43, 48	lspsnne2 21219	. . . 4 ⊢ (𝜑 → (𝑁‘{𝑧}) ≠ (𝑁‘{(𝑋 + 𝑌)}))
50	3, 6, 5, 44, 45, 43, 33, 23, 49	hdmaplem4 42437	. . 3 ⊢ (𝜑 → ¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{(𝑋 + 𝑌)})))
51	1, 18, 2, 3, 6, 7, 8, 15, 12, 41, 13, 43, 25, 50	hdmapval2 42495	. 2 ⊢ (𝜑 → (𝑆‘(𝑋 + 𝑌)) = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), (𝑋 + 𝑌)⟩))
52	3, 6, 44, 25, 29, 30, 32	lspindpi 21233	. . . . . 6 ⊢ (𝜑 → ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑌})))
53	52	simpld 499	. . . . 5 ⊢ (𝜑 → (𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}))
54	3, 6, 5, 44, 45, 29, 33, 23, 53	hdmaplem4 42437	. . . 4 ⊢ (𝜑 → ¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑋})))
55	1, 18, 2, 3, 6, 7, 8, 15, 12, 41, 13, 29, 25, 54	hdmapval2 42495	. . 3 ⊢ (𝜑 → (𝑆‘𝑋) = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), 𝑋⟩))
56	52	simprd 500	. . . . 5 ⊢ (𝜑 → (𝑁‘{𝑧}) ≠ (𝑁‘{𝑌}))
57	3, 6, 5, 44, 45, 30, 33, 23, 56	hdmaplem4 42437	. . . 4 ⊢ (𝜑 → ¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑌})))
58	1, 18, 2, 3, 6, 7, 8, 15, 12, 41, 13, 30, 25, 57	hdmapval2 42495	. . 3 ⊢ (𝜑 → (𝑆‘𝑌) = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), 𝑌⟩))
59	55, 58	oveq12d 7429	. 2 ⊢ (𝜑 → ((𝑆‘𝑋) ✚ (𝑆‘𝑌)) = ((𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), 𝑋⟩) ✚ (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), 𝑌⟩)))
60	40, 51, 59	3eqtr4d 2814	1 ⊢ (𝜑 → (𝑆‘(𝑋 + 𝑌)) = ((𝑆‘𝑋) ✚ (𝑆‘𝑌)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 400 = wceq 1567 ∈ wcel 2149 ≠ wne 2964 {csn 4594 {cpr 4596 ⟨cop 4600 ⟨cotp 4602 I cid 5556 ↾ cres 5664 ‘cfv 6537 (class class class)co 7411 Basecbs 17268 +_gcplusg 17309 0_gc0g 17491 -_gcsg 19001 LModclmod 20958 LSubSpclss 21029 LSpanclspn 21069 HLchlt 40013 LHypclh 40647 LTrncltrn 40764 DVecHcdvh 41741 LCDualclcd 42249 mapdcmpd 42287 HVMapchvm 42419 HDMap1chdma1 42454 HDMapchdma 42455

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 11155 ax-resscn 11156 ax-1cn 11157 ax-icn 11158 ax-addcl 11159 ax-addrcl 11160 ax-mulcl 11161 ax-mulrcl 11162 ax-mulcom 11163 ax-addass 11164 ax-mulass 11165 ax-distr 11166 ax-i2m1 11167 ax-1ne0 11168 ax-1rid 11169 ax-rnegex 11170 ax-rrecex 11171 ax-cnre 11172 ax-pre-lttri 11173 ax-pre-lttrn 11174 ax-pre-ltadd 11175 ax-pre-mulgt0 11176 ax-riotaBAD 39616

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-ot 4603 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 7862 df-1st 7985 df-2nd 7986 df-tpos 8221 df-undef 8268 df-frecs 8277 df-wrecs 8308 df-recs 8357 df-rdg 8396 df-1o 8452 df-2o 8453 df-er 8693 df-map 8825 df-en 8943 df-dom 8944 df-sdom 8945 df-fin 8946 df-pnf 11244 df-mnf 11245 df-xr 11246 df-ltxr 11247 df-le 11248 df-sub 11442 df-neg 11443 df-nn 12233 df-2 12302 df-3 12303 df-4 12304 df-5 12305 df-6 12306 df-n0 12504 df-z 12591 df-uz 12862 df-fz 13535 df-struct 17206 df-sets 17223 df-slot 17241 df-ndx 17253 df-base 17269 df-ress 17290 df-plusg 17322 df-mulr 17323 df-sca 17325 df-vsca 17326 df-0g 17493 df-mre 17637 df-mrc 17638 df-acs 17640 df-proset 18349 df-poset 18368 df-plt 18383 df-lub 18399 df-glb 18400 df-join 18401 df-meet 18402 df-p0 18478 df-p1 18479 df-lat 18487 df-clat 18554 df-mgm 18697 df-sgrp 18776 df-mnd 18792 df-submnd 18841 df-grp 19002 df-minusg 19003 df-sbg 19004 df-subg 19188 df-cntz 19386 df-oppg 19415 df-lsm 19705 df-cmn 19851 df-abl 19852 df-mgp 20216 df-rng 20230 df-ur 20263 df-ring 20316 df-oppr 20418 df-dvdsr 20438 df-unit 20439 df-invr 20469 df-dvr 20482 df-nzr 20595 df-rlreg 20778 df-domn 20779 df-drng 20814 df-lmod 20960 df-lss 21030 df-lsp 21070 df-lvec 21201 df-lsatoms 39639 df-lshyp 39640 df-lcv 39682 df-lfl 39721 df-lkr 39749 df-ldual 39787 df-oposet 39839 df-ol 39841 df-oml 39842 df-covers 39929 df-ats 39930 df-atl 39961 df-cvlat 39985 df-hlat 40014 df-llines 40161 df-lplanes 40162 df-lvols 40163 df-lines 40164 df-psubsp 40166 df-pmap 40167 df-padd 40459 df-lhyp 40651 df-laut 40652 df-ldil 40767 df-ltrn 40768 df-trl 40822 df-tgrp 41406 df-tendo 41418 df-edring 41420 df-dveca 41666 df-disoa 41692 df-dvech 41742 df-dib 41802 df-dic 41836 df-dih 41892 df-doch 42011 df-djh 42058 df-lcdual 42250 df-mapd 42288 df-hvmap 42420 df-hdmap1 42456 df-hdmap 42457

This theorem is referenced by: hdmap11lem2 42505

W3C validator