Proof of Theorem mapdh6dN
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | mapdh.h | . . . . . 6
⊢ 𝐻 = (LHyp‘𝐾) | 
| 2 |  | mapdh.c | . . . . . 6
⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) | 
| 3 |  | mapdh.k | . . . . . 6
⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) | 
| 4 | 1, 2, 3 | lcdlmod 41594 | . . . . 5
⊢ (𝜑 → 𝐶 ∈ LMod) | 
| 5 |  | mapdh.q | . . . . . 6
⊢ 𝑄 = (0g‘𝐶) | 
| 6 |  | mapdh.i | . . . . . 6
⊢ 𝐼 = (𝑥 ∈ V ↦ if((2nd
‘𝑥) = 0 , 𝑄, (℩ℎ ∈ 𝐷 ((𝑀‘(𝑁‘{(2nd ‘𝑥)})) = (𝐽‘{ℎ}) ∧ (𝑀‘(𝑁‘{((1st
‘(1st ‘𝑥)) − (2nd
‘𝑥))})) = (𝐽‘{((2nd
‘(1st ‘𝑥))𝑅ℎ)}))))) | 
| 7 |  | mapdh.m | . . . . . 6
⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) | 
| 8 |  | mapdh.u | . . . . . 6
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) | 
| 9 |  | mapdh.v | . . . . . 6
⊢ 𝑉 = (Base‘𝑈) | 
| 10 |  | mapdh.s | . . . . . 6
⊢  − =
(-g‘𝑈) | 
| 11 |  | mapdhc.o | . . . . . 6
⊢  0 =
(0g‘𝑈) | 
| 12 |  | mapdh.n | . . . . . 6
⊢ 𝑁 = (LSpan‘𝑈) | 
| 13 |  | mapdh.d | . . . . . 6
⊢ 𝐷 = (Base‘𝐶) | 
| 14 |  | mapdh.r | . . . . . 6
⊢ 𝑅 = (-g‘𝐶) | 
| 15 |  | mapdh.j | . . . . . 6
⊢ 𝐽 = (LSpan‘𝐶) | 
| 16 |  | mapdhc.f | . . . . . 6
⊢ (𝜑 → 𝐹 ∈ 𝐷) | 
| 17 |  | mapdh.mn | . . . . . 6
⊢ (𝜑 → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹})) | 
| 18 |  | mapdhcl.x | . . . . . 6
⊢ (𝜑 → 𝑋 ∈ (𝑉 ∖ { 0 })) | 
| 19 |  | mapdh6d.w | . . . . . . 7
⊢ (𝜑 → 𝑤 ∈ (𝑉 ∖ { 0 })) | 
| 20 | 19 | eldifad 3963 | . . . . . 6
⊢ (𝜑 → 𝑤 ∈ 𝑉) | 
| 21 | 1, 8, 3 | dvhlvec 41111 | . . . . . . . . 9
⊢ (𝜑 → 𝑈 ∈ LVec) | 
| 22 | 18 | eldifad 3963 | . . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ 𝑉) | 
| 23 |  | mapdh6d.y | . . . . . . . . . 10
⊢ (𝜑 → 𝑌 ∈ (𝑉 ∖ { 0 })) | 
| 24 | 23 | eldifad 3963 | . . . . . . . . 9
⊢ (𝜑 → 𝑌 ∈ 𝑉) | 
| 25 |  | mapdh6d.wn | . . . . . . . . 9
⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, 𝑌})) | 
| 26 | 9, 12, 21, 20, 22, 24, 25 | lspindpi 21134 | . . . . . . . 8
⊢ (𝜑 → ((𝑁‘{𝑤}) ≠ (𝑁‘{𝑋}) ∧ (𝑁‘{𝑤}) ≠ (𝑁‘{𝑌}))) | 
| 27 | 26 | simpld 494 | . . . . . . 7
⊢ (𝜑 → (𝑁‘{𝑤}) ≠ (𝑁‘{𝑋})) | 
| 28 | 27 | necomd 2996 | . . . . . 6
⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑤})) | 
| 29 | 5, 6, 1, 7, 8, 9, 10, 11, 12, 2, 13, 14, 15, 3, 16, 17, 18, 20, 28 | mapdhcl 41729 | . . . . 5
⊢ (𝜑 → (𝐼‘〈𝑋, 𝐹, 𝑤〉) ∈ 𝐷) | 
| 30 |  | mapdh.a | . . . . . 6
⊢  ✚ =
(+g‘𝐶) | 
| 31 | 13, 30, 5 | lmod0vrid 20891 | . . . . 5
⊢ ((𝐶 ∈ LMod ∧ (𝐼‘〈𝑋, 𝐹, 𝑤〉) ∈ 𝐷) → ((𝐼‘〈𝑋, 𝐹, 𝑤〉) ✚ 𝑄) = (𝐼‘〈𝑋, 𝐹, 𝑤〉)) | 
| 32 | 4, 29, 31 | syl2anc 584 | . . . 4
⊢ (𝜑 → ((𝐼‘〈𝑋, 𝐹, 𝑤〉) ✚ 𝑄) = (𝐼‘〈𝑋, 𝐹, 𝑤〉)) | 
| 33 | 32 | adantr 480 | . . 3
⊢ ((𝜑 ∧ (𝑌 + 𝑍) = 0 ) → ((𝐼‘〈𝑋, 𝐹, 𝑤〉) ✚ 𝑄) = (𝐼‘〈𝑋, 𝐹, 𝑤〉)) | 
| 34 |  | oteq3 4884 | . . . . . 6
⊢ ((𝑌 + 𝑍) = 0 → 〈𝑋, 𝐹, (𝑌 + 𝑍)〉 = 〈𝑋, 𝐹, 0 〉) | 
| 35 | 34 | fveq2d 6910 | . . . . 5
⊢ ((𝑌 + 𝑍) = 0 → (𝐼‘〈𝑋, 𝐹, (𝑌 + 𝑍)〉) = (𝐼‘〈𝑋, 𝐹, 0 〉)) | 
| 36 | 5, 6, 11, 18, 16 | mapdhval0 41727 | . . . . 5
⊢ (𝜑 → (𝐼‘〈𝑋, 𝐹, 0 〉) = 𝑄) | 
| 37 | 35, 36 | sylan9eqr 2799 | . . . 4
⊢ ((𝜑 ∧ (𝑌 + 𝑍) = 0 ) → (𝐼‘〈𝑋, 𝐹, (𝑌 + 𝑍)〉) = 𝑄) | 
| 38 | 37 | oveq2d 7447 | . . 3
⊢ ((𝜑 ∧ (𝑌 + 𝑍) = 0 ) → ((𝐼‘〈𝑋, 𝐹, 𝑤〉) ✚ (𝐼‘〈𝑋, 𝐹, (𝑌 + 𝑍)〉)) = ((𝐼‘〈𝑋, 𝐹, 𝑤〉) ✚ 𝑄)) | 
| 39 |  | oveq2 7439 | . . . . . 6
⊢ ((𝑌 + 𝑍) = 0 → (𝑤 + (𝑌 + 𝑍)) = (𝑤 + 0 )) | 
| 40 | 1, 8, 3 | dvhlmod 41112 | . . . . . . 7
⊢ (𝜑 → 𝑈 ∈ LMod) | 
| 41 |  | mapdh.p | . . . . . . . 8
⊢  + =
(+g‘𝑈) | 
| 42 | 9, 41, 11 | lmod0vrid 20891 | . . . . . . 7
⊢ ((𝑈 ∈ LMod ∧ 𝑤 ∈ 𝑉) → (𝑤 + 0 ) = 𝑤) | 
| 43 | 40, 20, 42 | syl2anc 584 | . . . . . 6
⊢ (𝜑 → (𝑤 + 0 ) = 𝑤) | 
| 44 | 39, 43 | sylan9eqr 2799 | . . . . 5
⊢ ((𝜑 ∧ (𝑌 + 𝑍) = 0 ) → (𝑤 + (𝑌 + 𝑍)) = 𝑤) | 
| 45 | 44 | oteq3d 4887 | . . . 4
⊢ ((𝜑 ∧ (𝑌 + 𝑍) = 0 ) → 〈𝑋, 𝐹, (𝑤 + (𝑌 + 𝑍))〉 = 〈𝑋, 𝐹, 𝑤〉) | 
| 46 | 45 | fveq2d 6910 | . . 3
⊢ ((𝜑 ∧ (𝑌 + 𝑍) = 0 ) → (𝐼‘〈𝑋, 𝐹, (𝑤 + (𝑌 + 𝑍))〉) = (𝐼‘〈𝑋, 𝐹, 𝑤〉)) | 
| 47 | 33, 38, 46 | 3eqtr4rd 2788 | . 2
⊢ ((𝜑 ∧ (𝑌 + 𝑍) = 0 ) → (𝐼‘〈𝑋, 𝐹, (𝑤 + (𝑌 + 𝑍))〉) = ((𝐼‘〈𝑋, 𝐹, 𝑤〉) ✚ (𝐼‘〈𝑋, 𝐹, (𝑌 + 𝑍)〉))) | 
| 48 | 3 | adantr 480 | . . 3
⊢ ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) | 
| 49 | 16 | adantr 480 | . . 3
⊢ ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → 𝐹 ∈ 𝐷) | 
| 50 | 17 | adantr 480 | . . 3
⊢ ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → (𝑀‘(𝑁‘{𝑋})) = (𝐽‘{𝐹})) | 
| 51 | 18 | adantr 480 | . . 3
⊢ ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → 𝑋 ∈ (𝑉 ∖ { 0 })) | 
| 52 | 19 | adantr 480 | . . 3
⊢ ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → 𝑤 ∈ (𝑉 ∖ { 0 })) | 
| 53 |  | mapdh6d.z | . . . . . . 7
⊢ (𝜑 → 𝑍 ∈ (𝑉 ∖ { 0 })) | 
| 54 | 53 | eldifad 3963 | . . . . . 6
⊢ (𝜑 → 𝑍 ∈ 𝑉) | 
| 55 | 9, 41 | lmodvacl 20873 | . . . . . 6
⊢ ((𝑈 ∈ LMod ∧ 𝑌 ∈ 𝑉 ∧ 𝑍 ∈ 𝑉) → (𝑌 + 𝑍) ∈ 𝑉) | 
| 56 | 40, 24, 54, 55 | syl3anc 1373 | . . . . 5
⊢ (𝜑 → (𝑌 + 𝑍) ∈ 𝑉) | 
| 57 | 56 | anim1i 615 | . . . 4
⊢ ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → ((𝑌 + 𝑍) ∈ 𝑉 ∧ (𝑌 + 𝑍) ≠ 0 )) | 
| 58 |  | eldifsn 4786 | . . . 4
⊢ ((𝑌 + 𝑍) ∈ (𝑉 ∖ { 0 }) ↔ ((𝑌 + 𝑍) ∈ 𝑉 ∧ (𝑌 + 𝑍) ≠ 0 )) | 
| 59 | 57, 58 | sylibr 234 | . . 3
⊢ ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → (𝑌 + 𝑍) ∈ (𝑉 ∖ { 0 })) | 
| 60 |  | mapdh6d.yz | . . . . . . 7
⊢ (𝜑 → (𝑁‘{𝑌}) = (𝑁‘{𝑍})) | 
| 61 |  | mapdh6d.xn | . . . . . . . . 9
⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑌, 𝑍})) | 
| 62 | 9, 12, 21, 22, 24, 54, 61 | lspindpi 21134 | . . . . . . . 8
⊢ (𝜑 → ((𝑁‘{𝑋}) ≠ (𝑁‘{𝑌}) ∧ (𝑁‘{𝑋}) ≠ (𝑁‘{𝑍}))) | 
| 63 | 62 | simpld 494 | . . . . . . 7
⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{𝑌})) | 
| 64 | 9, 41, 11, 12, 21, 18, 23, 53, 19, 60, 63, 25 | mapdindp1 41722 | . . . . . 6
⊢ (𝜑 → (𝑁‘{𝑋}) ≠ (𝑁‘{(𝑌 + 𝑍)})) | 
| 65 | 9, 41, 11, 12, 21, 18, 23, 53, 19, 60, 63, 25 | mapdindp2 41723 | . . . . . 6
⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑋, (𝑌 + 𝑍)})) | 
| 66 | 9, 11, 12, 21, 18, 56, 20, 64, 65 | lspindp1 21135 | . . . . 5
⊢ (𝜑 → ((𝑁‘{𝑤}) ≠ (𝑁‘{(𝑌 + 𝑍)}) ∧ ¬ 𝑋 ∈ (𝑁‘{𝑤, (𝑌 + 𝑍)}))) | 
| 67 | 66 | simprd 495 | . . . 4
⊢ (𝜑 → ¬ 𝑋 ∈ (𝑁‘{𝑤, (𝑌 + 𝑍)})) | 
| 68 | 67 | adantr 480 | . . 3
⊢ ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → ¬ 𝑋 ∈ (𝑁‘{𝑤, (𝑌 + 𝑍)})) | 
| 69 | 26 | simprd 495 | . . . . . . . . 9
⊢ (𝜑 → (𝑁‘{𝑤}) ≠ (𝑁‘{𝑌})) | 
| 70 | 9, 11, 12, 21, 19, 24, 69 | lspsnne1 21119 | . . . . . . . 8
⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑌})) | 
| 71 |  | eqid 2737 | . . . . . . . . . 10
⊢
(LSSum‘𝑈) =
(LSSum‘𝑈) | 
| 72 | 9, 12, 71, 40, 24, 54 | lsmpr 21088 | . . . . . . . . 9
⊢ (𝜑 → (𝑁‘{𝑌, 𝑍}) = ((𝑁‘{𝑌})(LSSum‘𝑈)(𝑁‘{𝑍}))) | 
| 73 | 60 | oveq2d 7447 | . . . . . . . . 9
⊢ (𝜑 → ((𝑁‘{𝑌})(LSSum‘𝑈)(𝑁‘{𝑌})) = ((𝑁‘{𝑌})(LSSum‘𝑈)(𝑁‘{𝑍}))) | 
| 74 |  | eqid 2737 | . . . . . . . . . . . . 13
⊢
(LSubSp‘𝑈) =
(LSubSp‘𝑈) | 
| 75 | 9, 74, 12 | lspsncl 20975 | . . . . . . . . . . . 12
⊢ ((𝑈 ∈ LMod ∧ 𝑌 ∈ 𝑉) → (𝑁‘{𝑌}) ∈ (LSubSp‘𝑈)) | 
| 76 | 40, 24, 75 | syl2anc 584 | . . . . . . . . . . 11
⊢ (𝜑 → (𝑁‘{𝑌}) ∈ (LSubSp‘𝑈)) | 
| 77 | 74 | lsssubg 20955 | . . . . . . . . . . 11
⊢ ((𝑈 ∈ LMod ∧ (𝑁‘{𝑌}) ∈ (LSubSp‘𝑈)) → (𝑁‘{𝑌}) ∈ (SubGrp‘𝑈)) | 
| 78 | 40, 76, 77 | syl2anc 584 | . . . . . . . . . 10
⊢ (𝜑 → (𝑁‘{𝑌}) ∈ (SubGrp‘𝑈)) | 
| 79 | 71 | lsmidm 19681 | . . . . . . . . . 10
⊢ ((𝑁‘{𝑌}) ∈ (SubGrp‘𝑈) → ((𝑁‘{𝑌})(LSSum‘𝑈)(𝑁‘{𝑌})) = (𝑁‘{𝑌})) | 
| 80 | 78, 79 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → ((𝑁‘{𝑌})(LSSum‘𝑈)(𝑁‘{𝑌})) = (𝑁‘{𝑌})) | 
| 81 | 72, 73, 80 | 3eqtr2d 2783 | . . . . . . . 8
⊢ (𝜑 → (𝑁‘{𝑌, 𝑍}) = (𝑁‘{𝑌})) | 
| 82 | 70, 81 | neleqtrrd 2864 | . . . . . . 7
⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑌, 𝑍})) | 
| 83 | 9, 41, 12, 40, 24, 54, 20, 82 | lspindp4 21139 | . . . . . 6
⊢ (𝜑 → ¬ 𝑤 ∈ (𝑁‘{𝑌, (𝑌 + 𝑍)})) | 
| 84 | 9, 12, 21, 20, 24, 56, 83 | lspindpi 21134 | . . . . 5
⊢ (𝜑 → ((𝑁‘{𝑤}) ≠ (𝑁‘{𝑌}) ∧ (𝑁‘{𝑤}) ≠ (𝑁‘{(𝑌 + 𝑍)}))) | 
| 85 | 84 | simprd 495 | . . . 4
⊢ (𝜑 → (𝑁‘{𝑤}) ≠ (𝑁‘{(𝑌 + 𝑍)})) | 
| 86 | 85 | adantr 480 | . . 3
⊢ ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → (𝑁‘{𝑤}) ≠ (𝑁‘{(𝑌 + 𝑍)})) | 
| 87 |  | eqidd 2738 | . . 3
⊢ ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → (𝐼‘〈𝑋, 𝐹, 𝑤〉) = (𝐼‘〈𝑋, 𝐹, 𝑤〉)) | 
| 88 |  | eqidd 2738 | . . 3
⊢ ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → (𝐼‘〈𝑋, 𝐹, (𝑌 + 𝑍)〉) = (𝐼‘〈𝑋, 𝐹, (𝑌 + 𝑍)〉)) | 
| 89 | 5, 6, 1, 7, 8, 9, 10, 11, 12, 2, 13, 14, 15, 48, 49, 50, 51, 41, 30, 52, 59, 68, 86, 87, 88 | mapdh6aN 41737 | . 2
⊢ ((𝜑 ∧ (𝑌 + 𝑍) ≠ 0 ) → (𝐼‘〈𝑋, 𝐹, (𝑤 + (𝑌 + 𝑍))〉) = ((𝐼‘〈𝑋, 𝐹, 𝑤〉) ✚ (𝐼‘〈𝑋, 𝐹, (𝑌 + 𝑍)〉))) | 
| 90 | 47, 89 | pm2.61dane 3029 | 1
⊢ (𝜑 → (𝐼‘〈𝑋, 𝐹, (𝑤 + (𝑌 + 𝑍))〉) = ((𝐼‘〈𝑋, 𝐹, 𝑤〉) ✚ (𝐼‘〈𝑋, 𝐹, (𝑌 + 𝑍)〉))) |