mapdh8b - Mathbox for Norm Megill

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

Theorem mapdh8b 42614

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 ∧ 𝑊 ∈ 𝐻))
mapdh8b.f	⊢ (𝜑 → 𝐺 ∈ 𝐷)
mapdh8b.mn	⊢ (𝜑 → (𝑀‘(𝑁‘{𝑌})) = (𝐽‘{𝐺}))
mapdh8b.a	⊢ (𝜑 → (𝐼‘⟨𝑌, 𝐺, 𝑤⟩) = 𝐸)
mapdh8b.x	⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))
mapdh8b.y	⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 }))
mapdh8b.yz	⊢ (𝜑 → (𝑁‘{𝑤}) ≠ (𝑁‘{𝑇}))
mapdh8b.xt	⊢ (𝜑 → 𝑇 ∈ (𝑉 ∖ { 0 }))
mapdh8b.vw	⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑤}))
mapdh8b.e	⊢ (𝜑 → 𝑋 ∈ (𝑁‘{𝑌, 𝑇}))
mapdh8b.xn	⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑤}))

**Assertion**
Ref	Expression
mapdh8b	⊢ (𝜑 → (𝐼‘⟨𝑤, 𝐸, 𝑇⟩) = (𝐼‘⟨𝑌, 𝐺, 𝑇⟩))

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

