mapdh6eN - Mathbox for Norm Megill

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

Theorem mapdh6eN 38868

Description: Lemmma for mapdh6N 38875. Part (6) in [Baer] p. 47 line 38. (Contributed by NM, 1-May-2015.) (New usage is discouraged.)

**Hypotheses**
Ref	Expression
mapdh.q	⊢ 𝑄 = (0_g‘𝐶)
mapdh.i	⊢ 𝐼 = (𝑥 ∈ V ↦ if((2^nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2^nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1^st ‘(1^st ‘𝑥)) − (2^nd ‘𝑥))})) = (𝐽‘{((2^nd ‘(1^st ‘𝑥))𝑅ℎ)})))))
mapdh.h	⊢ 𝐻 = (LHyp‘𝐾)
mapdh.m	⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)
mapdh.u	⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
mapdh.v	⊢ 𝑉 = (Base‘𝑈)
mapdh.s	⊢ − = (-_g‘𝑈)
mapdhc.o	⊢ 0 = (0_g‘𝑈)
mapdh.n	⊢ 𝑁 = (LSpan‘𝑈)
mapdh.c	⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)
mapdh.d	⊢ 𝐷 = (Base‘𝐶)
mapdh.r	⊢ 𝑅 = (-_g‘𝐶)
mapdh.j	⊢ 𝐽 = (LSpan‘𝐶)
mapdh.k	⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
mapdhc.f	⊢ (𝜑 → 𝐹 ∈ 𝐷)
mapdh.mn	⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹}))
mapdhcl.x	⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))
mapdh.p	⊢ + = (+_g‘𝑈)
mapdh.a	⊢ ✚ = (+_g‘𝐶)
mapdh6d.xn	⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))
mapdh6d.yz	⊢ (𝜑 → (𝑁‘{𝑌}) = (𝑁‘{𝑍}))
mapdh6d.y	⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))
mapdh6d.z	⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 }))
mapdh6d.w	⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 }))
mapdh6d.wn	⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌}))

**Assertion**
Ref	Expression
mapdh6eN	⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, ((𝑤 + 𝑌) + 𝑍)⟩) = ((𝐼‘⟨𝑋, 𝐹, (𝑤 + 𝑌)⟩) ✚ (𝐼‘⟨𝑋, 𝐹, 𝑍⟩)))

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

