mapdh8c - Mathbox for Norm Megill

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

Theorem mapdh8c 35887

Description: Part of Part (8) in [Baer] p. 48. (Contributed by NM, 6-May-2015.)

**Hypotheses**
Ref	Expression
mapdh8a.h	⊢ 𝐻 = (LHyp‘𝐾)
mapdh8a.u	⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
mapdh8a.v	⊢ 𝑉 = (Base‘𝑈)
mapdh8a.s	⊢ − = (-_g‘𝑈)
mapdh8a.o	⊢ 0 = (0_g‘𝑈)
mapdh8a.n	⊢ 𝑁 = (LSpan‘𝑈)
mapdh8a.c	⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)
mapdh8a.d	⊢ 𝐷 = (Base‘𝐶)
mapdh8a.r	⊢ 𝑅 = (-_g‘𝐶)
mapdh8a.q	⊢ 𝑄 = (0_g‘𝐶)
mapdh8a.j	⊢ 𝐽 = (LSpan‘𝐶)
mapdh8a.m	⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)
mapdh8a.i	⊢ 𝐼 = (𝑥 ∈ V ↦ if((2^nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2^nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1^st ‘(1^st ‘𝑥)) − (2^nd ‘𝑥))})) = (𝐽‘{((2^nd ‘(1^st ‘𝑥))𝑅ℎ)})))))
mapdh8a.k	⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
mapdh8c.f	⊢ (𝜑 → 𝐹 ∈ 𝐷)
mapdh8c.mn	⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹}))
mapdh8c.a	⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑤⟩) = 𝐸)
mapdh8c.x	⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))
mapdh8c.y	⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))
mapdh8c.xt	⊢ (𝜑 → 𝑇 ∈ (𝑉 ∖ { 0 }))
mapdh8c.yz	⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑇}))
mapdh8c.w	⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 }))
mapdh8c.wt	⊢ (𝜑 → (𝑁‘{𝑤}) ≠ (𝑁‘{𝑇}))
mapdh8c.ut	⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑇}))
mapdh8c.vw	⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑤}))
mapdh8c.e	⊢ (𝜑 → 𝑋 ∈ (𝑁‘{𝑌, 𝑇}))
mapdh8c.xn	⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑤}))

**Assertion**
Ref	Expression
mapdh8c	⊢ (𝜑 → (𝐼‘⟨𝑤, 𝐸, 𝑇⟩) = (𝐼‘⟨𝑋, 𝐹, 𝑇⟩))

Distinct variable groups: 𝑥,ℎ, − 0 ,ℎ,𝑥 𝐶,ℎ 𝐷,ℎ,𝑥 ℎ,𝐹,𝑥 ℎ,𝐼 ℎ,𝐽,𝑥 ℎ,𝑀,𝑥 ℎ,𝑁,𝑥 𝜑,ℎ 𝑅,ℎ,𝑥 𝑥,𝑄 𝑇,ℎ,𝑥 𝑈,ℎ ℎ,𝑋,𝑥 ℎ,𝑌,𝑥 ℎ,𝐸,𝑥 𝑤,ℎ,𝑥 Allowed substitution hints: 𝜑(𝑥,𝑤) 𝐶(𝑥,𝑤) 𝐷(𝑤) 𝑄(𝑤,ℎ) 𝑅(𝑤) 𝑇(𝑤) 𝑈(𝑥,𝑤) 𝐸(𝑤) 𝐹(𝑤) 𝐻(𝑥,𝑤,ℎ) 𝐼(𝑥,𝑤) 𝐽(𝑤) 𝐾(𝑥,𝑤,ℎ) 𝑀(𝑤) − (𝑤) 𝑁(𝑤) 𝑉(𝑥,𝑤,ℎ) 𝑊(𝑥,𝑤,ℎ) 𝑋(𝑤) 𝑌(𝑤) 0 (𝑤)

