hdmap14lem4a - Mathbox for Norm Megill

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

Theorem hdmap14lem4a 42456

Description: Simplify (𝐴 ∖ {𝑄}) in hdmap14lem3 42455 to provide a slightly simpler definition later. (Contributed by NM, 31-May-2015.)

**Hypotheses**
Ref	Expression
hdmap14lem1.h	⊢ 𝐻 = (LHyp‘𝐾)
hdmap14lem1.u	⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
hdmap14lem1.v	⊢ 𝑉 = (Base‘𝑈)
hdmap14lem1.t	⊢ · = ( ·_𝑠 ‘𝑈)
hdmap14lem3.o	⊢ 0 = (0_g‘𝑈)
hdmap14lem1.r	⊢ 𝑅 = (Scalar‘𝑈)
hdmap14lem1.b	⊢ 𝐵 = (Base‘𝑅)
hdmap14lem1.z	⊢ 𝑍 = (0_g‘𝑅)
hdmap14lem1.c	⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)
hdmap14lem2.e	⊢ ∙ = ( ·_𝑠 ‘𝐶)
hdmap14lem1.l	⊢ 𝐿 = (LSpan‘𝐶)
hdmap14lem2.p	⊢ 𝑃 = (Scalar‘𝐶)
hdmap14lem2.a	⊢ 𝐴 = (Base‘𝑃)
hdmap14lem2.q	⊢ 𝑄 = (0_g‘𝑃)
hdmap14lem1.s	⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)
hdmap14lem1.k	⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
hdmap14lem3.x	⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))
hdmap14lem1.f	⊢ (𝜑 → 𝐹 ∈ (𝐵 ∖ {𝑍}))

**Assertion**
Ref	Expression
hdmap14lem4a	⊢ (𝜑 → (∃!𝑔 ∈ (𝐴 ∖ {𝑄})(𝑆‘(𝐹 · 𝑋)) = (𝑔 ∙ (𝑆‘𝑋)) ↔ ∃!𝑔 ∈ 𝐴 (𝑆‘(𝐹 · 𝑋)) = (𝑔 ∙ (𝑆‘𝑋))))

Distinct variable groups: 𝐴,𝑔 ∙ ,𝑔 𝑔,𝐹 𝑄,𝑔 𝑆,𝑔 · ,𝑔 𝑔,𝑋 𝜑,𝑔 Allowed substitution hints: 𝐵(𝑔) 𝐶(𝑔) 𝑃(𝑔) 𝑅(𝑔) 𝑈(𝑔) 𝐻(𝑔) 𝐾(𝑔) 𝐿(𝑔) 𝑉(𝑔) 𝑊(𝑔) 0 (𝑔) 𝑍(𝑔)

