hdmapip0 - Mathbox for Norm Megill

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

Theorem hdmapip0 40134

Description: Zero property that will be used for inner product. (Contributed by NM, 9-Jun-2015.)

**Hypotheses**
Ref	Expression
hdmapip0.h	⊢ 𝐻 = (LHyp‘𝐾)
hdmapip0.u	⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
hdmapip0.v	⊢ 𝑉 = (Base‘𝑈)
hdmapip0.o	⊢ 0 = (0_g‘𝑈)
hdmapip0.r	⊢ 𝑅 = (Scalar‘𝑈)
hdmapip0.z	⊢ 𝑍 = (0_g‘𝑅)
hdmapip0.s	⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)
hdmapip0.k	⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
hdmapip0.x	⊢ (𝜑 → 𝑋 ∈ 𝑉)

**Assertion**
Ref	Expression
hdmapip0	⊢ (𝜑 → (((𝑆‘𝑋)‘𝑋) = 𝑍 ↔ 𝑋 = 0 ))

**Proof of Theorem hdmapip0**
Step	Hyp	Ref	Expression
1		hdmapip0.h	. . . . . . . 8 ⊢ 𝐻 = (LHyp‘𝐾)
2		eqid 2737	. . . . . . . 8 ⊢ ((ocH‘𝐾)‘𝑊) = ((ocH‘𝐾)‘𝑊)
3		hdmapip0.u	. . . . . . . 8 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
4		hdmapip0.v	. . . . . . . 8 ⊢ 𝑉 = (Base‘𝑈)
5		hdmapip0.o	. . . . . . . 8 ⊢ 0 = (0_g‘𝑈)
6		hdmapip0.k	. . . . . . . . 9 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
7	6	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 ≠ 0 ) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
8		hdmapip0.x	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
9	8	anim1i 615	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑋 ≠ 0 ) → (𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ))
10		eldifsn 4732	. . . . . . . . 9 ⊢ (𝑋 ∈ (𝑉 ∖ { 0 }) ↔ (𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ))
11	9, 10	sylibr 233	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑋 ≠ 0 ) → 𝑋 ∈ (𝑉 ∖ { 0 }))
12	1, 2, 3, 4, 5, 7, 11	dochnel 39612	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 ≠ 0 ) → ¬ 𝑋 ∈ (((ocH‘𝐾)‘𝑊)‘{𝑋}))
13		hdmapip0.r	. . . . . . . . . . . 12 ⊢ 𝑅 = (Scalar‘𝑈)
14		hdmapip0.z	. . . . . . . . . . . 12 ⊢ 𝑍 = (0_g‘𝑅)
15		eqid 2737	. . . . . . . . . . . 12 ⊢ (LFnl‘𝑈) = (LFnl‘𝑈)
16		eqid 2737	. . . . . . . . . . . 12 ⊢ (LKer‘𝑈) = (LKer‘𝑈)
17	1, 3, 6	dvhlmod 39329	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑈 ∈ LMod)
18		eqid 2737	. . . . . . . . . . . . 13 ⊢ ((LCDual‘𝐾)‘𝑊) = ((LCDual‘𝐾)‘𝑊)
19		eqid 2737	. . . . . . . . . . . . 13 ⊢ (Base‘((LCDual‘𝐾)‘𝑊)) = (Base‘((LCDual‘𝐾)‘𝑊))
20		hdmapip0.s	. . . . . . . . . . . . . 14 ⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊)
21	1, 3, 4, 18, 19, 20, 6, 8	hdmapcl 40049	. . . . . . . . . . . . 13 ⊢ (𝜑 → (𝑆‘𝑋) ∈ (Base‘((LCDual‘𝐾)‘𝑊)))
22	1, 18, 19, 3, 15, 6, 21	lcdvbaselfl 39814	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝑆‘𝑋) ∈ (LFnl‘𝑈))
23	4, 13, 14, 15, 16, 17, 22, 8	ellkr2 37309	. . . . . . . . . . 11 ⊢ (𝜑 → (𝑋 ∈ ((LKer‘𝑈)‘(𝑆‘𝑋)) ↔ ((𝑆‘𝑋)‘𝑋) = 𝑍))
24	23	biimpar 478	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑆‘𝑋)‘𝑋) = 𝑍) → 𝑋 ∈ ((LKer‘𝑈)‘(𝑆‘𝑋)))
25	1, 2, 3, 4, 15, 16, 20, 6, 8	hdmaplkr 40132	. . . . . . . . . . 11 ⊢ (𝜑 → ((LKer‘𝑈)‘(𝑆‘𝑋)) = (((ocH‘𝐾)‘𝑊)‘{𝑋}))
26	25	adantr 481	. . . . . . . . . 10 ⊢ ((𝜑 ∧ ((𝑆‘𝑋)‘𝑋) = 𝑍) → ((LKer‘𝑈)‘(𝑆‘𝑋)) = (((ocH‘𝐾)‘𝑊)‘{𝑋}))
27	24, 26	eleqtrd 2840	. . . . . . . . 9 ⊢ ((𝜑 ∧ ((𝑆‘𝑋)‘𝑋) = 𝑍) → 𝑋 ∈ (((ocH‘𝐾)‘𝑊)‘{𝑋}))
28	27	ex 413	. . . . . . . 8 ⊢ (𝜑 → (((𝑆‘𝑋)‘𝑋) = 𝑍 → 𝑋 ∈ (((ocH‘𝐾)‘𝑊)‘{𝑋})))
29	28	adantr 481	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑋 ≠ 0 ) → (((𝑆‘𝑋)‘𝑋) = 𝑍 → 𝑋 ∈ (((ocH‘𝐾)‘𝑊)‘{𝑋})))
30	12, 29	mtod 197	. . . . . 6 ⊢ ((𝜑 ∧ 𝑋 ≠ 0 ) → ¬ ((𝑆‘𝑋)‘𝑋) = 𝑍)
31	30	neqned 2948	. . . . 5 ⊢ ((𝜑 ∧ 𝑋 ≠ 0 ) → ((𝑆‘𝑋)‘𝑋) ≠ 𝑍)
32	31	ex 413	. . . 4 ⊢ (𝜑 → (𝑋 ≠ 0 → ((𝑆‘𝑋)‘𝑋) ≠ 𝑍))
33	32	necon4d 2965	. . 3 ⊢ (𝜑 → (((𝑆‘𝑋)‘𝑋) = 𝑍 → 𝑋 = 0 ))
34	33	imp 407	. 2 ⊢ ((𝜑 ∧ ((𝑆‘𝑋)‘𝑋) = 𝑍) → 𝑋 = 0 )
35		fveq2 6811	. . 3 ⊢ (𝑋 = 0 → ((𝑆‘𝑋)‘𝑋) = ((𝑆‘𝑋)‘ 0 ))
36	13, 14, 5, 15	lfl0 37283	. . . 4 ⊢ ((𝑈 ∈ LMod ∧ (𝑆‘𝑋) ∈ (LFnl‘𝑈)) → ((𝑆‘𝑋)‘ 0 ) = 𝑍)
37	17, 22, 36	syl2anc 584	. . 3 ⊢ (𝜑 → ((𝑆‘𝑋)‘ 0 ) = 𝑍)
38	35, 37	sylan9eqr 2799	. 2 ⊢ ((𝜑 ∧ 𝑋 = 0 ) → ((𝑆‘𝑋)‘𝑋) = 𝑍)
39	34, 38	impbida 798	1 ⊢ (𝜑 → (((𝑆‘𝑋)‘𝑋) = 𝑍 ↔ 𝑋 = 0 ))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 = wceq 1540 ∈ wcel 2105 ≠ wne 2941 ∖ cdif 3894 {csn 4571 ‘cfv 6465 Basecbs 16982 Scalarcsca 17035 0_gc0g 17220 LModclmod 20195 LFnlclfn 37275 LKerclk 37303 HLchlt 37568 LHypclh 38203 DVecHcdvh 39297 ocHcoch 39566 LCDualclcd 39805 HDMapchdma 40011

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1912 ax-6 1970 ax-7 2010 ax-8 2107 ax-9 2115 ax-10 2136 ax-11 2153 ax-12 2170 ax-ext 2708 ax-rep 5224 ax-sep 5238 ax-nul 5245 ax-pow 5303 ax-pr 5367 ax-un 7628 ax-cnex 11000 ax-resscn 11001 ax-1cn 11002 ax-icn 11003 ax-addcl 11004 ax-addrcl 11005 ax-mulcl 11006 ax-mulrcl 11007 ax-mulcom 11008 ax-addass 11009 ax-mulass 11010 ax-distr 11011 ax-i2m1 11012 ax-1ne0 11013 ax-1rid 11014 ax-rnegex 11015 ax-rrecex 11016 ax-cnre 11017 ax-pre-lttri 11018 ax-pre-lttrn 11019 ax-pre-ltadd 11020 ax-pre-mulgt0 11021 ax-riotaBAD 37171

This theorem depends on definitions: df-bi 206 df-an 397 df-or 845 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1781 df-nf 1785 df-sb 2067 df-mo 2539 df-eu 2568 df-clab 2715 df-cleq 2729 df-clel 2815 df-nfc 2887 df-ne 2942 df-nel 3048 df-ral 3063 df-rex 3072 df-rmo 3350 df-reu 3351 df-rab 3405 df-v 3443 df-sbc 3727 df-csb 3843 df-dif 3900 df-un 3902 df-in 3904 df-ss 3914 df-pss 3916 df-nul 4268 df-if 4472 df-pw 4547 df-sn 4572 df-pr 4574 df-tp 4576 df-op 4578 df-ot 4580 df-uni 4851 df-int 4893 df-iun 4939 df-iin 4940 df-br 5088 df-opab 5150 df-mpt 5171 df-tr 5205 df-id 5507 df-eprel 5513 df-po 5521 df-so 5522 df-fr 5562 df-we 5564 df-xp 5613 df-rel 5614 df-cnv 5615 df-co 5616 df-dm 5617 df-rn 5618 df-res 5619 df-ima 5620 df-pred 6224 df-ord 6291 df-on 6292 df-lim 6293 df-suc 6294 df-iota 6417 df-fun 6467 df-fn 6468 df-f 6469 df-f1 6470 df-fo 6471 df-f1o 6472 df-fv 6473 df-riota 7272 df-ov 7318 df-oprab 7319 df-mpo 7320 df-of 7573 df-om 7758 df-1st 7876 df-2nd 7877 df-tpos 8089 df-undef 8136 df-frecs 8144 df-wrecs 8175 df-recs 8249 df-rdg 8288 df-1o 8344 df-er 8546 df-map 8665 df-en 8782 df-dom 8783 df-sdom 8784 df-fin 8785 df-pnf 11084 df-mnf 11085 df-xr 11086 df-ltxr 11087 df-le 11088 df-sub 11280 df-neg 11281 df-nn 12047 df-2 12109 df-3 12110 df-4 12111 df-5 12112 df-6 12113 df-n0 12307 df-z 12393 df-uz 12656 df-fz 13313 df-struct 16918 df-sets 16935 df-slot 16953 df-ndx 16965 df-base 16983 df-ress 17012 df-plusg 17045 df-mulr 17046 df-sca 17048 df-vsca 17049 df-0g 17222 df-mre 17365 df-mrc 17366 df-acs 17368 df-proset 18083 df-poset 18101 df-plt 18118 df-lub 18134 df-glb 18135 df-join 18136 df-meet 18137 df-p0 18213 df-p1 18214 df-lat 18220 df-clat 18287 df-mgm 18396 df-sgrp 18445 df-mnd 18456 df-submnd 18501 df-grp 18649 df-minusg 18650 df-sbg 18651 df-subg 18821 df-cntz 18992 df-oppg 19019 df-lsm 19310 df-cmn 19456 df-abl 19457 df-mgp 19789 df-ur 19806 df-ring 19853 df-oppr 19930 df-dvdsr 19951 df-unit 19952 df-invr 19982 df-dvr 19993 df-drng 20065 df-lmod 20197 df-lss 20266 df-lsp 20306 df-lvec 20437 df-lsatoms 37194 df-lshyp 37195 df-lcv 37237 df-lfl 37276 df-lkr 37304 df-ldual 37342 df-oposet 37394 df-ol 37396 df-oml 37397 df-covers 37484 df-ats 37485 df-atl 37516 df-cvlat 37540 df-hlat 37569 df-llines 37717 df-lplanes 37718 df-lvols 37719 df-lines 37720 df-psubsp 37722 df-pmap 37723 df-padd 38015 df-lhyp 38207 df-laut 38208 df-ldil 38323 df-ltrn 38324 df-trl 38378 df-tgrp 38962 df-tendo 38974 df-edring 38976 df-dveca 39222 df-disoa 39248 df-dvech 39298 df-dib 39358 df-dic 39392 df-dih 39448 df-doch 39567 df-djh 39614 df-lcdual 39806 df-mapd 39844 df-hvmap 39976 df-hdmap1 40012 df-hdmap 40013

This theorem is referenced by: hdmapip1 40135 hgmapvvlem3 40144 hlhilphllem 40182

W3C validator