**Proof of Theorem mapdh8b**
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		mapdh8b.f	. 2 ⊢ (𝜑 → 𝐺 ∈ 𝐷)
16		mapdh8b.mn	. 2 ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑌})) = (𝐽‘{𝐺}))
17		mapdh8b.a	. 2 ⊢ (𝜑 → (𝐼‘⟨𝑌, 𝐺, 𝑤⟩) = 𝐸)
18		mapdh8b.x	. 2 ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))
19		mapdh8b.y	. 2 ⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 }))
20		mapdh8b.yz	. 2 ⊢ (𝜑 → (𝑁‘{𝑤}) ≠ (𝑁‘{𝑇}))
21		mapdh8b.xt	. 2 ⊢ (𝜑 → 𝑇 ∈ (𝑉 ∖ { 0 }))
22	1, 2, 14	dvhlvec 41943	. . . 4 ⊢ (𝜑 → 𝑈 ∈ LVec)
23	18	eldifad 3918	. . . 4 ⊢ (𝜑 → 𝑌 ∈ 𝑉)
24	19	eldifad 3918	. . . 4 ⊢ (𝜑 → 𝑤 ∈ 𝑉)
25	21	eldifad 3918	. . . 4 ⊢ (𝜑 → 𝑇 ∈ 𝑉)
26		mapdh8b.e	. . . 4 ⊢ (𝜑 → 𝑋 ∈ (𝑁‘{𝑌, 𝑇}))
27		mapdh8b.xn	. . . 4 ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑤}))
28	3, 6, 22, 23, 24, 25, 26, 27	lspindp5 42604	. . 3 ⊢ (𝜑 → ¬ 𝑇 ∈ (𝑁‘{𝑌, 𝑤}))
29		prcom 4700	. . . . . 6 ⊢ {𝑤, 𝑇} = {𝑇, 𝑤}
30	29	fveq2i 6888	. . . . 5 ⊢ (𝑁‘{𝑤, 𝑇}) = (𝑁‘{𝑇, 𝑤})
31	30	eleq2i 2857	. . . 4 ⊢ (𝑌 ∈ (𝑁‘{𝑤, 𝑇}) ↔ 𝑌 ∈ (𝑁‘{𝑇, 𝑤}))
32	22	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑌 ∈ (𝑁‘{𝑇, 𝑤})) → 𝑈 ∈ LVec)
33	18	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑌 ∈ (𝑁‘{𝑇, 𝑤})) → 𝑌 ∈ (𝑉 ∖ { 0 }))
34	25	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑌 ∈ (𝑁‘{𝑇, 𝑤})) → 𝑇 ∈ 𝑉)
35	24	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑌 ∈ (𝑁‘{𝑇, 𝑤})) → 𝑤 ∈ 𝑉)
36		mapdh8b.vw	. . . . . . 7 ⊢ (𝜑 → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑤}))
37	36	adantr 486	. . . . . 6 ⊢ ((𝜑 ∧ 𝑌 ∈ (𝑁‘{𝑇, 𝑤})) → (𝑁‘{𝑌}) ≠ (𝑁‘{𝑤}))
38		simpr 490	. . . . . 6 ⊢ ((𝜑 ∧ 𝑌 ∈ (𝑁‘{𝑇, 𝑤})) → 𝑌 ∈ (𝑁‘{𝑇, 𝑤}))
39	3, 5, 6, 32, 33, 34, 35, 37, 38	lspexch 21305	. . . . 5 ⊢ ((𝜑 ∧ 𝑌 ∈ (𝑁‘{𝑇, 𝑤})) → 𝑇 ∈ (𝑁‘{𝑌, 𝑤}))
40	39	ex 418	. . . 4 ⊢ (𝜑 → (𝑌 ∈ (𝑁‘{𝑇, 𝑤}) → 𝑇 ∈ (𝑁‘{𝑌, 𝑤})))
41	31, 40	biimtrid 245	. . 3 ⊢ (𝜑 → (𝑌 ∈ (𝑁‘{𝑤, 𝑇}) → 𝑇 ∈ (𝑁‘{𝑌, 𝑤})))
42	28, 41	mtod 201	. 2 ⊢ (𝜑 → ¬ 𝑌 ∈ (𝑁‘{𝑤, 𝑇}))
43	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 42	mapdh8a 42609	1 ⊢ (𝜑 → (𝐼‘⟨𝑤, 𝐸, 𝑇⟩) = (𝐼‘⟨𝑌, 𝐺, 𝑇⟩))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ¬ wn 3 → wi 4 ∧ wa 401 = wceq 1570 ∈ wcel 2146 ≠ wne 2960 Vcvv 3457 ∖ cdif 3903 ifcif 4489 {csn 4591 {cpr 4593 ⟨cotp 4599 ↦ cmpt 5194 ‘cfv 6540 ℩crio 7375 (class class class)co 7419 1^st c1st 7990 2^nd c2nd 7991 Basecbs 17293 0_gc0g 17516 -_gcsg 19048 LSpanclspn 21144 LVecclvec 21275 HLchlt 40184 LHypclh 40818 DVecHcdvh 41912 LCDualclcd 42420 mapdcmpd 42458

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 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7742 ax-cnex 11173 ax-resscn 11174 ax-1cn 11175 ax-icn 11176 ax-addcl 11177 ax-addrcl 11178 ax-mulcl 11179 ax-mulrcl 11180 ax-mulcom 11181 ax-addass 11182 ax-mulass 11183 ax-distr 11184 ax-i2m1 11185 ax-1ne0 11186 ax-1rid 11187 ax-rnegex 11188 ax-rrecex 11189 ax-cnre 11190 ax-pre-lttri 11191 ax-pre-lttrn 11192 ax-pre-ltadd 11193 ax-pre-mulgt0 11194 ax-riotaBAD 39787

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 2100 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3067 df-ral 3082 df-rex 3092 df-rmo 3371 df-reu 3372 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-tp 4596 df-op 4598 df-ot 4600 df-uni 4875 df-int 4915 df-iun 4960 df-iin 4961 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6306 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-riota 7376 df-ov 7422 df-oprab 7423 df-mpo 7424 df-of 7684 df-om 7869 df-1st 7992 df-2nd 7993 df-tpos 8228 df-undef 8275 df-frecs 8284 df-wrecs 8315 df-recs 8364 df-rdg 8403 df-1o 8459 df-2o 8460 df-er 8700 df-map 8832 df-en 8950 df-dom 8951 df-sdom 8952 df-fin 8953 df-pnf 11262 df-mnf 11263 df-xr 11264 df-ltxr 11265 df-le 11266 df-sub 11460 df-neg 11461 df-nn 12251 df-2 12320 df-3 12321 df-4 12322 df-5 12323 df-6 12324 df-n0 12522 df-z 12609 df-uz 12881 df-fz 13554 df-struct 17231 df-sets 17248 df-slot 17266 df-ndx 17278 df-base 17294 df-ress 17315 df-plusg 17347 df-mulr 17348 df-sca 17350 df-vsca 17351 df-0g 17518 df-mre 17662 df-mrc 17663 df-acs 17665 df-proset 18374 df-poset 18393 df-plt 18408 df-lub 18424 df-glb 18425 df-join 18426 df-meet 18427 df-p0 18503 df-p1 18504 df-lat 18512 df-clat 18579 df-mgm 18722 df-sgrp 18811 df-mnd 18827 df-submnd 18881 df-grp 19049 df-minusg 19050 df-sbg 19051 df-subg 19235 df-cntz 19433 df-oppg 19462 df-lsm 19752 df-cmn 19898 df-abl 19899 df-mgp 20263 df-rng 20277 df-ur 20310 df-ring 20363 df-oppr 20467 df-dvdsr 20487 df-unit 20488 df-invr 20518 df-dvr 20531 df-nzr 20662 df-rlreg 20845 df-domn 20846 df-drng 20881 df-lmod 21035 df-lss 21105 df-lsp 21145 df-lvec 21276 df-lsatoms 39810 df-lshyp 39811 df-lcv 39853 df-lfl 39892 df-lkr 39920 df-ldual 39958 df-oposet 40010 df-ol 40012 df-oml 40013 df-covers 40100 df-ats 40101 df-atl 40132 df-cvlat 40156 df-hlat 40185 df-llines 40332 df-lplanes 40333 df-lvols 40334 df-lines 40335 df-psubsp 40337 df-pmap 40338 df-padd 40630 df-lhyp 40822 df-laut 40823 df-ldil 40938 df-ltrn 40939 df-trl 40993 df-tgrp 41577 df-tendo 41589 df-edring 41591 df-dveca 41837 df-disoa 41863 df-dvech 41913 df-dib 41973 df-dic 42007 df-dih 42063 df-doch 42182 df-djh 42229 df-lcdual 42421 df-mapd 42459

This theorem is used by: mapdh8c 42615 mapdh8d0N 42616 mapdh8d 42617

W3C validator