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 39881

Description: Lemma for hdmapadd 39883. (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 2733	. . . . . 6 ⊢ (0_g‘𝐶) = (0_g‘𝐶)
15		hdmap11.j	. . . . . 6 ⊢ 𝐽 = ((HVMap‘𝐾)‘𝑊)
16		eqid 2733	. . . . . . 7 ⊢ (Base‘𝐾) = (Base‘𝐾)
17		eqid 2733	. . . . . . 7 ⊢ ((LTrn‘𝐾)‘𝑊) = ((LTrn‘𝐾)‘𝑊)
18		hdmap11.e	. . . . . . 7 ⊢ 𝐸 = ⟨( I ↾ (Base‘𝐾)), ( I ↾ ((LTrn‘𝐾)‘𝑊))⟩
19	1, 16, 17, 2, 3, 5, 18, 13	dvheveccl 39152	. . . . . 6 ⊢ (𝜑 → 𝐸 ∈ (𝑉 ∖ { 0 }))
20	1, 2, 3, 5, 7, 8, 14, 15, 13, 19	hvmapcl2 39806	. . . . 5 ⊢ (𝜑 → (𝐽‘𝐸) ∈ (𝐷 ∖ {(0_g‘𝐶)}))
21	20	eldifad 3901	. . . 4 ⊢ (𝜑 → (𝐽‘𝐸) ∈ 𝐷)
22	1, 2, 3, 5, 6, 7, 10, 11, 15, 13, 19	mapdhvmap 39809	. . . 4 ⊢ (𝜑 → (𝑀‘(𝑁‘{𝐸})) = (𝐿‘{(𝐽‘𝐸)}))
23		hdmap11lem0.2a	. . . . 5 ⊢ (𝜑 → (𝑁‘{𝑧}) ≠ (𝑁‘{𝐸}))
24	23	necomd 2994	. . . 4 ⊢ (𝜑 → (𝑁‘{𝐸}) ≠ (𝑁‘{𝑧}))
25		hdmap11lem0.1a	. . . 4 ⊢ (𝜑 → 𝑧 ∈ 𝑉)
26	1, 2, 3, 5, 6, 7, 8, 10, 11, 12, 13, 21, 22, 24, 19, 25	hdmap1cl 39844	. . 3 ⊢ (𝜑 → (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩) ∈ 𝐷)
27		eqid 2733	. . . 4 ⊢ (LSubSp‘𝑈) = (LSubSp‘𝑈)
28	1, 2, 13	dvhlmod 39150	. . . 4 ⊢ (𝜑 → 𝑈 ∈ LMod)
29		hdmap11.x	. . . . 5 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
30		hdmap11.y	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ 𝑉)
31	3, 27, 6, 28, 29, 30	lspprcl 20268	. . . 4 ⊢ (𝜑 → (𝑁‘{𝑋, 𝑌}) ∈ (LSubSp‘𝑈))
32		hdmap11lem0.6	. . . 4 ⊢ (𝜑 → ¬ 𝑧 ∈ (𝑁‘{𝑋, 𝑌}))
33	5, 27, 28, 31, 25, 32	lssneln0 20242	. . 3 ⊢ (𝜑 → 𝑧 ∈ (𝑉 ∖ { 0 }))
34		eqidd 2734	. . . . 5 ⊢ (𝜑 → (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩) = (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩))
35		eqid 2733	. . . . . 6 ⊢ (-_g‘𝑈) = (-_g‘𝑈)
36		eqid 2733	. . . . . 6 ⊢ (-_g‘𝐶) = (-_g‘𝐶)
37	1, 2, 3, 35, 5, 6, 7, 8, 36, 10, 11, 12, 13, 19, 21, 33, 26, 24, 22	hdmap1eq 39841	. . . . 5 ⊢ (𝜑 → ((𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩) = (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩) ↔ ((𝑀‘(𝑁‘{𝑧})) = (𝐿‘{(𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩)}) ∧ (𝑀‘(𝑁‘{(𝐸(-_g‘𝑈)𝑧)})) = (𝐿‘{((𝐽‘𝐸)(-_g‘𝐶)(𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩))}))))
38	34, 37	mpbid 231	. . . 4 ⊢ (𝜑 → ((𝑀‘(𝑁‘{𝑧})) = (𝐿‘{(𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩)}) ∧ (𝑀‘(𝑁‘{(𝐸(-_g‘𝑈)𝑧)})) = (𝐿‘{((𝐽‘𝐸)(-_g‘𝐶)(𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩))})))
39	38	simpld 494	. . 3 ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑧})) = (𝐿‘{(𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩)}))
40	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 26, 33, 29, 30, 32, 39	hdmap1l6 39861	. 2 ⊢ (𝜑 → (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), (𝑋 + 𝑌)⟩) = ((𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), 𝑋⟩) ✚ (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), 𝑌⟩)))
41		hdmap11.s	. . 3 ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)
42	3, 4	lmodvacl 20165	. . . 4 ⊢ ((𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 + 𝑌) ∈ 𝑉)
43	28, 29, 30, 42	syl3anc 1369	. . 3 ⊢ (𝜑 → (𝑋 + 𝑌) ∈ 𝑉)
44	1, 2, 13	dvhlvec 39149	. . . 4 ⊢ (𝜑 → 𝑈 ∈ LVec)
45	19	eldifad 3901	. . . 4 ⊢ (𝜑 → 𝐸 ∈ 𝑉)
46	3, 4, 6, 28, 29, 30	lspprvacl 20289	. . . . . . 7 ⊢ (𝜑 → (𝑋 + 𝑌) ∈ (𝑁‘{𝑋, 𝑌}))
47	27, 6, 28, 31, 46	lspsnel5a 20286	. . . . . 6 ⊢ (𝜑 → (𝑁‘{(𝑋 + 𝑌)}) ⊆ (𝑁‘{𝑋, 𝑌}))
48	47, 32	ssneldd 3926	. . . . 5 ⊢ (𝜑 → ¬ 𝑧 ∈ (𝑁‘{(𝑋 + 𝑌)}))
49	3, 6, 28, 25, 43, 48	lspsnne2 20408	. . . 4 ⊢ (𝜑 → (𝑁‘{𝑧}) ≠ (𝑁‘{(𝑋 + 𝑌)}))
50	3, 6, 5, 44, 45, 43, 33, 23, 49	hdmaplem4 39814	. . 3 ⊢ (𝜑 → ¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{(𝑋 + 𝑌)})))
51	1, 18, 2, 3, 6, 7, 8, 15, 12, 41, 13, 43, 25, 50	hdmapval2 39872	. 2 ⊢ (𝜑 → (𝑆‘(𝑋 + 𝑌)) = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), (𝑋 + 𝑌)⟩))
52	3, 6, 44, 25, 29, 30, 32	lspindpi 20422	. . . . . 6 ⊢ (𝜑 → ((𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑧}) ≠ (𝑁‘{𝑌})))
53	52	simpld 494	. . . . 5 ⊢ (𝜑 → (𝑁‘{𝑧}) ≠ (𝑁‘{𝑋}))
54	3, 6, 5, 44, 45, 29, 33, 23, 53	hdmaplem4 39814	. . . 4 ⊢ (𝜑 → ¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑋})))
55	1, 18, 2, 3, 6, 7, 8, 15, 12, 41, 13, 29, 25, 54	hdmapval2 39872	. . 3 ⊢ (𝜑 → (𝑆‘𝑋) = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), 𝑋⟩))
56	52	simprd 495	. . . . 5 ⊢ (𝜑 → (𝑁‘{𝑧}) ≠ (𝑁‘{𝑌}))
57	3, 6, 5, 44, 45, 30, 33, 23, 56	hdmaplem4 39814	. . . 4 ⊢ (𝜑 → ¬ 𝑧 ∈ ((𝑁‘{𝐸}) ∪ (𝑁‘{𝑌})))
58	1, 18, 2, 3, 6, 7, 8, 15, 12, 41, 13, 30, 25, 57	hdmapval2 39872	. . 3 ⊢ (𝜑 → (𝑆‘𝑌) = (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), 𝑌⟩))
59	55, 58	oveq12d 7313	. 2 ⊢ (𝜑 → ((𝑆‘𝑋) ✚ (𝑆‘𝑌)) = ((𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), 𝑋⟩) ✚ (𝐼‘⟨𝑧, (𝐼‘⟨𝐸, (𝐽‘𝐸), 𝑧⟩), 𝑌⟩)))
60	40, 51, 59	3eqtr4d 2783	1 ⊢ (𝜑 → (𝑆‘(𝑋 + 𝑌)) = ((𝑆‘𝑋) ✚ (𝑆‘𝑌)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 395 = wceq 1537 ∈ wcel 2101 ≠ wne 2938 {csn 4564 {cpr 4566 ⟨cop 4570 ⟨cotp 4572 I cid 5490 ↾ cres 5593 ‘cfv 6447 (class class class)co 7295 Basecbs 16940 +_gcplusg 16990 0_gc0g 17178 -_gcsg 18607 LModclmod 20151 LSubSpclss 20221 LSpanclspn 20261 HLchlt 37390 LHypclh 38024 LTrncltrn 38141 DVecHcdvh 39118 LCDualclcd 39626 mapdcmpd 39664 HVMapchvm 39796 HDMap1chdma1 39831 HDMapchdma 39832

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2103 ax-9 2111 ax-10 2132 ax-11 2149 ax-12 2166 ax-ext 2704 ax-rep 5212 ax-sep 5226 ax-nul 5233 ax-pow 5291 ax-pr 5355 ax-un 7608 ax-cnex 10955 ax-resscn 10956 ax-1cn 10957 ax-icn 10958 ax-addcl 10959 ax-addrcl 10960 ax-mulcl 10961 ax-mulrcl 10962 ax-mulcom 10963 ax-addass 10964 ax-mulass 10965 ax-distr 10966 ax-i2m1 10967 ax-1ne0 10968 ax-1rid 10969 ax-rnegex 10970 ax-rrecex 10971 ax-cnre 10972 ax-pre-lttri 10973 ax-pre-lttrn 10974 ax-pre-ltadd 10975 ax-pre-mulgt0 10976 ax-riotaBAD 36993

This theorem depends on definitions: df-bi 206 df-an 396 df-or 844 df-3or 1086 df-3an 1087 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2063 df-mo 2535 df-eu 2564 df-clab 2711 df-cleq 2725 df-clel 2811 df-nfc 2884 df-ne 2939 df-nel 3045 df-ral 3060 df-rex 3069 df-rmo 3222 df-reu 3223 df-rab 3224 df-v 3436 df-sbc 3719 df-csb 3835 df-dif 3892 df-un 3894 df-in 3896 df-ss 3906 df-pss 3908 df-nul 4260 df-if 4463 df-pw 4538 df-sn 4565 df-pr 4567 df-tp 4569 df-op 4571 df-ot 4573 df-uni 4842 df-int 4883 df-iun 4929 df-iin 4930 df-br 5078 df-opab 5140 df-mpt 5161 df-tr 5195 df-id 5491 df-eprel 5497 df-po 5505 df-so 5506 df-fr 5546 df-we 5548 df-xp 5597 df-rel 5598 df-cnv 5599 df-co 5600 df-dm 5601 df-rn 5602 df-res 5603 df-ima 5604 df-pred 6206 df-ord 6273 df-on 6274 df-lim 6275 df-suc 6276 df-iota 6399 df-fun 6449 df-fn 6450 df-f 6451 df-f1 6452 df-fo 6453 df-f1o 6454 df-fv 6455 df-riota 7252 df-ov 7298 df-oprab 7299 df-mpo 7300 df-of 7553 df-om 7733 df-1st 7851 df-2nd 7852 df-tpos 8062 df-undef 8109 df-frecs 8117 df-wrecs 8148 df-recs 8222 df-rdg 8261 df-1o 8317 df-er 8518 df-map 8637 df-en 8754 df-dom 8755 df-sdom 8756 df-fin 8757 df-pnf 11039 df-mnf 11040 df-xr 11041 df-ltxr 11042 df-le 11043 df-sub 11235 df-neg 11236 df-nn 12002 df-2 12064 df-3 12065 df-4 12066 df-5 12067 df-6 12068 df-n0 12262 df-z 12348 df-uz 12611 df-fz 13268 df-struct 16876 df-sets 16893 df-slot 16911 df-ndx 16923 df-base 16941 df-ress 16970 df-plusg 17003 df-mulr 17004 df-sca 17006 df-vsca 17007 df-0g 17180 df-mre 17323 df-mrc 17324 df-acs 17326 df-proset 18041 df-poset 18059 df-plt 18076 df-lub 18092 df-glb 18093 df-join 18094 df-meet 18095 df-p0 18171 df-p1 18172 df-lat 18178 df-clat 18245 df-mgm 18354 df-sgrp 18403 df-mnd 18414 df-submnd 18459 df-grp 18608 df-minusg 18609 df-sbg 18610 df-subg 18780 df-cntz 18951 df-oppg 18978 df-lsm 19269 df-cmn 19416 df-abl 19417 df-mgp 19749 df-ur 19766 df-ring 19813 df-oppr 19890 df-dvdsr 19911 df-unit 19912 df-invr 19942 df-dvr 19953 df-drng 20021 df-lmod 20153 df-lss 20222 df-lsp 20262 df-lvec 20393 df-lsatoms 37016 df-lshyp 37017 df-lcv 37059 df-lfl 37098 df-lkr 37126 df-ldual 37164 df-oposet 37216 df-ol 37218 df-oml 37219 df-covers 37306 df-ats 37307 df-atl 37338 df-cvlat 37362 df-hlat 37391 df-llines 37538 df-lplanes 37539 df-lvols 37540 df-lines 37541 df-psubsp 37543 df-pmap 37544 df-padd 37836 df-lhyp 38028 df-laut 38029 df-ldil 38144 df-ltrn 38145 df-trl 38199 df-tgrp 38783 df-tendo 38795 df-edring 38797 df-dveca 39043 df-disoa 39069 df-dvech 39119 df-dib 39179 df-dic 39213 df-dih 39269 df-doch 39388 df-djh 39435 df-lcdual 39627 df-mapd 39665 df-hvmap 39797 df-hdmap1 39833 df-hdmap 39834

This theorem is referenced by: hdmap11lem2 39882

W3C validator