Metamath Proof Explorer

Theorem hdmap11lem2

Description: Lemma for hdmapadd . (Contributed by NM, 26-May-2015)

Ref Expression
Hypotheses hdmap11.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
hdmap11.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
hdmap11.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
hdmap11.p ⊢ + = ( +g ‘ 𝑈 )
hdmap11.c ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
hdmap11.a ⊢ ✚ = ( +g ‘ 𝐶 )
hdmap11.s ⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
hdmap11.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
hdmap11.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
hdmap11.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
hdmap11.e ⊢ 𝐸 = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩
hdmap11.o ⊢ 0 = ( 0g ‘ 𝑈 )
hdmap11.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
hdmap11.d ⊢ 𝐷 = ( Base ‘ 𝐶 )
hdmap11.l ⊢ 𝐿 = ( LSpan ‘ 𝐶 )
hdmap11.m ⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
hdmap11.j ⊢ 𝐽 = ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 )
hdmap11.i ⊢ 𝐼 = ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 )
Assertion hdmap11lem2 ( 𝜑 → ( 𝑆 ‘ ( 𝑋 + 𝑌 ) ) = ( ( 𝑆 ‘ 𝑋 ) ✚ ( 𝑆 ‘ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 hdmap11.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 hdmap11.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 hdmap11.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
4 hdmap11.p ⊢ + = ( +g ‘ 𝑈 )
5 hdmap11.c ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
6 hdmap11.a ⊢ ✚ = ( +g ‘ 𝐶 )
7 hdmap11.s ⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
8 hdmap11.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
9 hdmap11.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
10 hdmap11.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
11 hdmap11.e ⊢ 𝐸 = ⟨ ( I ↾ ( Base ‘ 𝐾 ) ) , ( I ↾ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) ) ⟩
12 hdmap11.o ⊢ 0 = ( 0g ‘ 𝑈 )
13 hdmap11.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
14 hdmap11.d ⊢ 𝐷 = ( Base ‘ 𝐶 )
15 hdmap11.l ⊢ 𝐿 = ( LSpan ‘ 𝐶 )
16 hdmap11.m ⊢ 𝑀 = ( ( mapd ‘ 𝐾 ) ‘ 𝑊 )
17 hdmap11.j ⊢ 𝐽 = ( ( HVMap ‘ 𝐾 ) ‘ 𝑊 )
18 hdmap11.i ⊢ 𝐼 = ( ( HDMap1 ‘ 𝐾 ) ‘ 𝑊 )
19 1 2 3 13 8 9 10 dvh3dim ⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
20 19 adantr ⊢ ( ( 𝜑 ∧ 𝐸 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) → ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
21 eqid ⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
22 1 2 8 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
23 22 adantr ⊢ ( ( 𝜑 ∧ 𝐸 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) → 𝑈 ∈ LMod )
24 3 21 13 22 9 10 lspprcl ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∈ ( LSubSp ‘ 𝑈 ) )
25 24 adantr ⊢ ( ( 𝜑 ∧ 𝐸 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∈ ( LSubSp ‘ 𝑈 ) )
26 simpr ⊢ ( ( 𝜑 ∧ 𝐸 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) → 𝐸 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
27 21 13 23 25 26 lspsnel5a ⊢ ( ( 𝜑 ∧ 𝐸 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) → ( 𝑁 ‘ { 𝐸 } ) ⊆ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
28 27 ssneld ⊢ ( ( 𝜑 ∧ 𝐸 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) → ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) → ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝐸 } ) ) )
29 28 ancld ⊢ ( ( 𝜑 ∧ 𝐸 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) → ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) → ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝐸 } ) ) ) )
30 29 reximdv ⊢ ( ( 𝜑 ∧ 𝐸 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) → ( ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) → ∃ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝐸 } ) ) ) )
31 20 30 mpd ⊢ ( ( 𝜑 ∧ 𝐸 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) → ∃ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝐸 } ) ) )
32 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
33 eqid ⊢ ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
34 1 32 33 2 3 12 11 8 dvheveccl ⊢ ( 𝜑 → 𝐸 ∈ ( 𝑉 ∖ { 0 } ) )
35 34 eldifad ⊢ ( 𝜑 → 𝐸 ∈ 𝑉 )
36 1 2 3 13 8 35 10 dvh3dim ⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝐸 , 𝑌 } ) )
37 36 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = 0 ) → ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝐸 , 𝑌 } ) )
38 preq1 ⊢ ( 𝑋 = 0 → { 𝑋 , 𝑌 } = { 0 , 𝑌 } )
39 prcom ⊢ { 0 , 𝑌 } = { 𝑌 , 0 }
40 38 39 eqtrdi ⊢ ( 𝑋 = 0 → { 𝑋 , 𝑌 } = { 𝑌 , 0 } )
41 40 fveq2d ⊢ ( 𝑋 = 0 → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) = ( 𝑁 ‘ { 𝑌 , 0 } ) )
42 3 12 13 22 10 lsppr0 ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 , 0 } ) = ( 𝑁 ‘ { 𝑌 } ) )
43 41 42 sylan9eqr ⊢ ( ( 𝜑 ∧ 𝑋 = 0 ) → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) = ( 𝑁 ‘ { 𝑌 } ) )
44 3 21 13 22 35 10 lspprcl ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝐸 , 𝑌 } ) ∈ ( LSubSp ‘ 𝑈 ) )
45 3 13 22 35 10 lspprid2 ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑁 ‘ { 𝐸 , 𝑌 } ) )
46 21 13 22 44 45 lspsnel5a ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ⊆ ( 𝑁 ‘ { 𝐸 , 𝑌 } ) )
47 46 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = 0 ) → ( 𝑁 ‘ { 𝑌 } ) ⊆ ( 𝑁 ‘ { 𝐸 , 𝑌 } ) )
48 43 47 eqsstrd ⊢ ( ( 𝜑 ∧ 𝑋 = 0 ) → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ⊆ ( 𝑁 ‘ { 𝐸 , 𝑌 } ) )
49 48 ssneld ⊢ ( ( 𝜑 ∧ 𝑋 = 0 ) → ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝐸 , 𝑌 } ) → ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) )
50 3 13 22 35 10 lspprid1 ⊢ ( 𝜑 → 𝐸 ∈ ( 𝑁 ‘ { 𝐸 , 𝑌 } ) )
51 21 13 22 44 50 lspsnel5a ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝐸 } ) ⊆ ( 𝑁 ‘ { 𝐸 , 𝑌 } ) )
52 51 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = 0 ) → ( 𝑁 ‘ { 𝐸 } ) ⊆ ( 𝑁 ‘ { 𝐸 , 𝑌 } ) )
53 52 ssneld ⊢ ( ( 𝜑 ∧ 𝑋 = 0 ) → ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝐸 , 𝑌 } ) → ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝐸 } ) ) )
54 49 53 jcad ⊢ ( ( 𝜑 ∧ 𝑋 = 0 ) → ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝐸 , 𝑌 } ) → ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝐸 } ) ) ) )
55 54 reximdv ⊢ ( ( 𝜑 ∧ 𝑋 = 0 ) → ( ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝐸 , 𝑌 } ) → ∃ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝐸 } ) ) ) )
56 37 55 mpd ⊢ ( ( 𝜑 ∧ 𝑋 = 0 ) → ∃ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝐸 } ) ) )
57 56 adantlr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐸 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑋 = 0 ) → ∃ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝐸 } ) ) )
58 3 4 lmodvacl ⊢ ( ( 𝑈 ∈ LMod ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) → ( 𝐸 + 𝑋 ) ∈ 𝑉 )
59 22 35 9 58 syl3anc ⊢ ( 𝜑 → ( 𝐸 + 𝑋 ) ∈ 𝑉 )
60 59 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐸 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑋 ≠ 0 ) → ( 𝐸 + 𝑋 ) ∈ 𝑉 )
61 22 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐸 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑋 ≠ 0 ) → 𝑈 ∈ LMod )
62 24 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐸 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑋 ≠ 0 ) → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∈ ( LSubSp ‘ 𝑈 ) )
63 3 13 22 9 10 lspprid1 ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
64 63 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐸 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑋 ≠ 0 ) → 𝑋 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
65 35 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐸 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑋 ≠ 0 ) → 𝐸 ∈ 𝑉 )
66 simplr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐸 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑋 ≠ 0 ) → ¬ 𝐸 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
67 3 4 21 61 62 64 65 66 lssvancl2 ⊢ ( ( ( 𝜑 ∧ ¬ 𝐸 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑋 ≠ 0 ) → ¬ ( 𝐸 + 𝑋 ) ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
68 3 21 13 lspsncl ⊢ ( ( 𝑈 ∈ LMod ∧ 𝐸 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝐸 } ) ∈ ( LSubSp ‘ 𝑈 ) )
69 22 35 68 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝐸 } ) ∈ ( LSubSp ‘ 𝑈 ) )
70 69 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐸 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑋 ≠ 0 ) → ( 𝑁 ‘ { 𝐸 } ) ∈ ( LSubSp ‘ 𝑈 ) )
71 3 13 lspsnid ⊢ ( ( 𝑈 ∈ LMod ∧ 𝐸 ∈ 𝑉 ) → 𝐸 ∈ ( 𝑁 ‘ { 𝐸 } ) )
72 22 35 71 syl2anc ⊢ ( 𝜑 → 𝐸 ∈ ( 𝑁 ‘ { 𝐸 } ) )
73 72 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐸 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑋 ≠ 0 ) → 𝐸 ∈ ( 𝑁 ‘ { 𝐸 } ) )
74 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐸 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑋 ≠ 0 ) → 𝑋 ∈ 𝑉 )
75 1 2 8 dvhlvec ⊢ ( 𝜑 → 𝑈 ∈ LVec )
76 75 ad2antrr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐸 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑋 ≠ 0 ) → 𝑈 ∈ LVec )
77 simpr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐸 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑋 ≠ 0 ) → 𝑋 ≠ 0 )
78 eldifsn ⊢ ( 𝑋 ∈ ( 𝑉 ∖ { 0 } ) ↔ ( 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) )
79 74 77 78 sylanbrc ⊢ ( ( ( 𝜑 ∧ ¬ 𝐸 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑋 ≠ 0 ) → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
80 21 13 22 24 63 lspsnel5a ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ⊆ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
81 80 sseld ⊢ ( 𝜑 → ( 𝐸 ∈ ( 𝑁 ‘ { 𝑋 } ) → 𝐸 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) )
82 81 con3dimp ⊢ ( ( 𝜑 ∧ ¬ 𝐸 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) → ¬ 𝐸 ∈ ( 𝑁 ‘ { 𝑋 } ) )
83 82 adantr ⊢ ( ( ( 𝜑 ∧ ¬ 𝐸 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑋 ≠ 0 ) → ¬ 𝐸 ∈ ( 𝑁 ‘ { 𝑋 } ) )
84 3 12 13 76 65 79 83 lspsnnecom ⊢ ( ( ( 𝜑 ∧ ¬ 𝐸 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑋 ≠ 0 ) → ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝐸 } ) )
85 3 4 21 61 70 73 74 84 lssvancl1 ⊢ ( ( ( 𝜑 ∧ ¬ 𝐸 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑋 ≠ 0 ) → ¬ ( 𝐸 + 𝑋 ) ∈ ( 𝑁 ‘ { 𝐸 } ) )
86 eleq1 ⊢ ( 𝑧 = ( 𝐸 + 𝑋 ) → ( 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ↔ ( 𝐸 + 𝑋 ) ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) )
87 86 notbid ⊢ ( 𝑧 = ( 𝐸 + 𝑋 ) → ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ↔ ¬ ( 𝐸 + 𝑋 ) ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) )
88 eleq1 ⊢ ( 𝑧 = ( 𝐸 + 𝑋 ) → ( 𝑧 ∈ ( 𝑁 ‘ { 𝐸 } ) ↔ ( 𝐸 + 𝑋 ) ∈ ( 𝑁 ‘ { 𝐸 } ) ) )
89 88 notbid ⊢ ( 𝑧 = ( 𝐸 + 𝑋 ) → ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝐸 } ) ↔ ¬ ( 𝐸 + 𝑋 ) ∈ ( 𝑁 ‘ { 𝐸 } ) ) )
90 87 89 anbi12d ⊢ ( 𝑧 = ( 𝐸 + 𝑋 ) → ( ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝐸 } ) ) ↔ ( ¬ ( 𝐸 + 𝑋 ) ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ ( 𝐸 + 𝑋 ) ∈ ( 𝑁 ‘ { 𝐸 } ) ) ) )
91 90 rspcev ⊢ ( ( ( 𝐸 + 𝑋 ) ∈ 𝑉 ∧ ( ¬ ( 𝐸 + 𝑋 ) ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ ( 𝐸 + 𝑋 ) ∈ ( 𝑁 ‘ { 𝐸 } ) ) ) → ∃ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝐸 } ) ) )
92 60 67 85 91 syl12anc ⊢ ( ( ( 𝜑 ∧ ¬ 𝐸 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑋 ≠ 0 ) → ∃ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝐸 } ) ) )
93 57 92 pm2.61dane ⊢ ( ( 𝜑 ∧ ¬ 𝐸 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) → ∃ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝐸 } ) ) )
94 31 93 pm2.61dan ⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝐸 } ) ) )
95 8 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑉 ∧ ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝐸 } ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
96 9 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑉 ∧ ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝐸 } ) ) ) → 𝑋 ∈ 𝑉 )
97 10 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑉 ∧ ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝐸 } ) ) ) → 𝑌 ∈ 𝑉 )
98 simp2 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑉 ∧ ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝐸 } ) ) ) → 𝑧 ∈ 𝑉 )
99 simp3l ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑉 ∧ ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝐸 } ) ) ) → ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
100 22 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑉 ∧ ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝐸 } ) ) ) → 𝑈 ∈ LMod )
101 35 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑉 ∧ ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝐸 } ) ) ) → 𝐸 ∈ 𝑉 )
102 simp3r ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑉 ∧ ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝐸 } ) ) ) → ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝐸 } ) )
103 3 13 100 98 101 102 lspsnne2 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑉 ∧ ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝐸 } ) ) ) → ( 𝑁 ‘ { 𝑧 } ) ≠ ( 𝑁 ‘ { 𝐸 } ) )
104 1 2 3 4 5 6 7 95 96 97 11 12 13 14 15 16 17 18 98 99 103 hdmap11lem1 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑉 ∧ ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝐸 } ) ) ) → ( 𝑆 ‘ ( 𝑋 + 𝑌 ) ) = ( ( 𝑆 ‘ 𝑋 ) ✚ ( 𝑆 ‘ 𝑌 ) ) )
105 104 rexlimdv3a ⊢ ( 𝜑 → ( ∃ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝐸 } ) ) → ( 𝑆 ‘ ( 𝑋 + 𝑌 ) ) = ( ( 𝑆 ‘ 𝑋 ) ✚ ( 𝑆 ‘ 𝑌 ) ) ) )
106 94 105 mpd ⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝑋 + 𝑌 ) ) = ( ( 𝑆 ‘ 𝑋 ) ✚ ( 𝑆 ‘ 𝑌 ) ) )