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 43164

Description: Lemma for hdmapadd 43166. (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 2763	. . . . . 6 ⊢ (0_g‘𝐶) = (0_g‘𝐶)
15		hdmap11.j	. . . . . 6 ⊢ 𝐽 = ((HVMap‘𝐾)‘𝑊)
16		eqid 2763	. . . . . . 7 ⊢ (Base‘𝐾) = (Base‘𝐾)
17		eqid 2763	. . . . . . 7 ⊢ ((LTrn‘𝐾)‘𝑊) = ((LTrn‘𝐾)‘𝑊)
18		hdmap11.e	. . . . . . 7 ⊢ 𝐸 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩
19	1, 16, 17, 2, 3, 5, 18, 13	dvheveccl 42435	. . . . . 6 ⊢ (𝜑 → 𝐸 ∈ (𝑉 ∖ { 0 }))
20	1, 2, 3, 5, 7, 8, 14, 15, 13, 19	hvmapcl2 43089	. . . . 5 ⊢ (𝜑 → (𝐽‘𝐸) ∈ (𝐷 ∖ {(0_g‘𝐶)}))
21	20	eldifad 4054	. . . 4 ⊢ (𝜑 → (𝐽‘𝐸) ∈ 𝐷)
22	1, 2, 3, 5, 6, 7, 10, 11, 15, 13, 19	mapdhvmap 43092	. . . 4 ⊢ (𝜑 → (𝑀‘(𝑁‘{𝐸})) = (𝐿‘{(𝐽‘𝐸)}))
23		hdmap11lem0.2a	. . . . 5 ⊢ (𝜑 → (𝑁‘{𝑧}) ≠ (𝑁‘{𝐸}))
24	23	necomd 3014	. . . 4 ⊢ (𝜑 → (𝑁‘{𝐸}) ≠ (𝑁‘{𝑧}))
25		hdmap11lem0.1a	. . . 4 ⊢ (𝜑 → 𝑧 ∈ 𝑉)
26	1, 2, 3, 5, 6, 7, 8, 10, 11, 12, 13, 21, 22, 24, 19, 25	hdmap1cl 43127	. . 3 ⊢ (𝜑 → (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩) ∈ 𝐷)
27		eqid 2763	. . . 4 ⊢ (LSubSp‘𝑈) = (LSubSp‘𝑈)
28	1, 2, 13	dvhlmod 42433	. . . 4 ⊢ (𝜑 → 𝑈 ∈ LMod)
29		hdmap11.x	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
30		hdmap11.y	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ 𝑉)
31	3, 27, 6, 28, 29, 30	lspprcl 21304	. . . 4 ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) ∈ (LSubSp‘𝑈))
32		hdmap11lem0.6	. . . 4 ⊢ (𝜑 → ¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}))
33	5, 27, 28, 31, 25, 32	lssneln0 21279	. . 3 ⊢ (𝜑 → 𝑧 ∈ (𝑉 ∖ { 0 }))
34		eqidd 2764	. . . . 5 ⊢ (𝜑 → (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩) = (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩))
35		eqid 2763	. . . . . 6 ⊢ (-_g‘𝑈) = (-_g‘𝑈)
36		eqid 2763	. . . . . 6 ⊢ (-_g‘𝐶) = (-_g‘𝐶)
37	1, 2, 3, 35, 5, 6, 7, 8, 36, 10, 11, 12, 13, 19, 21, 33, 26, 24, 22	hdmap1eq 43124	. . . . 5 ⊢ (𝜑 → ((𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩) = (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩) ↔ ((𝑀‘(𝑁‘{𝑧})) = (𝐿‘{(𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩)}) ∧ (𝑀‘(𝑁‘{(𝐸(-_g‘𝑈)𝑧)})) = (𝐿‘{((𝐽‘𝐸)(-_g‘𝐶)(𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩))}))))
38	34, 37	mpbid 235	. . . 4 ⊢ (𝜑 → ((𝑀‘(𝑁‘{𝑧})) = (𝐿‘{(𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩)}) ∧ (𝑀‘(𝑁‘{(𝐸(-_g‘𝑈)𝑧)})) = (𝐿‘{((𝐽‘𝐸)(-_g‘𝐶)(𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩))})))
39	38	simpld 500	. . 3 ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑧})) = (𝐿‘{(𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩)}))
40	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 26, 33, 29, 30, 32, 39	hdmap1l6 43144	. 2 ⊢ (𝜑 → (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), (𝑋 + 𝑌)⟩) = ((𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), 𝑋⟩) + (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), 𝑌⟩)))
41		hdmap11.s	. . 3 ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)
42	3, 4	lmodvacl 21201	. . . 4 ⊢ ((𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 + 𝑌) ∈ 𝑉)
43	28, 29, 30, 42	syl3anc 1399	. . 3 ⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝑉)
44	1, 2, 13	dvhlvec 42432	. . . 4 ⊢ (𝜑 → 𝑈 ∈ LVec)
45	19	eldifad 4054	. . . 4 ⊢ (𝜑 → 𝐸 ∈ 𝑉)
46	3, 4, 6, 28, 29, 30	lspprvacl 21325	. . . . . . 7 ⊢ (𝜑 → (𝑋 + 𝑌) ∈ (𝑁‘{𝑋, 𝑌}))
47	27, 6, 28, 31, 46	ellspsn5 21322	. . . . . 6 ⊢ (𝜑 → (𝑁‘{(𝑋 + 𝑌)}) ⊆ (𝑁‘{𝑋, 𝑌}))
48	47, 32	ssneldd 3916	. . . . 5 ⊢ (𝜑 → ¬ 𝑧 ∈ (𝑁‘{(𝑋 + 𝑌)}))
49	3, 6, 28, 25, 43, 48	lspsnne2 21447	. . . 4 ⊢ (𝜑 → (𝑁‘{𝑧}) ≠ (𝑁‘{(𝑋 + 𝑌)}))
50	3, 6, 5, 44, 45, 43, 33, 23, 49	hdmaplem4 43097	. . 3 ⊢ (𝜑 → ¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{(𝑋 + 𝑌)})))
51	1, 18, 2, 3, 6, 7, 8, 15, 12, 41, 13, 43, 25, 50	hdmapval2 43155	. 2 ⊢ (𝜑 → (𝑆‘(𝑋 + 𝑌)) = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), (𝑋 + 𝑌)⟩))
52	3, 6, 44, 25, 29, 30, 32	lspindpi 21461	. . . . . 6 ⊢ (𝜑 → ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑌})))
53	52	simpld 500	. . . . 5 ⊢ (𝜑 → (𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}))
54	3, 6, 5, 44, 45, 29, 33, 23, 53	hdmaplem4 43097	. . . 4 ⊢ (𝜑 → ¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑋})))
55	1, 18, 2, 3, 6, 7, 8, 15, 12, 41, 13, 29, 25, 54	hdmapval2 43155	. . 3 ⊢ (𝜑 → (𝑆‘𝑋) = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), 𝑋⟩))
56	52	simprd 501	. . . . 5 ⊢ (𝜑 → (𝑁‘{𝑧}) ≠ (𝑁‘{𝑌}))
57	3, 6, 5, 44, 45, 30, 33, 23, 56	hdmaplem4 43097	. . . 4 ⊢ (𝜑 → ¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑌})))
58	1, 18, 2, 3, 6, 7, 8, 15, 12, 41, 13, 30, 25, 57	hdmapval2 43155	. . 3 ⊢ (𝜑 → (𝑆‘𝑌) = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), 𝑌⟩))
59	55, 58	oveq12d 7469	. 2 ⊢ (𝜑 → ((𝑆‘𝑋) + (𝑆‘𝑌)) = ((𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), 𝑋⟩) + (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), 𝑌⟩)))
60	40, 51, 59	3eqtr4d 2808	1 ⊢ (𝜑 → (𝑆‘(𝑋 + 𝑌)) = ((𝑆‘𝑋) + (𝑆‘𝑌)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 401 = wceq 1570 ∈ wcel 2147 ≠ wne 2959 {csn 4588 {cpr 4590 ⟨cop 4840 ⟨cotp 4863 I cid 5552 ↾ cres 5660 ‘cfv 6566 (class class class)co 7451 Basecbs 17431 +_gcplusg 17472 0_gc0g 17660 -_gcsg 19196 LModclmod 21186 LSubSpclss 21257 LSpanclspn 21297 HLchlt 40673 LHypclh 41307 LTrncltrn 41424 DVecHcdvh 42401 LCDualclcd 42909 mapdcmpd 42947 HVMapchvm 43079 HDMap1chdma1 43114 HDMapchdma 43115

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5238 ax-sep 5255 ax-nul 5266 ax-pow 5334 ax-pr 5398 ax-un 7783 ax-cnex 11295 ax-resscn 11296 ax-1cn 11297 ax-icn 11298 ax-addcl 11299 ax-addrcl 11300 ax-mulcl 11301 ax-mulrcl 11302 ax-mulcom 11303 ax-addass 11304 ax-mulass 11305 ax-distr 11306 ax-i2m1 11307 ax-1ne0 11308 ax-1rid 11309 ax-rnegex 11310 ax-rrecex 11311 ax-cnre 11312 ax-pre-lttri 11313 ax-pre-lttrn 11314 ax-pre-ltadd 11315 ax-pre-mulgt0 11316 ax-riotaBAD 40276

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4841 df-ot 4864 df-uni 4873 df-int 4913 df-iun 4958 df-iin 4959 df-br 5109 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-we 5613 df-xp 5664 df-rel 5665 df-cnv 5666 df-co 5667 df-dm 5668 df-rn 5669 df-res 5670 df-ima 5671 df-pred 6330 df-ord 6391 df-on 6392 df-lim 6393 df-suc 6394 df-iota 6520 df-fun 6568 df-fn 6569 df-f 6570 df-f1 6571 df-fo 6572 df-f1o 6573 df-fv 6574 df-riota 7408 df-ov 7454 df-oprab 7455 df-mpo 7456 df-of 7725 df-om 7912 df-1st 8035 df-2nd 8036 df-tpos 8281 df-undef 8328 df-frecs 8337 df-wrecs 8368 df-recs 8417 df-rdg 8456 df-1o 8514 df-2o 8515 df-er 8755 df-map 8887 df-en 9012 df-dom 9013 df-sdom 9014 df-fin 9015 df-pnf 11384 df-mnf 11385 df-xr 11386 df-ltxr 11387 df-le 11388 df-sub 11582 df-neg 11583 df-nn 12376 df-2 12445 df-3 12446 df-4 12447 df-5 12448 df-6 12449 df-n0 12647 df-z 12734 df-uz 13006 df-fz 13680 df-struct 17369 df-sets 17386 df-slot 17404 df-ndx 17416 df-base 17432 df-ress 17453 df-plusg 17486 df-mulr 17487 df-sca 17489 df-vsca 17490 df-0g 17662 df-mre 17806 df-mrc 17807 df-acs 17809 df-proset 18518 df-poset 18537 df-plt 18552 df-lub 18568 df-glb 18569 df-join 18570 df-meet 18571 df-p0 18647 df-p1 18648 df-lat 18656 df-clat 18723 df-mgm 18866 df-sgrp 18958 df-mnd 18974 df-submnd 19029 df-grp 19197 df-minusg 19198 df-sbg 19199 df-subg 19383 df-cntz 19582 df-oppg 19611 df-lsm 19901 df-cmn 20047 df-abl 20048 df-mgp 20412 df-rng 20426 df-ur 20459 df-ring 20512 df-oppr 20618 df-dvdsr 20638 df-unit 20639 df-invr 20669 df-dvr 20682 df-nzr 20814 df-rlreg 20997 df-domn 20998 df-drng 21033 df-lmod 21188 df-lss 21258 df-lsp 21298 df-lvec 21429 df-lsatoms 40299 df-lshyp 40300 df-lcv 40342 df-lfl 40381 df-lkr 40409 df-ldual 40447 df-oposet 40499 df-ol 40501 df-oml 40502 df-covers 40589 df-ats 40590 df-atl 40621 df-cvlat 40645 df-hlat 40674 df-llines 40821 df-lplanes 40822 df-lvols 40823 df-lines 40824 df-psubsp 40826 df-pmap 40827 df-padd 41119 df-lhyp 41311 df-laut 41312 df-ldil 41427 df-ltrn 41428 df-trl 41482 df-tgrp 42066 df-tendo 42078 df-edring 42080 df-dveca 42326 df-disoa 42352 df-dvech 42402 df-dib 42462 df-dic 42496 df-dih 42552 df-doch 42671 df-djh 42718 df-lcdual 42910 df-mapd 42948 df-hvmap 43080 df-hdmap1 43116 df-hdmap 43117

This theorem is used by: hdmap11lem2 43165

W3C validator