**Proof of Theorem mapdh6eN**
Step	Hyp	Ref	Expression
1		mapdh.q	. 2 ⊢ 𝑄 = (0_g‘𝐶)
2		mapdh.i	. 2 ⊢ 𝐼 = (𝑥 ∈ V ↦ if((2^nd ‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2^nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1^st ‘(1^st ‘𝑥)) − (2^nd ‘𝑥))})) = (𝐽‘{((2^nd ‘(1^st ‘𝑥))𝑅ℎ)})))))
3		mapdh.h	. 2 ⊢ 𝐻 = (LHyp‘𝐾)
4		mapdh.m	. 2 ⊢ 𝑀 = ((mapd‘𝐾)‘𝑊)
5		mapdh.u	. 2 ⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊)
6		mapdh.v	. 2 ⊢ 𝑉 = (Base‘𝑈)
7		mapdh.s	. 2 ⊢ − = (-_g‘𝑈)
8		mapdhc.o	. 2 ⊢ 0 = (0_g‘𝑈)
9		mapdh.n	. 2 ⊢ 𝑁 = (LSpan‘𝑈)
10		mapdh.c	. 2 ⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊)
11		mapdh.d	. 2 ⊢ 𝐷 = (Base‘𝐶)
12		mapdh.r	. 2 ⊢ 𝑅 = (-_g‘𝐶)
13		mapdh.j	. 2 ⊢ 𝐽 = (LSpan‘𝐶)
14		mapdh.k	. 2 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
15		mapdhc.f	. 2 ⊢ (𝜑 → 𝐹 ∈ 𝐷)
16		mapdh.mn	. 2 ⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹}))
17		mapdhcl.x	. 2 ⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 }))
18		mapdh.p	. 2 ⊢ + = (+_g‘𝑈)
19		mapdh.a	. 2 ⊢ ✚ = (+_g‘𝐶)
20	3, 5, 14	dvhlmod 38238	. . . 4 ⊢ (𝜑 → 𝑈 ∈ LMod)
21		mapdh6d.w	. . . . 5 ⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 }))
22	21	eldifad 3946	. . . 4 ⊢ (𝜑 → 𝑤 ∈ 𝑉)
23		mapdh6d.y	. . . . 5 ⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 }))
24	23	eldifad 3946	. . . 4 ⊢ (𝜑 → 𝑌 ∈ 𝑉)
25	6, 18	lmodvacl 19640	. . . 4 ⊢ ((𝑈 ∈ LMod ∧ 𝑤 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑤 + 𝑌) ∈ 𝑉)
26	20, 22, 24, 25	syl3anc 1366	. . 3 ⊢ (𝜑 → (𝑤 + 𝑌) ∈ 𝑉)
27	3, 5, 14	dvhlvec 38237	. . . . . 6 ⊢ (𝜑 → 𝑈 ∈ LVec)
28	17	eldifad 3946	. . . . . 6 ⊢ (𝜑 → 𝑋 ∈ 𝑉)
29		mapdh6d.wn	. . . . . 6 ⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌}))
30	6, 9, 27, 22, 28, 24, 29	lspindpi 19896	. . . . 5 ⊢ (𝜑 → ((𝑁‘{𝑤}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑤}) ≠ (𝑁‘{𝑌})))
31	30	simprd 498	. . . 4 ⊢ (𝜑 → (𝑁‘{𝑤}) ≠ (𝑁‘{𝑌}))
32	6, 18, 8, 9, 20, 22, 24, 31	lmodindp1 19778	. . 3 ⊢ (𝜑 → (𝑤 + 𝑌) ≠ 0 )
33		eldifsn 4711	. . 3 ⊢ ((𝑤 + 𝑌) ∈ (𝑉 ∖ { 0 }) ↔ ((𝑤 + 𝑌) ∈ 𝑉 ∧ (𝑤 + 𝑌) ≠ 0 ))
34	26, 32, 33	sylanbrc 585	. 2 ⊢ (𝜑 → (𝑤 + 𝑌) ∈ (𝑉 ∖ { 0 }))
35		mapdh6d.z	. 2 ⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 }))
36	35	eldifad 3946	. . . . 5 ⊢ (𝜑 → 𝑍 ∈ 𝑉)
37		mapdh6d.yz	. . . . . 6 ⊢ (𝜑 → (𝑁‘{𝑌}) = (𝑁‘{𝑍}))
38		mapdh6d.xn	. . . . . . . 8 ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍}))
39	6, 9, 27, 28, 24, 36, 38	lspindpi 19896	. . . . . . 7 ⊢ (𝜑 → ((𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}) ∧ (𝑁‘{𝑋}) ≠ (𝑁‘{𝑍})))
40	39	simpld 497	. . . . . 6 ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}))
41	6, 18, 8, 9, 27, 17, 23, 35, 21, 37, 40, 29	mapdindp3 38850	. . . . 5 ⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{(𝑤 + 𝑌)}))
42	6, 18, 8, 9, 27, 17, 23, 35, 21, 37, 40, 29	mapdindp4 38851	. . . . 5 ⊢ (𝜑 → ¬ 𝑍 ∈ (𝑁‘{𝑋, (𝑤 + 𝑌)}))
43	6, 8, 9, 27, 17, 26, 36, 41, 42	lspindp1 19897	. . . 4 ⊢ (𝜑 → ((𝑁‘{𝑍}) ≠ (𝑁‘{(𝑤 + 𝑌)}) ∧ ¬ 𝑋 ∈ (𝑁‘{𝑍, (𝑤 + 𝑌)})))
44	43	simprd 498	. . 3 ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑍, (𝑤 + 𝑌)}))
45		prcom 4660	. . . . 5 ⊢ {(𝑤 + 𝑌), 𝑍} = {𝑍, (𝑤 + 𝑌)}
46	45	fveq2i 6666	. . . 4 ⊢ (𝑁‘{(𝑤 + 𝑌), 𝑍}) = (𝑁‘{𝑍, (𝑤 + 𝑌)})
47	46	eleq2i 2902	. . 3 ⊢ (𝑋 ∈ (𝑁‘{(𝑤 + 𝑌), 𝑍}) ↔ 𝑋 ∈ (𝑁‘{𝑍, (𝑤 + 𝑌)}))
48	44, 47	sylnibr 331	. 2 ⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{(𝑤 + 𝑌), 𝑍}))
49	6, 9, 27, 36, 28, 26, 42	lspindpi 19896	. . . 4 ⊢ (𝜑 → ((𝑁‘{𝑍}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑍}) ≠ (𝑁‘{(𝑤 + 𝑌)})))
50	49	simprd 498	. . 3 ⊢ (𝜑 → (𝑁‘{𝑍}) ≠ (𝑁‘{(𝑤 + 𝑌)}))
51	50	necomd 3069	. 2 ⊢ (𝜑 → (𝑁‘{(𝑤 + 𝑌)}) ≠ (𝑁‘{𝑍}))
52		eqidd 2820	. 2 ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, (𝑤 + 𝑌)⟩) = (𝐼‘⟨𝑋, 𝐹, (𝑤 + 𝑌)⟩))
53		eqidd 2820	. 2 ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, 𝑍⟩) = (𝐼‘⟨𝑋, 𝐹, 𝑍⟩))
54	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 34, 35, 48, 51, 52, 53	mapdh6aN 38863	1 ⊢ (𝜑 → (𝐼‘⟨𝑋, 𝐹, ((𝑤 + 𝑌) + 𝑍)⟩) = ((𝐼‘⟨𝑋, 𝐹, (𝑤 + 𝑌)⟩) ✚ (𝐼‘⟨𝑋, 𝐹, 𝑍⟩)))

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ∧ wa 398 = wceq 1531 ∈ wcel 2108 ≠ wne 3014 Vcvv 3493 ∖ cdif 3931 ifcif 4465 {csn 4559 {cpr 4561 ⟨cotp 4567 ↦ cmpt 5137 ‘cfv 6348 ℩crio 7105 (class class class)co 7148 1^st c1st 7679 2^nd c2nd 7680 Basecbs 16475 +_gcplusg 16557 0_gc0g 16705 -_gcsg 18097 LModclmod 19626 LSpanclspn 19735 HLchlt 36478 LHypclh 37112 DVecHcdvh 38206 LCDualclcd 38714 mapdcmpd 38752

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1905 ax-6 1964 ax-7 2009 ax-8 2110 ax-9 2118 ax-10 2139 ax-11 2154 ax-12 2170 ax-ext 2791 ax-rep 5181 ax-sep 5194 ax-nul 5201 ax-pow 5257 ax-pr 5320 ax-un 7453 ax-cnex 10585 ax-resscn 10586 ax-1cn 10587 ax-icn 10588 ax-addcl 10589 ax-addrcl 10590 ax-mulcl 10591 ax-mulrcl 10592 ax-mulcom 10593 ax-addass 10594 ax-mulass 10595 ax-distr 10596 ax-i2m1 10597 ax-1ne0 10598 ax-1rid 10599 ax-rnegex 10600 ax-rrecex 10601 ax-cnre 10602 ax-pre-lttri 10603 ax-pre-lttrn 10604 ax-pre-ltadd 10605 ax-pre-mulgt0 10606 ax-riotaBAD 36081

This theorem depends on definitions: df-bi 209 df-an 399 df-or 844 df-3or 1083 df-3an 1084 df-tru 1534 df-fal 1544 df-ex 1775 df-nf 1779 df-sb 2064 df-mo 2616 df-eu 2648 df-clab 2798 df-cleq 2812 df-clel 2891 df-nfc 2961 df-ne 3015 df-nel 3122 df-ral 3141 df-rex 3142 df-reu 3143 df-rmo 3144 df-rab 3145 df-v 3495 df-sbc 3771 df-csb 3882 df-dif 3937 df-un 3939 df-in 3941 df-ss 3950 df-pss 3952 df-nul 4290 df-if 4466 df-pw 4539 df-sn 4560 df-pr 4562 df-tp 4564 df-op 4566 df-ot 4568 df-uni 4831 df-int 4868 df-iun 4912 df-iin 4913 df-br 5058 df-opab 5120 df-mpt 5138 df-tr 5164 df-id 5453 df-eprel 5458 df-po 5467 df-so 5468 df-fr 5507 df-we 5509 df-xp 5554 df-rel 5555 df-cnv 5556 df-co 5557 df-dm 5558 df-rn 5559 df-res 5560 df-ima 5561 df-pred 6141 df-ord 6187 df-on 6188 df-lim 6189 df-suc 6190 df-iota 6307 df-fun 6350 df-fn 6351 df-f 6352 df-f1 6353 df-fo 6354 df-f1o 6355 df-fv 6356 df-riota 7106 df-ov 7151 df-oprab 7152 df-mpo 7153 df-of 7401 df-om 7573 df-1st 7681 df-2nd 7682 df-tpos 7884 df-undef 7931 df-wrecs 7939 df-recs 8000 df-rdg 8038 df-1o 8094 df-oadd 8098 df-er 8281 df-map 8400 df-en 8502 df-dom 8503 df-sdom 8504 df-fin 8505 df-pnf 10669 df-mnf 10670 df-xr 10671 df-ltxr 10672 df-le 10673 df-sub 10864 df-neg 10865 df-nn 11631 df-2 11692 df-3 11693 df-4 11694 df-5 11695 df-6 11696 df-n0 11890 df-z 11974 df-uz 12236 df-fz 12885 df-struct 16477 df-ndx 16478 df-slot 16479 df-base 16481 df-sets 16482 df-ress 16483 df-plusg 16570 df-mulr 16571 df-sca 16573 df-vsca 16574 df-0g 16707 df-mre 16849 df-mrc 16850 df-acs 16852 df-proset 17530 df-poset 17548 df-plt 17560 df-lub 17576 df-glb 17577 df-join 17578 df-meet 17579 df-p0 17641 df-p1 17642 df-lat 17648 df-clat 17710 df-mgm 17844 df-sgrp 17893 df-mnd 17904 df-submnd 17949 df-grp 18098 df-minusg 18099 df-sbg 18100 df-subg 18268 df-cntz 18439 df-oppg 18466 df-lsm 18753 df-cmn 18900 df-abl 18901 df-mgp 19232 df-ur 19244 df-ring 19291 df-oppr 19365 df-dvdsr 19383 df-unit 19384 df-invr 19414 df-dvr 19425 df-drng 19496 df-lmod 19628 df-lss 19696 df-lsp 19736 df-lvec 19867 df-lsatoms 36104 df-lshyp 36105 df-lcv 36147 df-lfl 36186 df-lkr 36214 df-ldual 36252 df-oposet 36304 df-ol 36306 df-oml 36307 df-covers 36394 df-ats 36395 df-atl 36426 df-cvlat 36450 df-hlat 36479 df-llines 36626 df-lplanes 36627 df-lvols 36628 df-lines 36629 df-psubsp 36631 df-pmap 36632 df-padd 36924 df-lhyp 37116 df-laut 37117 df-ldil 37232 df-ltrn 37233 df-trl 37287 df-tgrp 37871 df-tendo 37883 df-edring 37885 df-dveca 38131 df-disoa 38157 df-dvech 38207 df-dib 38267 df-dic 38301 df-dih 38357 df-doch 38476 df-djh 38523 df-lcdual 38715 df-mapd 38753

This theorem is referenced by: mapdh6gN 38870

W3C validator