Proof of Theorem hdmaprnlem3eN
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | hdmaprnlem1.v | . . 3
⊢ 𝑉 = (Base‘𝑈) | 
| 2 |  | hdmaprnlem3e.p | . . 3
⊢  + =
(+g‘𝑈) | 
| 3 |  | hdmaprnlem1.o | . . 3
⊢  0 =
(0g‘𝑈) | 
| 4 |  | hdmaprnlem1.n | . . 3
⊢ 𝑁 = (LSpan‘𝑈) | 
| 5 |  | eqid 2736 | . . 3
⊢
(LSAtoms‘𝑈) =
(LSAtoms‘𝑈) | 
| 6 |  | hdmaprnlem1.h | . . . 4
⊢ 𝐻 = (LHyp‘𝐾) | 
| 7 |  | hdmaprnlem1.u | . . . 4
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) | 
| 8 |  | hdmaprnlem1.k | . . . 4
⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) | 
| 9 | 6, 7, 8 | dvhlvec 41112 | . . 3
⊢ (𝜑 → 𝑈 ∈ LVec) | 
| 10 |  | hdmaprnlem1.m | . . . 4
⊢ 𝑀 = ((mapd‘𝐾)‘𝑊) | 
| 11 |  | hdmaprnlem1.c | . . . 4
⊢ 𝐶 = ((LCDual‘𝐾)‘𝑊) | 
| 12 |  | eqid 2736 | . . . 4
⊢
(LSAtoms‘𝐶) =
(LSAtoms‘𝐶) | 
| 13 |  | hdmaprnlem1.d | . . . . 5
⊢ 𝐷 = (Base‘𝐶) | 
| 14 |  | hdmaprnlem1.l | . . . . 5
⊢ 𝐿 = (LSpan‘𝐶) | 
| 15 |  | hdmaprnlem1.q | . . . . 5
⊢ 𝑄 = (0g‘𝐶) | 
| 16 | 6, 11, 8 | lcdlmod 41595 | . . . . 5
⊢ (𝜑 → 𝐶 ∈ LMod) | 
| 17 |  | hdmaprnlem1.s | . . . . . . . 8
⊢ 𝑆 = ((HDMap‘𝐾)‘𝑊) | 
| 18 |  | hdmaprnlem1.ue | . . . . . . . 8
⊢ (𝜑 → 𝑢 ∈ 𝑉) | 
| 19 | 6, 7, 1, 11, 13, 17, 8, 18 | hdmapcl 41833 | . . . . . . 7
⊢ (𝜑 → (𝑆‘𝑢) ∈ 𝐷) | 
| 20 |  | hdmaprnlem1.se | . . . . . . . 8
⊢ (𝜑 → 𝑠 ∈ (𝐷 ∖ {𝑄})) | 
| 21 | 20 | eldifad 3962 | . . . . . . 7
⊢ (𝜑 → 𝑠 ∈ 𝐷) | 
| 22 |  | hdmaprnlem1.a | . . . . . . . 8
⊢  ✚ =
(+g‘𝐶) | 
| 23 | 13, 22 | lmodvacl 20874 | . . . . . . 7
⊢ ((𝐶 ∈ LMod ∧ (𝑆‘𝑢) ∈ 𝐷 ∧ 𝑠 ∈ 𝐷) → ((𝑆‘𝑢) ✚ 𝑠) ∈ 𝐷) | 
| 24 | 16, 19, 21, 23 | syl3anc 1372 | . . . . . 6
⊢ (𝜑 → ((𝑆‘𝑢) ✚ 𝑠) ∈ 𝐷) | 
| 25 |  | hdmaprnlem1.ve | . . . . . . . 8
⊢ (𝜑 → 𝑣 ∈ 𝑉) | 
| 26 |  | hdmaprnlem1.e | . . . . . . . 8
⊢ (𝜑 → (𝑀‘(𝑁‘{𝑣})) = (𝐿‘{𝑠})) | 
| 27 |  | hdmaprnlem1.un | . . . . . . . 8
⊢ (𝜑 → ¬ 𝑢 ∈ (𝑁‘{𝑣})) | 
| 28 | 6, 7, 1, 4, 11, 14, 10, 17, 8, 20, 25, 26, 18, 27 | hdmaprnlem1N 41852 | . . . . . . 7
⊢ (𝜑 → (𝐿‘{(𝑆‘𝑢)}) ≠ (𝐿‘{𝑠})) | 
| 29 | 13, 22, 15, 14, 16, 19, 21, 28 | lmodindp1 21013 | . . . . . 6
⊢ (𝜑 → ((𝑆‘𝑢) ✚ 𝑠) ≠ 𝑄) | 
| 30 |  | eldifsn 4785 | . . . . . 6
⊢ (((𝑆‘𝑢) ✚ 𝑠) ∈ (𝐷 ∖ {𝑄}) ↔ (((𝑆‘𝑢) ✚ 𝑠) ∈ 𝐷 ∧ ((𝑆‘𝑢) ✚ 𝑠) ≠ 𝑄)) | 
| 31 | 24, 29, 30 | sylanbrc 583 | . . . . 5
⊢ (𝜑 → ((𝑆‘𝑢) ✚ 𝑠) ∈ (𝐷 ∖ {𝑄})) | 
| 32 | 13, 14, 15, 12, 16, 31 | lsatlspsn 38995 | . . . 4
⊢ (𝜑 → (𝐿‘{((𝑆‘𝑢) ✚ 𝑠)}) ∈ (LSAtoms‘𝐶)) | 
| 33 | 6, 10, 7, 5, 11, 12, 8, 32 | mapdcnvatN 41669 | . . 3
⊢ (𝜑 → (◡𝑀‘(𝐿‘{((𝑆‘𝑢) ✚ 𝑠)})) ∈ (LSAtoms‘𝑈)) | 
| 34 | 6, 7, 1, 4, 11, 14, 10, 17, 8, 20, 25, 26, 18, 27, 13, 15, 3, 22 | hdmaprnlem3uN 41854 | . . . 4
⊢ (𝜑 → (𝑁‘{𝑢}) ≠ (◡𝑀‘(𝐿‘{((𝑆‘𝑢) ✚ 𝑠)}))) | 
| 35 | 34 | necomd 2995 | . . 3
⊢ (𝜑 → (◡𝑀‘(𝐿‘{((𝑆‘𝑢) ✚ 𝑠)})) ≠ (𝑁‘{𝑢})) | 
| 36 | 6, 7, 1, 4, 11, 14, 10, 17, 8, 20, 25, 26, 18, 27, 13, 15, 3, 22 | hdmaprnlem3N 41853 | . . . 4
⊢ (𝜑 → (𝑁‘{𝑣}) ≠ (◡𝑀‘(𝐿‘{((𝑆‘𝑢) ✚ 𝑠)}))) | 
| 37 | 36 | necomd 2995 | . . 3
⊢ (𝜑 → (◡𝑀‘(𝐿‘{((𝑆‘𝑢) ✚ 𝑠)})) ≠ (𝑁‘{𝑣})) | 
| 38 |  | eqid 2736 | . . . . . . 7
⊢
(LSubSp‘𝐶) =
(LSubSp‘𝐶) | 
| 39 |  | eqid 2736 | . . . . . . . . 9
⊢
(LSubSp‘𝑈) =
(LSubSp‘𝑈) | 
| 40 | 6, 7, 8 | dvhlmod 41113 | . . . . . . . . . 10
⊢ (𝜑 → 𝑈 ∈ LMod) | 
| 41 | 1, 39, 4 | lspsncl 20976 | . . . . . . . . . 10
⊢ ((𝑈 ∈ LMod ∧ 𝑢 ∈ 𝑉) → (𝑁‘{𝑢}) ∈ (LSubSp‘𝑈)) | 
| 42 | 40, 18, 41 | syl2anc 584 | . . . . . . . . 9
⊢ (𝜑 → (𝑁‘{𝑢}) ∈ (LSubSp‘𝑈)) | 
| 43 | 6, 10, 7, 39, 11, 38, 8, 42 | mapdcl2 41659 | . . . . . . . 8
⊢ (𝜑 → (𝑀‘(𝑁‘{𝑢})) ∈ (LSubSp‘𝐶)) | 
| 44 | 1, 39, 4 | lspsncl 20976 | . . . . . . . . . 10
⊢ ((𝑈 ∈ LMod ∧ 𝑣 ∈ 𝑉) → (𝑁‘{𝑣}) ∈ (LSubSp‘𝑈)) | 
| 45 | 40, 25, 44 | syl2anc 584 | . . . . . . . . 9
⊢ (𝜑 → (𝑁‘{𝑣}) ∈ (LSubSp‘𝑈)) | 
| 46 | 6, 10, 7, 39, 11, 38, 8, 45 | mapdcl2 41659 | . . . . . . . 8
⊢ (𝜑 → (𝑀‘(𝑁‘{𝑣})) ∈ (LSubSp‘𝐶)) | 
| 47 |  | eqid 2736 | . . . . . . . . 9
⊢
(LSSum‘𝐶) =
(LSSum‘𝐶) | 
| 48 | 38, 47 | lsmcl 21083 | . . . . . . . 8
⊢ ((𝐶 ∈ LMod ∧ (𝑀‘(𝑁‘{𝑢})) ∈ (LSubSp‘𝐶) ∧ (𝑀‘(𝑁‘{𝑣})) ∈ (LSubSp‘𝐶)) → ((𝑀‘(𝑁‘{𝑢}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑣}))) ∈ (LSubSp‘𝐶)) | 
| 49 | 16, 43, 46, 48 | syl3anc 1372 | . . . . . . 7
⊢ (𝜑 → ((𝑀‘(𝑁‘{𝑢}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑣}))) ∈ (LSubSp‘𝐶)) | 
| 50 | 38 | lsssssubg 20957 | . . . . . . . . . 10
⊢ (𝐶 ∈ LMod →
(LSubSp‘𝐶) ⊆
(SubGrp‘𝐶)) | 
| 51 | 16, 50 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → (LSubSp‘𝐶) ⊆ (SubGrp‘𝐶)) | 
| 52 | 51, 43 | sseldd 3983 | . . . . . . . 8
⊢ (𝜑 → (𝑀‘(𝑁‘{𝑢})) ∈ (SubGrp‘𝐶)) | 
| 53 | 51, 46 | sseldd 3983 | . . . . . . . 8
⊢ (𝜑 → (𝑀‘(𝑁‘{𝑣})) ∈ (SubGrp‘𝐶)) | 
| 54 | 13, 14 | lspsnid 20992 | . . . . . . . . . 10
⊢ ((𝐶 ∈ LMod ∧ (𝑆‘𝑢) ∈ 𝐷) → (𝑆‘𝑢) ∈ (𝐿‘{(𝑆‘𝑢)})) | 
| 55 | 16, 19, 54 | syl2anc 584 | . . . . . . . . 9
⊢ (𝜑 → (𝑆‘𝑢) ∈ (𝐿‘{(𝑆‘𝑢)})) | 
| 56 | 6, 7, 1, 4, 11, 14, 10, 17, 8, 18 | hdmap10 41843 | . . . . . . . . 9
⊢ (𝜑 → (𝑀‘(𝑁‘{𝑢})) = (𝐿‘{(𝑆‘𝑢)})) | 
| 57 | 55, 56 | eleqtrrd 2843 | . . . . . . . 8
⊢ (𝜑 → (𝑆‘𝑢) ∈ (𝑀‘(𝑁‘{𝑢}))) | 
| 58 |  | eqimss2 4042 | . . . . . . . . . 10
⊢ ((𝑀‘(𝑁‘{𝑣})) = (𝐿‘{𝑠}) → (𝐿‘{𝑠}) ⊆ (𝑀‘(𝑁‘{𝑣}))) | 
| 59 | 26, 58 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → (𝐿‘{𝑠}) ⊆ (𝑀‘(𝑁‘{𝑣}))) | 
| 60 | 13, 38, 14, 16, 46, 21 | ellspsn5b 20994 | . . . . . . . . 9
⊢ (𝜑 → (𝑠 ∈ (𝑀‘(𝑁‘{𝑣})) ↔ (𝐿‘{𝑠}) ⊆ (𝑀‘(𝑁‘{𝑣})))) | 
| 61 | 59, 60 | mpbird 257 | . . . . . . . 8
⊢ (𝜑 → 𝑠 ∈ (𝑀‘(𝑁‘{𝑣}))) | 
| 62 | 22, 47 | lsmelvali 19669 | . . . . . . . 8
⊢ ((((𝑀‘(𝑁‘{𝑢})) ∈ (SubGrp‘𝐶) ∧ (𝑀‘(𝑁‘{𝑣})) ∈ (SubGrp‘𝐶)) ∧ ((𝑆‘𝑢) ∈ (𝑀‘(𝑁‘{𝑢})) ∧ 𝑠 ∈ (𝑀‘(𝑁‘{𝑣})))) → ((𝑆‘𝑢) ✚ 𝑠) ∈ ((𝑀‘(𝑁‘{𝑢}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑣})))) | 
| 63 | 52, 53, 57, 61, 62 | syl22anc 838 | . . . . . . 7
⊢ (𝜑 → ((𝑆‘𝑢) ✚ 𝑠) ∈ ((𝑀‘(𝑁‘{𝑢}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑣})))) | 
| 64 | 38, 14, 16, 49, 63 | ellspsn5 20995 | . . . . . 6
⊢ (𝜑 → (𝐿‘{((𝑆‘𝑢) ✚ 𝑠)}) ⊆ ((𝑀‘(𝑁‘{𝑢}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑣})))) | 
| 65 |  | eqid 2736 | . . . . . . 7
⊢
(LSSum‘𝑈) =
(LSSum‘𝑈) | 
| 66 | 6, 10, 7, 39, 65, 11, 47, 8, 42, 45 | mapdlsm 41667 | . . . . . 6
⊢ (𝜑 → (𝑀‘((𝑁‘{𝑢})(LSSum‘𝑈)(𝑁‘{𝑣}))) = ((𝑀‘(𝑁‘{𝑢}))(LSSum‘𝐶)(𝑀‘(𝑁‘{𝑣})))) | 
| 67 | 64, 66 | sseqtrrd 4020 | . . . . 5
⊢ (𝜑 → (𝐿‘{((𝑆‘𝑢) ✚ 𝑠)}) ⊆ (𝑀‘((𝑁‘{𝑢})(LSSum‘𝑈)(𝑁‘{𝑣})))) | 
| 68 | 13, 38, 14 | lspsncl 20976 | . . . . . . . 8
⊢ ((𝐶 ∈ LMod ∧ ((𝑆‘𝑢) ✚ 𝑠) ∈ 𝐷) → (𝐿‘{((𝑆‘𝑢) ✚ 𝑠)}) ∈ (LSubSp‘𝐶)) | 
| 69 | 16, 24, 68 | syl2anc 584 | . . . . . . 7
⊢ (𝜑 → (𝐿‘{((𝑆‘𝑢) ✚ 𝑠)}) ∈ (LSubSp‘𝐶)) | 
| 70 | 6, 10, 11, 38, 8 | mapdrn2 41654 | . . . . . . 7
⊢ (𝜑 → ran 𝑀 = (LSubSp‘𝐶)) | 
| 71 | 69, 70 | eleqtrrd 2843 | . . . . . 6
⊢ (𝜑 → (𝐿‘{((𝑆‘𝑢) ✚ 𝑠)}) ∈ ran 𝑀) | 
| 72 | 39, 65 | lsmcl 21083 | . . . . . . . 8
⊢ ((𝑈 ∈ LMod ∧ (𝑁‘{𝑢}) ∈ (LSubSp‘𝑈) ∧ (𝑁‘{𝑣}) ∈ (LSubSp‘𝑈)) → ((𝑁‘{𝑢})(LSSum‘𝑈)(𝑁‘{𝑣})) ∈ (LSubSp‘𝑈)) | 
| 73 | 40, 42, 45, 72 | syl3anc 1372 | . . . . . . 7
⊢ (𝜑 → ((𝑁‘{𝑢})(LSSum‘𝑈)(𝑁‘{𝑣})) ∈ (LSubSp‘𝑈)) | 
| 74 | 6, 10, 7, 39, 8, 73 | mapdcl 41656 | . . . . . 6
⊢ (𝜑 → (𝑀‘((𝑁‘{𝑢})(LSSum‘𝑈)(𝑁‘{𝑣}))) ∈ ran 𝑀) | 
| 75 | 6, 10, 8, 71, 74 | mapdcnvordN 41661 | . . . . 5
⊢ (𝜑 → ((◡𝑀‘(𝐿‘{((𝑆‘𝑢) ✚ 𝑠)})) ⊆ (◡𝑀‘(𝑀‘((𝑁‘{𝑢})(LSSum‘𝑈)(𝑁‘{𝑣})))) ↔ (𝐿‘{((𝑆‘𝑢) ✚ 𝑠)}) ⊆ (𝑀‘((𝑁‘{𝑢})(LSSum‘𝑈)(𝑁‘{𝑣}))))) | 
| 76 | 67, 75 | mpbird 257 | . . . 4
⊢ (𝜑 → (◡𝑀‘(𝐿‘{((𝑆‘𝑢) ✚ 𝑠)})) ⊆ (◡𝑀‘(𝑀‘((𝑁‘{𝑢})(LSSum‘𝑈)(𝑁‘{𝑣}))))) | 
| 77 | 1, 4, 65, 40, 18, 25 | lsmpr 21089 | . . . . 5
⊢ (𝜑 → (𝑁‘{𝑢, 𝑣}) = ((𝑁‘{𝑢})(LSSum‘𝑈)(𝑁‘{𝑣}))) | 
| 78 | 6, 10, 7, 39, 8, 73 | mapdcnvid1N 41657 | . . . . 5
⊢ (𝜑 → (◡𝑀‘(𝑀‘((𝑁‘{𝑢})(LSSum‘𝑈)(𝑁‘{𝑣})))) = ((𝑁‘{𝑢})(LSSum‘𝑈)(𝑁‘{𝑣}))) | 
| 79 | 77, 78 | eqtr4d 2779 | . . . 4
⊢ (𝜑 → (𝑁‘{𝑢, 𝑣}) = (◡𝑀‘(𝑀‘((𝑁‘{𝑢})(LSSum‘𝑈)(𝑁‘{𝑣}))))) | 
| 80 | 76, 79 | sseqtrrd 4020 | . . 3
⊢ (𝜑 → (◡𝑀‘(𝐿‘{((𝑆‘𝑢) ✚ 𝑠)})) ⊆ (𝑁‘{𝑢, 𝑣})) | 
| 81 | 1, 2, 3, 4, 5, 9, 33, 18, 25, 35, 37, 80 | lsatfixedN 39011 | . 2
⊢ (𝜑 → ∃𝑡 ∈ ((𝑁‘{𝑣}) ∖ { 0 })(◡𝑀‘(𝐿‘{((𝑆‘𝑢) ✚ 𝑠)})) = (𝑁‘{(𝑢 + 𝑡)})) | 
| 82 |  | simpr 484 | . . . . . 6
⊢ (((𝜑 ∧ 𝑡 ∈ ((𝑁‘{𝑣}) ∖ { 0 })) ∧ (◡𝑀‘(𝐿‘{((𝑆‘𝑢) ✚ 𝑠)})) = (𝑁‘{(𝑢 + 𝑡)})) → (◡𝑀‘(𝐿‘{((𝑆‘𝑢) ✚ 𝑠)})) = (𝑁‘{(𝑢 + 𝑡)})) | 
| 83 | 8 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ ((𝑁‘{𝑣}) ∖ { 0 })) ∧ (◡𝑀‘(𝐿‘{((𝑆‘𝑢) ✚ 𝑠)})) = (𝑁‘{(𝑢 + 𝑡)})) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) | 
| 84 | 40 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ ((𝑁‘{𝑣}) ∖ { 0 })) ∧ (◡𝑀‘(𝐿‘{((𝑆‘𝑢) ✚ 𝑠)})) = (𝑁‘{(𝑢 + 𝑡)})) → 𝑈 ∈ LMod) | 
| 85 | 18 | ad2antrr 726 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ ((𝑁‘{𝑣}) ∖ { 0 })) ∧ (◡𝑀‘(𝐿‘{((𝑆‘𝑢) ✚ 𝑠)})) = (𝑁‘{(𝑢 + 𝑡)})) → 𝑢 ∈ 𝑉) | 
| 86 | 20 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ ((𝑁‘{𝑣}) ∖ { 0 })) ∧ (◡𝑀‘(𝐿‘{((𝑆‘𝑢) ✚ 𝑠)})) = (𝑁‘{(𝑢 + 𝑡)})) → 𝑠 ∈ (𝐷 ∖ {𝑄})) | 
| 87 | 25 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ ((𝑁‘{𝑣}) ∖ { 0 })) ∧ (◡𝑀‘(𝐿‘{((𝑆‘𝑢) ✚ 𝑠)})) = (𝑁‘{(𝑢 + 𝑡)})) → 𝑣 ∈ 𝑉) | 
| 88 | 26 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ ((𝑁‘{𝑣}) ∖ { 0 })) ∧ (◡𝑀‘(𝐿‘{((𝑆‘𝑢) ✚ 𝑠)})) = (𝑁‘{(𝑢 + 𝑡)})) → (𝑀‘(𝑁‘{𝑣})) = (𝐿‘{𝑠})) | 
| 89 | 27 | ad2antrr 726 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ ((𝑁‘{𝑣}) ∖ { 0 })) ∧ (◡𝑀‘(𝐿‘{((𝑆‘𝑢) ✚ 𝑠)})) = (𝑁‘{(𝑢 + 𝑡)})) → ¬ 𝑢 ∈ (𝑁‘{𝑣})) | 
| 90 |  | simplr 768 | . . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑡 ∈ ((𝑁‘{𝑣}) ∖ { 0 })) ∧ (◡𝑀‘(𝐿‘{((𝑆‘𝑢) ✚ 𝑠)})) = (𝑁‘{(𝑢 + 𝑡)})) → 𝑡 ∈ ((𝑁‘{𝑣}) ∖ { 0 })) | 
| 91 | 6, 7, 1, 4, 11, 14, 10, 17, 83, 86, 87, 88, 85, 89, 13, 15, 3, 22, 90 | hdmaprnlem4tN 41855 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑡 ∈ ((𝑁‘{𝑣}) ∖ { 0 })) ∧ (◡𝑀‘(𝐿‘{((𝑆‘𝑢) ✚ 𝑠)})) = (𝑁‘{(𝑢 + 𝑡)})) → 𝑡 ∈ 𝑉) | 
| 92 | 1, 2 | lmodvacl 20874 | . . . . . . . . 9
⊢ ((𝑈 ∈ LMod ∧ 𝑢 ∈ 𝑉 ∧ 𝑡 ∈ 𝑉) → (𝑢 + 𝑡) ∈ 𝑉) | 
| 93 | 84, 85, 91, 92 | syl3anc 1372 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑡 ∈ ((𝑁‘{𝑣}) ∖ { 0 })) ∧ (◡𝑀‘(𝐿‘{((𝑆‘𝑢) ✚ 𝑠)})) = (𝑁‘{(𝑢 + 𝑡)})) → (𝑢 + 𝑡) ∈ 𝑉) | 
| 94 | 1, 39, 4 | lspsncl 20976 | . . . . . . . 8
⊢ ((𝑈 ∈ LMod ∧ (𝑢 + 𝑡) ∈ 𝑉) → (𝑁‘{(𝑢 + 𝑡)}) ∈ (LSubSp‘𝑈)) | 
| 95 | 84, 93, 94 | syl2anc 584 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑡 ∈ ((𝑁‘{𝑣}) ∖ { 0 })) ∧ (◡𝑀‘(𝐿‘{((𝑆‘𝑢) ✚ 𝑠)})) = (𝑁‘{(𝑢 + 𝑡)})) → (𝑁‘{(𝑢 + 𝑡)}) ∈ (LSubSp‘𝑈)) | 
| 96 | 6, 10, 7, 39, 83, 95 | mapdcnvid1N 41657 | . . . . . 6
⊢ (((𝜑 ∧ 𝑡 ∈ ((𝑁‘{𝑣}) ∖ { 0 })) ∧ (◡𝑀‘(𝐿‘{((𝑆‘𝑢) ✚ 𝑠)})) = (𝑁‘{(𝑢 + 𝑡)})) → (◡𝑀‘(𝑀‘(𝑁‘{(𝑢 + 𝑡)}))) = (𝑁‘{(𝑢 + 𝑡)})) | 
| 97 | 82, 96 | eqtr4d 2779 | . . . . 5
⊢ (((𝜑 ∧ 𝑡 ∈ ((𝑁‘{𝑣}) ∖ { 0 })) ∧ (◡𝑀‘(𝐿‘{((𝑆‘𝑢) ✚ 𝑠)})) = (𝑁‘{(𝑢 + 𝑡)})) → (◡𝑀‘(𝐿‘{((𝑆‘𝑢) ✚ 𝑠)})) = (◡𝑀‘(𝑀‘(𝑁‘{(𝑢 + 𝑡)})))) | 
| 98 | 71 | ad2antrr 726 | . . . . . 6
⊢ (((𝜑 ∧ 𝑡 ∈ ((𝑁‘{𝑣}) ∖ { 0 })) ∧ (◡𝑀‘(𝐿‘{((𝑆‘𝑢) ✚ 𝑠)})) = (𝑁‘{(𝑢 + 𝑡)})) → (𝐿‘{((𝑆‘𝑢) ✚ 𝑠)}) ∈ ran 𝑀) | 
| 99 | 6, 10, 7, 39, 83, 95 | mapdcl 41656 | . . . . . 6
⊢ (((𝜑 ∧ 𝑡 ∈ ((𝑁‘{𝑣}) ∖ { 0 })) ∧ (◡𝑀‘(𝐿‘{((𝑆‘𝑢) ✚ 𝑠)})) = (𝑁‘{(𝑢 + 𝑡)})) → (𝑀‘(𝑁‘{(𝑢 + 𝑡)})) ∈ ran 𝑀) | 
| 100 | 6, 10, 83, 98, 99 | mapdcnv11N 41662 | . . . . 5
⊢ (((𝜑 ∧ 𝑡 ∈ ((𝑁‘{𝑣}) ∖ { 0 })) ∧ (◡𝑀‘(𝐿‘{((𝑆‘𝑢) ✚ 𝑠)})) = (𝑁‘{(𝑢 + 𝑡)})) → ((◡𝑀‘(𝐿‘{((𝑆‘𝑢) ✚ 𝑠)})) = (◡𝑀‘(𝑀‘(𝑁‘{(𝑢 + 𝑡)}))) ↔ (𝐿‘{((𝑆‘𝑢) ✚ 𝑠)}) = (𝑀‘(𝑁‘{(𝑢 + 𝑡)})))) | 
| 101 | 97, 100 | mpbid 232 | . . . 4
⊢ (((𝜑 ∧ 𝑡 ∈ ((𝑁‘{𝑣}) ∖ { 0 })) ∧ (◡𝑀‘(𝐿‘{((𝑆‘𝑢) ✚ 𝑠)})) = (𝑁‘{(𝑢 + 𝑡)})) → (𝐿‘{((𝑆‘𝑢) ✚ 𝑠)}) = (𝑀‘(𝑁‘{(𝑢 + 𝑡)}))) | 
| 102 | 101 | ex 412 | . . 3
⊢ ((𝜑 ∧ 𝑡 ∈ ((𝑁‘{𝑣}) ∖ { 0 })) → ((◡𝑀‘(𝐿‘{((𝑆‘𝑢) ✚ 𝑠)})) = (𝑁‘{(𝑢 + 𝑡)}) → (𝐿‘{((𝑆‘𝑢) ✚ 𝑠)}) = (𝑀‘(𝑁‘{(𝑢 + 𝑡)})))) | 
| 103 | 102 | reximdva 3167 | . 2
⊢ (𝜑 → (∃𝑡 ∈ ((𝑁‘{𝑣}) ∖ { 0 })(◡𝑀‘(𝐿‘{((𝑆‘𝑢) ✚ 𝑠)})) = (𝑁‘{(𝑢 + 𝑡)}) → ∃𝑡 ∈ ((𝑁‘{𝑣}) ∖ { 0 })(𝐿‘{((𝑆‘𝑢) ✚ 𝑠)}) = (𝑀‘(𝑁‘{(𝑢 + 𝑡)})))) | 
| 104 | 81, 103 | mpd 15 | 1
⊢ (𝜑 → ∃𝑡 ∈ ((𝑁‘{𝑣}) ∖ { 0 })(𝐿‘{((𝑆‘𝑢) ✚ 𝑠)}) = (𝑀‘(𝑁‘{(𝑢 + 𝑡)}))) |