**Proof of Theorem mapdh8c**
Step	Hyp	Ref	Expression
1		mapdh8a.h	. 2 ⊢ 𝐻 = (LHyp‘𝐾)
2		mapdh8a.u	. 2 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
3		mapdh8a.v	. 2 ⊢ 𝑉 = (Base‘𝑈)
4		mapdh8a.s	. 2 ⊢ − = (-_g‘𝑈)
5		mapdh8a.o	. 2 ⊢ 0 = (0_g‘𝑈)
6		mapdh8a.n	. 2 ⊢ 𝑁 = (LSpan‘𝑈)
7		mapdh8a.c	. 2 ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)
8		mapdh8a.d	. 2 ⊢ 𝐷 = (Base‘𝐶)
9		mapdh8a.r	. 2 ⊢ 𝑅 = (-_g‘𝐶)
10		mapdh8a.q	. 2 ⊢ 𝑄 = (0_g‘𝐶)
11		mapdh8a.j	. 2 ⊢ 𝐽 = (LSpan‘𝐶)
12		mapdh8a.m	. 2 ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)
13		mapdh8a.i	. 2 ⊢ 𝐼 = (𝑥 ∈ V ↦ if((2^nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2^nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1^st ‘(1^st ‘𝑥)) − (2^nd ‘𝑥))})) = (𝐽‘{((2^nd ‘(1^st ‘𝑥))𝑅ℎ)})))))
14		mapdh8a.k	. 2 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
15		mapdh8c.f	. 2 ⊢ (𝜑 → 𝐹 ∈ 𝐷)
16		mapdh8c.mn	. 2 ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹}))
17		mapdh8c.a	. 2 ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑤⟩) = 𝐸)
18		mapdh8c.x	. 2 ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))
19		mapdh8c.w	. 2 ⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 }))
20		mapdh8c.wt	. 2 ⊢ (𝜑 → (𝑁‘{𝑤}) ≠ (𝑁‘{𝑇}))
21		mapdh8c.xt	. 2 ⊢ (𝜑 → 𝑇 ∈ (𝑉 ∖ { 0 }))
22	1, 2, 14	dvhlvec 35215	. . . 4 ⊢ (𝜑 → 𝑈 ∈ LVec)
23	18	eldifad 3547	. . . 4 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
24		mapdh8c.y	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))
25	24	eldifad 3547	. . . 4 ⊢ (𝜑 → 𝑌 ∈ 𝑉)
26	19	eldifad 3547	. . . 4 ⊢ (𝜑 → 𝑤 ∈ 𝑉)
27		mapdh8c.xn	. . . 4 ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑤}))
28	3, 6, 22, 23, 25, 26, 27	lspindpi 18895	. . 3 ⊢ (𝜑 → ((𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}) ∧ (𝑁‘{𝑋}) ≠ (𝑁‘{𝑤})))
29	28	simprd 477	. 2 ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑤}))
30	21	eldifad 3547	. . 3 ⊢ (𝜑 → 𝑇 ∈ 𝑉)
31		mapdh8c.ut	. . 3 ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑇}))
32		mapdh8c.e	. . 3 ⊢ (𝜑 → 𝑋 ∈ (𝑁‘{𝑌, 𝑇}))
33	3, 5, 6, 22, 18, 25, 30, 31, 32	lspexch 18892	. 2 ⊢ (𝜑 → 𝑌 ∈ (𝑁‘{𝑋, 𝑇}))
34	22	adantr 479	. . . 4 ⊢ ((𝜑 ∧ 𝑌 ∈ (𝑁‘{𝑋, 𝑤})) → 𝑈 ∈ LVec)
35	24	adantr 479	. . . 4 ⊢ ((𝜑 ∧ 𝑌 ∈ (𝑁‘{𝑋, 𝑤})) → 𝑌 ∈ (𝑉 ∖ { 0 }))
36	23	adantr 479	. . . 4 ⊢ ((𝜑 ∧ 𝑌 ∈ (𝑁‘{𝑋, 𝑤})) → 𝑋 ∈ 𝑉)
37	26	adantr 479	. . . 4 ⊢ ((𝜑 ∧ 𝑌 ∈ (𝑁‘{𝑋, 𝑤})) → 𝑤 ∈ 𝑉)
38		mapdh8c.vw	. . . . 5 ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑤}))
39	38	adantr 479	. . . 4 ⊢ ((𝜑 ∧ 𝑌 ∈ (𝑁‘{𝑋, 𝑤})) → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑤}))
40		simpr 475	. . . 4 ⊢ ((𝜑 ∧ 𝑌 ∈ (𝑁‘{𝑋, 𝑤})) → 𝑌 ∈ (𝑁‘{𝑋, 𝑤}))
41	3, 5, 6, 34, 35, 36, 37, 39, 40	lspexch 18892	. . 3 ⊢ ((𝜑 ∧ 𝑌 ∈ (𝑁‘{𝑋, 𝑤})) → 𝑋 ∈ (𝑁‘{𝑌, 𝑤}))
42	27, 41	mtand 688	. 2 ⊢ (𝜑 → ¬ 𝑌 ∈ (𝑁‘{𝑋, 𝑤}))
43	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 29, 33, 42	mapdh8b 35886	1 ⊢ (𝜑 → (𝐼‘⟨𝑤, 𝐸, 𝑇⟩) = (𝐼‘⟨𝑋, 𝐹, 𝑇⟩))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 382 = wceq 1474 ∈ wcel 1975 ≠ wne 2775 Vcvv 3168 ∖ cdif 3532 ifcif 4031 {csn 4120 {cpr 4122 ⟨cotp 4128 ↦ cmpt 4633 ‘cfv 5786 ℩crio 6484 (class class class)co 6523 1^st c1st 7030 2^nd c2nd 7031 Basecbs 15637 0_gc0g 15865 -_gcsg 17189 LSpanclspn 18734 LVecclvec 18865 HLchlt 33454 LHypclh 34087 DVecHcdvh 35184 LCDualclcd 35692 mapdcmpd 35730

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1711 ax-4 1726 ax-5 1825 ax-6 1873 ax-7 1920 ax-8 1977 ax-9 1984 ax-10 2004 ax-11 2019 ax-12 2031 ax-13 2228 ax-ext 2585 ax-rep 4689 ax-sep 4699 ax-nul 4708 ax-pow 4760 ax-pr 4824 ax-un 6820 ax-cnex 9844 ax-resscn 9845 ax-1cn 9846 ax-icn 9847 ax-addcl 9848 ax-addrcl 9849 ax-mulcl 9850 ax-mulrcl 9851 ax-mulcom 9852 ax-addass 9853 ax-mulass 9854 ax-distr 9855 ax-i2m1 9856 ax-1ne0 9857 ax-1rid 9858 ax-rnegex 9859 ax-rrecex 9860 ax-cnre 9861 ax-pre-lttri 9862 ax-pre-lttrn 9863 ax-pre-ltadd 9864 ax-pre-mulgt0 9865 ax-riotaBAD 33056

This theorem depends on definitions: df-bi 195 df-or 383 df-an 384 df-3or 1031 df-3an 1032 df-tru 1477 df-fal 1480 df-ex 1695 df-nf 1700 df-sb 1866 df-eu 2457 df-mo 2458 df-clab 2592 df-cleq 2598 df-clel 2601 df-nfc 2735 df-ne 2777 df-nel 2778 df-ral 2896 df-rex 2897 df-reu 2898 df-rmo 2899 df-rab 2900 df-v 3170 df-sbc 3398 df-csb 3495 df-dif 3538 df-un 3540 df-in 3542 df-ss 3549 df-pss 3551 df-nul 3870 df-if 4032 df-pw 4105 df-sn 4121 df-pr 4123 df-tp 4125 df-op 4127 df-ot 4129 df-uni 4363 df-int 4401 df-iun 4447 df-iin 4448 df-br 4574 df-opab 4634 df-mpt 4635 df-tr 4671 df-eprel 4935 df-id 4939 df-po 4945 df-so 4946 df-fr 4983 df-we 4985 df-xp 5030 df-rel 5031 df-cnv 5032 df-co 5033 df-dm 5034 df-rn 5035 df-res 5036 df-ima 5037 df-pred 5579 df-ord 5625 df-on 5626 df-lim 5627 df-suc 5628 df-iota 5750 df-fun 5788 df-fn 5789 df-f 5790 df-f1 5791 df-fo 5792 df-f1o 5793 df-fv 5794 df-riota 6485 df-ov 6526 df-oprab 6527 df-mpt2 6528 df-of 6768 df-om 6931 df-1st 7032 df-2nd 7033 df-tpos 7212 df-undef 7259 df-wrecs 7267 df-recs 7328 df-rdg 7366 df-1o 7420 df-oadd 7424 df-er 7602 df-map 7719 df-en 7815 df-dom 7816 df-sdom 7817 df-fin 7818 df-pnf 9928 df-mnf 9929 df-xr 9930 df-ltxr 9931 df-le 9932 df-sub 10115 df-neg 10116 df-nn 10864 df-2 10922 df-3 10923 df-4 10924 df-5 10925 df-6 10926 df-n0 11136 df-z 11207 df-uz 11516 df-fz 12149 df-struct 15639 df-ndx 15640 df-slot 15641 df-base 15642 df-sets 15643 df-ress 15644 df-plusg 15723 df-mulr 15724 df-sca 15726 df-vsca 15727 df-0g 15867 df-mre 16011 df-mrc 16012 df-acs 16014 df-preset 16693 df-poset 16711 df-plt 16723 df-lub 16739 df-glb 16740 df-join 16741 df-meet 16742 df-p0 16804 df-p1 16805 df-lat 16811 df-clat 16873 df-mgm 17007 df-sgrp 17049 df-mnd 17060 df-submnd 17101 df-grp 17190 df-minusg 17191 df-sbg 17192 df-subg 17356 df-cntz 17515 df-oppg 17541 df-lsm 17816 df-cmn 17960 df-abl 17961 df-mgp 18255 df-ur 18267 df-ring 18314 df-oppr 18388 df-dvdsr 18406 df-unit 18407 df-invr 18437 df-dvr 18448 df-drng 18514 df-lmod 18630 df-lss 18696 df-lsp 18735 df-lvec 18866 df-lsatoms 33080 df-lshyp 33081 df-lcv 33123 df-lfl 33162 df-lkr 33190 df-ldual 33228 df-oposet 33280 df-ol 33282 df-oml 33283 df-covers 33370 df-ats 33371 df-atl 33402 df-cvlat 33426 df-hlat 33455 df-llines 33601 df-lplanes 33602 df-lvols 33603 df-lines 33604 df-psubsp 33606 df-pmap 33607 df-padd 33899 df-lhyp 34091 df-laut 34092 df-ldil 34207 df-ltrn 34208 df-trl 34263 df-tgrp 34848 df-tendo 34860 df-edring 34862 df-dveca 35108 df-disoa 35135 df-dvech 35185 df-dib 35245 df-dic 35279 df-dih 35335 df-doch 35454 df-djh 35501 df-lcdual 35693 df-mapd 35731

This theorem is referenced by: mapdh8d0N 35888 mapdh8d 35889

W3C validator