Metamath Proof Explorer

Theorem hdmaprnlem3eN

Description: Lemma for hdmaprnN . (Contributed by NM, 29-May-2015) (New usage is discouraged.)

Ref Expression
Hypotheses hdmaprnlem1.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
hdmaprnlem1.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
hdmaprnlem1.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
hdmaprnlem1.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
hdmaprnlem1.c ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
hdmaprnlem1.l ⊢ 𝐿 = ( LSpan ‘ 𝐶 )
hdmaprnlem1.m ⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
hdmaprnlem1.s ⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
hdmaprnlem1.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
hdmaprnlem1.se ⊢ ( 𝜑 → 𝑠 ∈ ( 𝐷 ∖ { 𝑄 } ) )
hdmaprnlem1.ve ⊢ ( 𝜑 → 𝑣 ∈ 𝑉 )
hdmaprnlem1.e ⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { 𝑣 } ) ) = ( 𝐿 ‘ { 𝑠 } ) )
hdmaprnlem1.ue ⊢ ( 𝜑 → 𝑢 ∈ 𝑉 )
hdmaprnlem1.un ⊢ ( 𝜑 → ¬ 𝑢 ∈ ( 𝑁 ‘ { 𝑣 } ) )
hdmaprnlem1.d ⊢ 𝐷 = ( Base ‘ 𝐶 )
hdmaprnlem1.q ⊢ 𝑄 = ( 0g ‘ 𝐶 )
hdmaprnlem1.o ⊢ 0 = ( 0g ‘ 𝑈 )
hdmaprnlem1.a ⊢ ✚ = ( +g ‘ 𝐶 )
hdmaprnlem3e.p ⊢ + = ( +g ‘ 𝑈 )
Assertion hdmaprnlem3eN ( 𝜑 → ∃ 𝑡 ∈ ( ( 𝑁 ‘ { 𝑣 } ) ∖ { 0 } ) ( 𝐿 ‘ { ( ( 𝑆 ‘ 𝑢 ) ✚ 𝑠 ) } ) = ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑢 + 𝑡 ) } ) ) )

Proof

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