**Proof of Theorem hdmap14lem4a**
Step	Hyp	Ref	Expression
1		hdmap14lem1.h	. . . . . . . . 9 ⊢ 𝐻 = (LHyp‘𝐾)
2		hdmap14lem1.u	. . . . . . . . 9 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
3		hdmap14lem1.v	. . . . . . . . 9 ⊢ 𝑉 = (Base‘𝑈)
4		hdmap14lem3.o	. . . . . . . . 9 ⊢ 0 = (0_g‘𝑈)
5		hdmap14lem1.c	. . . . . . . . 9 ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)
6		eqid 2761	. . . . . . . . 9 ⊢ (0_g‘𝐶) = (0_g‘𝐶)
7		eqid 2761	. . . . . . . . 9 ⊢ (Base‘𝐶) = (Base‘𝐶)
8		hdmap14lem1.s	. . . . . . . . 9 ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)
9		hdmap14lem1.k	. . . . . . . . 9 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
10	1, 2, 9	dvhlmod 41695	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑈 ∈ LMod)
11		hdmap14lem1.f	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐹 ∈ (𝐵 ∖ {𝑍}))
12	11	eldifad 3914	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ∈ 𝐵)
13		hdmap14lem3.x	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))
14	13	eldifad 3914	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
15		hdmap14lem1.r	. . . . . . . . . . . 12 ⊢ 𝑅 = (Scalar‘𝑈)
16		hdmap14lem1.t	. . . . . . . . . . . 12 ⊢ · = ( ·_𝑠 ‘𝑈)
17		hdmap14lem1.b	. . . . . . . . . . . 12 ⊢ 𝐵 = (Base‘𝑅)
18	3, 15, 16, 17	lmodvscl 20933	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ LMod ∧ 𝐹 ∈ 𝐵 ∧ 𝑋 ∈ 𝑉) → (𝐹 · 𝑋) ∈ 𝑉)
19	10, 12, 14, 18	syl3anc 1389	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹 · 𝑋) ∈ 𝑉)
20		eldifsni 4747	. . . . . . . . . . . 12 ⊢ (𝐹 ∈ (𝐵 ∖ {𝑍}) → 𝐹 ≠ 𝑍)
21	11, 20	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝐹 ≠ 𝑍)
22		eldifsni 4747	. . . . . . . . . . . 12 ⊢ (𝑋 ∈ (𝑉 ∖ { 0 }) → 𝑋 ≠ 0 )
23	13, 22	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑋 ≠ 0 )
24		hdmap14lem1.z	. . . . . . . . . . . 12 ⊢ 𝑍 = (0_g‘𝑅)
25	1, 2, 9	dvhlvec 41694	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑈 ∈ LVec)
26	3, 16, 15, 17, 24, 4, 25, 12, 14	lvecvsn0 21167	. . . . . . . . . . 11 ⊢ (𝜑 → ((𝐹 · 𝑋) ≠ 0 ↔ (𝐹 ≠ 𝑍 ∧ 𝑋 ≠ 0 )))
27	21, 23, 26	mpbir2and 723	. . . . . . . . . 10 ⊢ (𝜑 → (𝐹 · 𝑋) ≠ 0 )
28		eldifsn 4743	. . . . . . . . . 10 ⊢ ((𝐹 · 𝑋) ∈ (𝑉 ∖ { 0 }) ↔ ((𝐹 · 𝑋) ∈ 𝑉 ∧ (𝐹 · 𝑋) ≠ 0 ))
29	19, 27, 28	sylanbrc 592	. . . . . . . . 9 ⊢ (𝜑 → (𝐹 · 𝑋) ∈ (𝑉 ∖ { 0 }))
30	1, 2, 3, 4, 5, 6, 7, 8, 9, 29	hdmapnzcl 42430	. . . . . . . 8 ⊢ (𝜑 → (𝑆‘(𝐹 · 𝑋)) ∈ ((Base‘𝐶) ∖ {(0_g‘𝐶)}))
31		eldifsni 4747	. . . . . . . 8 ⊢ ((𝑆‘(𝐹 · 𝑋)) ∈ ((Base‘𝐶) ∖ {(0_g‘𝐶)}) → (𝑆‘(𝐹 · 𝑋)) ≠ (0_g‘𝐶))
32	30, 31	syl 17	. . . . . . 7 ⊢ (𝜑 → (𝑆‘(𝐹 · 𝑋)) ≠ (0_g‘𝐶))
33	32	adantr 484	. . . . . 6 ⊢ ((𝜑 ∧ 𝑔 ∈ {𝑄}) → (𝑆‘(𝐹 · 𝑋)) ≠ (0_g‘𝐶))
34		elsni 4596	. . . . . . . 8 ⊢ (𝑔 ∈ {𝑄} → 𝑔 = 𝑄)
35	34	oveq1d 7406	. . . . . . 7 ⊢ (𝑔 ∈ {𝑄} → (𝑔 ∙ (𝑆‘𝑋)) = (𝑄 ∙ (𝑆‘𝑋)))
36	1, 5, 9	lcdlmod 42177	. . . . . . . 8 ⊢ (𝜑 → 𝐶 ∈ LMod)
37	1, 2, 3, 5, 7, 8, 9, 14	hdmapcl 42415	. . . . . . . 8 ⊢ (𝜑 → (𝑆‘𝑋) ∈ (Base‘𝐶))
38		hdmap14lem2.p	. . . . . . . . 9 ⊢ 𝑃 = (Scalar‘𝐶)
39		hdmap14lem2.e	. . . . . . . . 9 ⊢ ∙ = ( ·_𝑠 ‘𝐶)
40		hdmap14lem2.q	. . . . . . . . 9 ⊢ 𝑄 = (0_g‘𝑃)
41	7, 38, 39, 40, 6	lmod0vs 20950	. . . . . . . 8 ⊢ ((𝐶 ∈ LMod ∧ (𝑆‘𝑋) ∈ (Base‘𝐶)) → (𝑄 ∙ (𝑆‘𝑋)) = (0_g‘𝐶))
42	36, 37, 41	syl2anc 593	. . . . . . 7 ⊢ (𝜑 → (𝑄 ∙ (𝑆‘𝑋)) = (0_g‘𝐶))
43	35, 42	sylan9eqr 2818	. . . . . 6 ⊢ ((𝜑 ∧ 𝑔 ∈ {𝑄}) → (𝑔 ∙ (𝑆‘𝑋)) = (0_g‘𝐶))
44	33, 43	neeqtrrd 3030	. . . . 5 ⊢ ((𝜑 ∧ 𝑔 ∈ {𝑄}) → (𝑆‘(𝐹 · 𝑋)) ≠ (𝑔 ∙ (𝑆‘𝑋)))
45	44	neneqd 2961	. . . 4 ⊢ ((𝜑 ∧ 𝑔 ∈ {𝑄}) → ¬ (𝑆‘(𝐹 · 𝑋)) = (𝑔 ∙ (𝑆‘𝑋)))
46	45	nrexdv 3156	. . 3 ⊢ (𝜑 → ¬ ∃𝑔 ∈ {𝑄} (𝑆‘(𝐹 · 𝑋)) = (𝑔 ∙ (𝑆‘𝑋)))
47		reuun2 4275	. . 3 ⊢ (¬ ∃𝑔 ∈ {𝑄} (𝑆‘(𝐹 · 𝑋)) = (𝑔 ∙ (𝑆‘𝑋)) → (∃!𝑔 ∈ ((𝐴 ∖ {𝑄}) ∪ {𝑄})(𝑆‘(𝐹 · 𝑋)) = (𝑔 ∙ (𝑆‘𝑋)) ↔ ∃!𝑔 ∈ (𝐴 ∖ {𝑄})(𝑆‘(𝐹 · 𝑋)) = (𝑔 ∙ (𝑆‘𝑋))))
48	46, 47	syl 17	. 2 ⊢ (𝜑 → (∃!𝑔 ∈ ((𝐴 ∖ {𝑄}) ∪ {𝑄})(𝑆‘(𝐹 · 𝑋)) = (𝑔 ∙ (𝑆‘𝑋)) ↔ ∃!𝑔 ∈ (𝐴 ∖ {𝑄})(𝑆‘(𝐹 · 𝑋)) = (𝑔 ∙ (𝑆‘𝑋))))
49		hdmap14lem2.a	. . . 4 ⊢ 𝐴 = (Base‘𝑃)
50	38, 49, 40	lmod0cl 20943	. . 3 ⊢ (𝐶 ∈ LMod → 𝑄 ∈ 𝐴)
51		difsnid 4765	. . 3 ⊢ (𝑄 ∈ 𝐴 → ((𝐴 ∖ {𝑄}) ∪ {𝑄}) = 𝐴)
52		reueq1 3398	. . 3 ⊢ (((𝐴 ∖ {𝑄}) ∪ {𝑄}) = 𝐴 → (∃!𝑔 ∈ ((𝐴 ∖ {𝑄}) ∪ {𝑄})(𝑆‘(𝐹 · 𝑋)) = (𝑔 ∙ (𝑆‘𝑋)) ↔ ∃!𝑔 ∈ 𝐴 (𝑆‘(𝐹 · 𝑋)) = (𝑔 ∙ (𝑆‘𝑋))))
53	36, 50, 51, 52	4syl 19	. 2 ⊢ (𝜑 → (∃!𝑔 ∈ ((𝐴 ∖ {𝑄}) ∪ {𝑄})(𝑆‘(𝐹 · 𝑋)) = (𝑔 ∙ (𝑆‘𝑋)) ↔ ∃!𝑔 ∈ 𝐴 (𝑆‘(𝐹 · 𝑋)) = (𝑔 ∙ (𝑆‘𝑋))))
54	48, 53	bitr3d 283	1 ⊢ (𝜑 → (∃!𝑔 ∈ (𝐴 ∖ {𝑄})(𝑆‘(𝐹 · 𝑋)) = (𝑔 ∙ (𝑆‘𝑋)) ↔ ∃!𝑔 ∈ 𝐴 (𝑆‘(𝐹 · 𝑋)) = (𝑔 ∙ (𝑆‘𝑋))))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 208 ∧ wa 399 = wceq 1559 ∈ wcel 2141 ≠ wne 2956 ∃wrex 3085 ∃!wreu 3364 ∖ cdif 3899 ∪ cun 3900 {csn 4579 ‘cfv 6516 (class class class)co 7391 Basecbs 17236 Scalarcsca 17280 ·_𝑠 cvsca 17281 0_gc0g 17459 LModclmod 20915 LSpanclspn 21026 HLchlt 39935 LHypclh 40569 DVecHcdvh 41663 LCDualclcd 42171 HDMapchdma 42377

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-rep 5224 ax-sep 5243 ax-nul 5253 ax-pow 5319 ax-pr 5387 ax-un 7713 ax-cnex 11123 ax-resscn 11124 ax-1cn 11125 ax-icn 11126 ax-addcl 11127 ax-addrcl 11128 ax-mulcl 11129 ax-mulrcl 11130 ax-mulcom 11131 ax-addass 11132 ax-mulass 11133 ax-distr 11134 ax-i2m1 11135 ax-1ne0 11136 ax-1rid 11137 ax-rnegex 11138 ax-rrecex 11139 ax-cnre 11140 ax-pre-lttri 11141 ax-pre-lttrn 11142 ax-pre-ltadd 11143 ax-pre-mulgt0 11144 ax-riotaBAD 39538

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1098 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-nf 1803 df-sb 2090 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3061 df-ral 3076 df-rex 3086 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3455 df-sbc 3743 df-csb 3851 df-dif 3905 df-un 3907 df-in 3909 df-ss 3919 df-pss 3922 df-nul 4284 df-if 4478 df-pw 4554 df-sn 4580 df-pr 4582 df-tp 4584 df-op 4586 df-ot 4588 df-uni 4863 df-int 4903 df-iun 4948 df-iin 4949 df-br 5098 df-opab 5160 df-mpt 5179 df-tr 5205 df-id 5538 df-eprel 5543 df-po 5551 df-so 5552 df-fr 5596 df-we 5598 df-xp 5649 df-rel 5650 df-cnv 5651 df-co 5652 df-dm 5653 df-rn 5654 df-res 5655 df-ima 5656 df-pred 6283 df-ord 6344 df-on 6345 df-lim 6346 df-suc 6347 df-iota 6472 df-fun 6518 df-fn 6519 df-f 6520 df-f1 6521 df-fo 6522 df-f1o 6523 df-fv 6524 df-riota 7348 df-ov 7394 df-oprab 7395 df-mpo 7396 df-of 7655 df-om 7842 df-1st 7965 df-2nd 7966 df-tpos 8200 df-undef 8247 df-frecs 8256 df-wrecs 8287 df-recs 8336 df-rdg 8375 df-1o 8431 df-2o 8432 df-er 8672 df-map 8804 df-en 8922 df-dom 8923 df-sdom 8924 df-fin 8925 df-pnf 11212 df-mnf 11213 df-xr 11214 df-ltxr 11215 df-le 11216 df-sub 11410 df-neg 11411 df-nn 12205 df-2 12274 df-3 12275 df-4 12276 df-5 12277 df-6 12278 df-n0 12476 df-z 12563 df-uz 12834 df-fz 13507 df-struct 17174 df-sets 17191 df-slot 17209 df-ndx 17221 df-base 17237 df-ress 17258 df-plusg 17290 df-mulr 17291 df-sca 17293 df-vsca 17294 df-0g 17461 df-mre 17605 df-mrc 17606 df-acs 17608 df-proset 18317 df-poset 18336 df-plt 18351 df-lub 18367 df-glb 18368 df-join 18369 df-meet 18370 df-p0 18446 df-p1 18447 df-lat 18455 df-clat 18522 df-mgm 18665 df-sgrp 18744 df-mnd 18760 df-submnd 18809 df-grp 18969 df-minusg 18970 df-sbg 18971 df-subg 19156 df-cntz 19348 df-oppg 19377 df-lsm 19667 df-cmn 19813 df-abl 19814 df-mgp 20178 df-rng 20190 df-ur 20219 df-ring 20272 df-oppr 20373 df-dvdsr 20393 df-unit 20394 df-invr 20424 df-dvr 20437 df-nzr 20550 df-rlreg 20731 df-domn 20732 df-drng 20768 df-lmod 20917 df-lss 20987 df-lsp 21027 df-lvec 21158 df-lsatoms 39561 df-lshyp 39562 df-lcv 39604 df-lfl 39643 df-lkr 39671 df-ldual 39709 df-oposet 39761 df-ol 39763 df-oml 39764 df-covers 39851 df-ats 39852 df-atl 39883 df-cvlat 39907 df-hlat 39936 df-llines 40083 df-lplanes 40084 df-lvols 40085 df-lines 40086 df-psubsp 40088 df-pmap 40089 df-padd 40381 df-lhyp 40573 df-laut 40574 df-ldil 40689 df-ltrn 40690 df-trl 40744 df-tgrp 41328 df-tendo 41340 df-edring 41342 df-dveca 41588 df-disoa 41614 df-dvech 41664 df-dib 41724 df-dic 41758 df-dih 41814 df-doch 41933 df-djh 41980 df-lcdual 42172 df-mapd 42210 df-hvmap 42342 df-hdmap1 42378 df-hdmap 42379

This theorem is referenced by: hdmap14lem4 42457

W3C validator