Metamath Proof Explorer

Theorem dvh3dim3N

Description: There is a vector that is outside of 2 spans. TODO: decide to use either this or dvh3dim2 everywhere. If this one is needed, make dvh3dim2 into a lemma. (Contributed by NM, 21-May-2015) (New usage is discouraged.)

Ref Expression
Hypotheses dvh3dim.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
dvh3dim.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
dvh3dim.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
dvh3dim.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
dvh3dim.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
dvh3dim.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
dvh3dim.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
dvh3dim2.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
dvh3dim3.t ⊢ ( 𝜑 → 𝑇 ∈ 𝑉 )
Assertion dvh3dim3N ( 𝜑 → ∃ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) )

Proof

Step Hyp Ref Expression
1 dvh3dim.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 dvh3dim.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 dvh3dim.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
4 dvh3dim.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
5 dvh3dim.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
6 dvh3dim.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
7 dvh3dim.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
8 dvh3dim2.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
9 dvh3dim3.t ⊢ ( 𝜑 → 𝑇 ∈ 𝑉 )
10 eqid ⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
11 1 2 5 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
12 11 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) → 𝑈 ∈ LMod )
13 3 10 4 11 8 9 lspprcl ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ∈ ( LSubSp ‘ 𝑈 ) )
14 13 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) → ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ∈ ( LSubSp ‘ 𝑈 ) )
15 simpr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) → 𝑌 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) )
16 3 4 11 8 9 lspprid2 ⊢ ( 𝜑 → 𝑇 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) )
17 16 adantr ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) → 𝑇 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) )
18 10 4 12 14 15 17 lspprss ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) → ( 𝑁 ‘ { 𝑌 , 𝑇 } ) ⊆ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) )
19 sspss ⊢ ( ( 𝑁 ‘ { 𝑌 , 𝑇 } ) ⊆ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ↔ ( ( 𝑁 ‘ { 𝑌 , 𝑇 } ) ⊊ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ∨ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) = ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) )
20 18 19 sylib ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) → ( ( 𝑁 ‘ { 𝑌 , 𝑇 } ) ⊊ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ∨ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) = ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) )
21 1 2 5 dvhlvec ⊢ ( 𝜑 → 𝑈 ∈ LVec )
22 21 adantr ⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) ⊊ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) → 𝑈 ∈ LVec )
23 3 10 4 11 7 9 lspprcl ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 , 𝑇 } ) ∈ ( LSubSp ‘ 𝑈 ) )
24 23 adantr ⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) ⊊ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) → ( 𝑁 ‘ { 𝑌 , 𝑇 } ) ∈ ( LSubSp ‘ 𝑈 ) )
25 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) ⊊ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) → 𝑍 ∈ 𝑉 )
26 9 adantr ⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) ⊊ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) → 𝑇 ∈ 𝑉 )
27 simpr ⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) ⊊ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) → ( 𝑁 ‘ { 𝑌 , 𝑇 } ) ⊊ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) )
28 3 10 4 22 24 25 26 27 lspprat ⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) ⊊ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) → ∃ 𝑤 ∈ 𝑉 ( 𝑁 ‘ { 𝑌 , 𝑇 } ) = ( 𝑁 ‘ { 𝑤 } ) )
29 5 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑉 ∧ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) = ( 𝑁 ‘ { 𝑤 } ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
30 simp2 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑉 ∧ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) = ( 𝑁 ‘ { 𝑤 } ) ) → 𝑤 ∈ 𝑉 )
31 6 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑉 ∧ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) = ( 𝑁 ‘ { 𝑤 } ) ) → 𝑋 ∈ 𝑉 )
32 8 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑉 ∧ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) = ( 𝑁 ‘ { 𝑤 } ) ) → 𝑍 ∈ 𝑉 )
33 1 2 3 4 29 30 31 32 dvh3dim2 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑉 ∧ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) = ( 𝑁 ‘ { 𝑤 } ) ) → ∃ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑤 , 𝑋 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑤 , 𝑍 } ) ) )
34 11 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑉 ∧ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) = ( 𝑁 ‘ { 𝑤 } ) ) → 𝑈 ∈ LMod )
35 10 lsssssubg ⊢ ( 𝑈 ∈ LMod → ( LSubSp ‘ 𝑈 ) ⊆ ( SubGrp ‘ 𝑈 ) )
36 34 35 syl ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑉 ∧ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) = ( 𝑁 ‘ { 𝑤 } ) ) → ( LSubSp ‘ 𝑈 ) ⊆ ( SubGrp ‘ 𝑈 ) )
37 3 10 4 lspsncl ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑈 ) )
38 11 6 37 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑈 ) )
39 38 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑉 ∧ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) = ( 𝑁 ‘ { 𝑤 } ) ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ( LSubSp ‘ 𝑈 ) )
40 36 39 sseldd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑉 ∧ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) = ( 𝑁 ‘ { 𝑤 } ) ) → ( 𝑁 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝑈 ) )
41 3 10 4 lspsncl ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑤 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑤 } ) ∈ ( LSubSp ‘ 𝑈 ) )
42 34 30 41 syl2anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑉 ∧ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) = ( 𝑁 ‘ { 𝑤 } ) ) → ( 𝑁 ‘ { 𝑤 } ) ∈ ( LSubSp ‘ 𝑈 ) )
43 36 42 sseldd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑉 ∧ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) = ( 𝑁 ‘ { 𝑤 } ) ) → ( 𝑁 ‘ { 𝑤 } ) ∈ ( SubGrp ‘ 𝑈 ) )
44 prssi ⊢ ( ( 𝑌 ∈ 𝑉 ∧ 𝑇 ∈ 𝑉 ) → { 𝑌 , 𝑇 } ⊆ 𝑉 )
45 7 9 44 syl2anc ⊢ ( 𝜑 → { 𝑌 , 𝑇 } ⊆ 𝑉 )
46 snsspr1 ⊢ { 𝑌 } ⊆ { 𝑌 , 𝑇 }
47 46 a1i ⊢ ( 𝜑 → { 𝑌 } ⊆ { 𝑌 , 𝑇 } )
48 3 4 lspss ⊢ ( ( 𝑈 ∈ LMod ∧ { 𝑌 , 𝑇 } ⊆ 𝑉 ∧ { 𝑌 } ⊆ { 𝑌 , 𝑇 } ) → ( 𝑁 ‘ { 𝑌 } ) ⊆ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) )
49 11 45 47 48 syl3anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ⊆ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) )
50 49 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑉 ∧ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) = ( 𝑁 ‘ { 𝑤 } ) ) → ( 𝑁 ‘ { 𝑌 } ) ⊆ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) )
51 simp3 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑉 ∧ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) = ( 𝑁 ‘ { 𝑤 } ) ) → ( 𝑁 ‘ { 𝑌 , 𝑇 } ) = ( 𝑁 ‘ { 𝑤 } ) )
52 50 51 sseqtrd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑉 ∧ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) = ( 𝑁 ‘ { 𝑤 } ) ) → ( 𝑁 ‘ { 𝑌 } ) ⊆ ( 𝑁 ‘ { 𝑤 } ) )
53 eqid ⊢ ( LSSum ‘ 𝑈 ) = ( LSSum ‘ 𝑈 )
54 53 lsmless2 ⊢ ( ( ( 𝑁 ‘ { 𝑋 } ) ∈ ( SubGrp ‘ 𝑈 ) ∧ ( 𝑁 ‘ { 𝑤 } ) ∈ ( SubGrp ‘ 𝑈 ) ∧ ( 𝑁 ‘ { 𝑌 } ) ⊆ ( 𝑁 ‘ { 𝑤 } ) ) → ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑌 } ) ) ⊆ ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑤 } ) ) )
55 40 43 52 54 syl3anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑉 ∧ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) = ( 𝑁 ‘ { 𝑤 } ) ) → ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑌 } ) ) ⊆ ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑤 } ) ) )
56 3 4 53 11 6 7 lsmpr ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) = ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑌 } ) ) )
57 56 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑉 ∧ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) = ( 𝑁 ‘ { 𝑤 } ) ) → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) = ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑌 } ) ) )
58 prcom ⊢ { 𝑤 , 𝑋 } = { 𝑋 , 𝑤 }
59 58 fveq2i ⊢ ( 𝑁 ‘ { 𝑤 , 𝑋 } ) = ( 𝑁 ‘ { 𝑋 , 𝑤 } )
60 3 4 53 34 31 30 lsmpr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑉 ∧ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) = ( 𝑁 ‘ { 𝑤 } ) ) → ( 𝑁 ‘ { 𝑋 , 𝑤 } ) = ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑤 } ) ) )
61 59 60 syl5eq ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑉 ∧ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) = ( 𝑁 ‘ { 𝑤 } ) ) → ( 𝑁 ‘ { 𝑤 , 𝑋 } ) = ( ( 𝑁 ‘ { 𝑋 } ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑤 } ) ) )
62 55 57 61 3sstr4d ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑉 ∧ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) = ( 𝑁 ‘ { 𝑤 } ) ) → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ⊆ ( 𝑁 ‘ { 𝑤 , 𝑋 } ) )
63 62 ssneld ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑉 ∧ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) = ( 𝑁 ‘ { 𝑤 } ) ) → ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑤 , 𝑋 } ) → ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) )
64 3 10 4 lspsncl ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑍 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑍 } ) ∈ ( LSubSp ‘ 𝑈 ) )
65 11 8 64 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑍 } ) ∈ ( LSubSp ‘ 𝑈 ) )
66 65 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑉 ∧ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) = ( 𝑁 ‘ { 𝑤 } ) ) → ( 𝑁 ‘ { 𝑍 } ) ∈ ( LSubSp ‘ 𝑈 ) )
67 36 66 sseldd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑉 ∧ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) = ( 𝑁 ‘ { 𝑤 } ) ) → ( 𝑁 ‘ { 𝑍 } ) ∈ ( SubGrp ‘ 𝑈 ) )
68 snsspr2 ⊢ { 𝑇 } ⊆ { 𝑌 , 𝑇 }
69 68 a1i ⊢ ( 𝜑 → { 𝑇 } ⊆ { 𝑌 , 𝑇 } )
70 3 4 lspss ⊢ ( ( 𝑈 ∈ LMod ∧ { 𝑌 , 𝑇 } ⊆ 𝑉 ∧ { 𝑇 } ⊆ { 𝑌 , 𝑇 } ) → ( 𝑁 ‘ { 𝑇 } ) ⊆ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) )
71 11 45 69 70 syl3anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑇 } ) ⊆ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) )
72 71 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑉 ∧ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) = ( 𝑁 ‘ { 𝑤 } ) ) → ( 𝑁 ‘ { 𝑇 } ) ⊆ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) )
73 72 51 sseqtrd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑉 ∧ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) = ( 𝑁 ‘ { 𝑤 } ) ) → ( 𝑁 ‘ { 𝑇 } ) ⊆ ( 𝑁 ‘ { 𝑤 } ) )
74 53 lsmless2 ⊢ ( ( ( 𝑁 ‘ { 𝑍 } ) ∈ ( SubGrp ‘ 𝑈 ) ∧ ( 𝑁 ‘ { 𝑤 } ) ∈ ( SubGrp ‘ 𝑈 ) ∧ ( 𝑁 ‘ { 𝑇 } ) ⊆ ( 𝑁 ‘ { 𝑤 } ) ) → ( ( 𝑁 ‘ { 𝑍 } ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑇 } ) ) ⊆ ( ( 𝑁 ‘ { 𝑍 } ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑤 } ) ) )
75 67 43 73 74 syl3anc ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑉 ∧ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) = ( 𝑁 ‘ { 𝑤 } ) ) → ( ( 𝑁 ‘ { 𝑍 } ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑇 } ) ) ⊆ ( ( 𝑁 ‘ { 𝑍 } ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑤 } ) ) )
76 3 4 53 11 8 9 lsmpr ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑍 , 𝑇 } ) = ( ( 𝑁 ‘ { 𝑍 } ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑇 } ) ) )
77 76 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑉 ∧ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) = ( 𝑁 ‘ { 𝑤 } ) ) → ( 𝑁 ‘ { 𝑍 , 𝑇 } ) = ( ( 𝑁 ‘ { 𝑍 } ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑇 } ) ) )
78 prcom ⊢ { 𝑤 , 𝑍 } = { 𝑍 , 𝑤 }
79 78 fveq2i ⊢ ( 𝑁 ‘ { 𝑤 , 𝑍 } ) = ( 𝑁 ‘ { 𝑍 , 𝑤 } )
80 3 4 53 34 32 30 lsmpr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑉 ∧ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) = ( 𝑁 ‘ { 𝑤 } ) ) → ( 𝑁 ‘ { 𝑍 , 𝑤 } ) = ( ( 𝑁 ‘ { 𝑍 } ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑤 } ) ) )
81 79 80 syl5eq ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑉 ∧ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) = ( 𝑁 ‘ { 𝑤 } ) ) → ( 𝑁 ‘ { 𝑤 , 𝑍 } ) = ( ( 𝑁 ‘ { 𝑍 } ) ( LSSum ‘ 𝑈 ) ( 𝑁 ‘ { 𝑤 } ) ) )
82 75 77 81 3sstr4d ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑉 ∧ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) = ( 𝑁 ‘ { 𝑤 } ) ) → ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ⊆ ( 𝑁 ‘ { 𝑤 , 𝑍 } ) )
83 82 ssneld ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑉 ∧ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) = ( 𝑁 ‘ { 𝑤 } ) ) → ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑤 , 𝑍 } ) → ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) )
84 63 83 anim12d ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑉 ∧ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) = ( 𝑁 ‘ { 𝑤 } ) ) → ( ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑤 , 𝑋 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑤 , 𝑍 } ) ) → ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) ) )
85 84 reximdv ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑉 ∧ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) = ( 𝑁 ‘ { 𝑤 } ) ) → ( ∃ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑤 , 𝑋 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑤 , 𝑍 } ) ) → ∃ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) ) )
86 33 85 mpd ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑉 ∧ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) = ( 𝑁 ‘ { 𝑤 } ) ) → ∃ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) )
87 86 rexlimdv3a ⊢ ( 𝜑 → ( ∃ 𝑤 ∈ 𝑉 ( 𝑁 ‘ { 𝑌 , 𝑇 } ) = ( 𝑁 ‘ { 𝑤 } ) → ∃ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) ) )
88 87 adantr ⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) ⊊ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) → ( ∃ 𝑤 ∈ 𝑉 ( 𝑁 ‘ { 𝑌 , 𝑇 } ) = ( 𝑁 ‘ { 𝑤 } ) → ∃ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) ) )
89 28 88 mpd ⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) ⊊ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) → ∃ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) )
90 1 2 3 4 5 7 6 9 dvh3dim2 ⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) ) )
91 90 adantr ⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) = ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) → ∃ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) ) )
92 simpr ⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) = ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) → ( 𝑁 ‘ { 𝑌 , 𝑇 } ) = ( 𝑁 ‘ { 𝑍 , 𝑇 } ) )
93 prcom ⊢ { 𝑌 , 𝑋 } = { 𝑋 , 𝑌 }
94 93 fveq2i ⊢ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) = ( 𝑁 ‘ { 𝑋 , 𝑌 } )
95 94 eleq2i ⊢ ( 𝑧 ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ↔ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
96 95 notbii ⊢ ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ↔ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
97 96 a1i ⊢ ( ( 𝑁 ‘ { 𝑌 , 𝑇 } ) = ( 𝑁 ‘ { 𝑍 , 𝑇 } ) → ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ↔ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) )
98 eleq2 ⊢ ( ( 𝑁 ‘ { 𝑌 , 𝑇 } ) = ( 𝑁 ‘ { 𝑍 , 𝑇 } ) → ( 𝑧 ∈ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) ↔ 𝑧 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) )
99 98 notbid ⊢ ( ( 𝑁 ‘ { 𝑌 , 𝑇 } ) = ( 𝑁 ‘ { 𝑍 , 𝑇 } ) → ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) ↔ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) )
100 97 99 anbi12d ⊢ ( ( 𝑁 ‘ { 𝑌 , 𝑇 } ) = ( 𝑁 ‘ { 𝑍 , 𝑇 } ) → ( ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) ) ↔ ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) ) )
101 92 100 syl ⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) = ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) → ( ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) ) ↔ ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) ) )
102 101 rexbidv ⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) = ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) → ( ∃ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) ) ↔ ∃ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) ) )
103 91 102 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) = ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) → ∃ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) )
104 89 103 jaodan ⊢ ( ( 𝜑 ∧ ( ( 𝑁 ‘ { 𝑌 , 𝑇 } ) ⊊ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ∨ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) = ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) ) → ∃ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) )
105 20 104 syldan ⊢ ( ( 𝜑 ∧ 𝑌 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) → ∃ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) )
106 1 2 3 4 5 7 6 9 dvh3dim2 ⊢ ( 𝜑 → ∃ 𝑤 ∈ 𝑉 ( ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ∧ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) ) )
107 106 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) → ∃ 𝑤 ∈ 𝑉 ( ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ∧ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) ) )
108 simpl1l ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) ∧ 𝑤 ∈ 𝑉 ∧ ( ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ∧ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) ) ) ∧ 𝑤 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) → 𝜑 )
109 108 11 syl ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) ∧ 𝑤 ∈ 𝑉 ∧ ( ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ∧ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) ) ) ∧ 𝑤 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) → 𝑈 ∈ LMod )
110 simpl2 ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) ∧ 𝑤 ∈ 𝑉 ∧ ( ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ∧ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) ) ) ∧ 𝑤 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) → 𝑤 ∈ 𝑉 )
111 108 7 syl ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) ∧ 𝑤 ∈ 𝑉 ∧ ( ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ∧ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) ) ) ∧ 𝑤 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) → 𝑌 ∈ 𝑉 )
112 eqid ⊢ ( +g ‘ 𝑈 ) = ( +g ‘ 𝑈 )
113 3 112 lmodvacl ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑤 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉 ) → ( 𝑤 ( +g ‘ 𝑈 ) 𝑌 ) ∈ 𝑉 )
114 109 110 111 113 syl3anc ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) ∧ 𝑤 ∈ 𝑉 ∧ ( ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ∧ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) ) ) ∧ 𝑤 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) → ( 𝑤 ( +g ‘ 𝑈 ) 𝑌 ) ∈ 𝑉 )
115 3 10 4 11 6 7 lspprcl ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∈ ( LSubSp ‘ 𝑈 ) )
116 108 115 syl ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) ∧ 𝑤 ∈ 𝑉 ∧ ( ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ∧ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) ) ) ∧ 𝑤 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∈ ( LSubSp ‘ 𝑈 ) )
117 3 4 11 6 7 lspprid2 ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
118 108 117 syl ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) ∧ 𝑤 ∈ 𝑉 ∧ ( ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ∧ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) ) ) ∧ 𝑤 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) → 𝑌 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
119 simpl3l ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) ∧ 𝑤 ∈ 𝑉 ∧ ( ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ∧ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) ) ) ∧ 𝑤 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) → ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) )
120 94 eleq2i ⊢ ( 𝑤 ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ↔ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
121 119 120 sylnib ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) ∧ 𝑤 ∈ 𝑉 ∧ ( ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ∧ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) ) ) ∧ 𝑤 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) → ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
122 3 112 10 109 116 118 110 121 lssvancl2 ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) ∧ 𝑤 ∈ 𝑉 ∧ ( ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ∧ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) ) ) ∧ 𝑤 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) → ¬ ( 𝑤 ( +g ‘ 𝑈 ) 𝑌 ) ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
123 108 13 syl ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) ∧ 𝑤 ∈ 𝑉 ∧ ( ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ∧ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) ) ) ∧ 𝑤 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) → ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ∈ ( LSubSp ‘ 𝑈 ) )
124 simpr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) ∧ 𝑤 ∈ 𝑉 ∧ ( ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ∧ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) ) ) ∧ 𝑤 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) → 𝑤 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) )
125 simpl1r ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) ∧ 𝑤 ∈ 𝑉 ∧ ( ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ∧ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) ) ) ∧ 𝑤 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) → ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) )
126 3 112 10 109 123 124 111 125 lssvancl1 ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) ∧ 𝑤 ∈ 𝑉 ∧ ( ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ∧ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) ) ) ∧ 𝑤 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) → ¬ ( 𝑤 ( +g ‘ 𝑈 ) 𝑌 ) ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) )
127 eleq1 ⊢ ( 𝑧 = ( 𝑤 ( +g ‘ 𝑈 ) 𝑌 ) → ( 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ↔ ( 𝑤 ( +g ‘ 𝑈 ) 𝑌 ) ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) )
128 127 notbid ⊢ ( 𝑧 = ( 𝑤 ( +g ‘ 𝑈 ) 𝑌 ) → ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ↔ ¬ ( 𝑤 ( +g ‘ 𝑈 ) 𝑌 ) ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) )
129 eleq1 ⊢ ( 𝑧 = ( 𝑤 ( +g ‘ 𝑈 ) 𝑌 ) → ( 𝑧 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ↔ ( 𝑤 ( +g ‘ 𝑈 ) 𝑌 ) ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) )
130 129 notbid ⊢ ( 𝑧 = ( 𝑤 ( +g ‘ 𝑈 ) 𝑌 ) → ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ↔ ¬ ( 𝑤 ( +g ‘ 𝑈 ) 𝑌 ) ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) )
131 128 130 anbi12d ⊢ ( 𝑧 = ( 𝑤 ( +g ‘ 𝑈 ) 𝑌 ) → ( ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) ↔ ( ¬ ( 𝑤 ( +g ‘ 𝑈 ) 𝑌 ) ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ ( 𝑤 ( +g ‘ 𝑈 ) 𝑌 ) ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) ) )
132 131 rspcev ⊢ ( ( ( 𝑤 ( +g ‘ 𝑈 ) 𝑌 ) ∈ 𝑉 ∧ ( ¬ ( 𝑤 ( +g ‘ 𝑈 ) 𝑌 ) ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ ( 𝑤 ( +g ‘ 𝑈 ) 𝑌 ) ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) ) → ∃ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) )
133 114 122 126 132 syl12anc ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) ∧ 𝑤 ∈ 𝑉 ∧ ( ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ∧ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) ) ) ∧ 𝑤 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) → ∃ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) )
134 simpl2 ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) ∧ 𝑤 ∈ 𝑉 ∧ ( ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ∧ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) ) ) ∧ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) → 𝑤 ∈ 𝑉 )
135 simpl3l ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) ∧ 𝑤 ∈ 𝑉 ∧ ( ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ∧ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) ) ) ∧ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) → ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) )
136 135 120 sylnib ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) ∧ 𝑤 ∈ 𝑉 ∧ ( ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ∧ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) ) ) ∧ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) → ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
137 simpr ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) ∧ 𝑤 ∈ 𝑉 ∧ ( ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ∧ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) ) ) ∧ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) → ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) )
138 eleq1 ⊢ ( 𝑧 = 𝑤 → ( 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ↔ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) )
139 138 notbid ⊢ ( 𝑧 = 𝑤 → ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ↔ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) )
140 eleq1 ⊢ ( 𝑧 = 𝑤 → ( 𝑧 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ↔ 𝑤 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) )
141 140 notbid ⊢ ( 𝑧 = 𝑤 → ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ↔ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) )
142 139 141 anbi12d ⊢ ( 𝑧 = 𝑤 → ( ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) ↔ ( ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) ) )
143 142 rspcev ⊢ ( ( 𝑤 ∈ 𝑉 ∧ ( ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) ) → ∃ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) )
144 134 136 137 143 syl12anc ⊢ ( ( ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) ∧ 𝑤 ∈ 𝑉 ∧ ( ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ∧ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) ) ) ∧ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) → ∃ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) )
145 133 144 pm2.61dan ⊢ ( ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) ∧ 𝑤 ∈ 𝑉 ∧ ( ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ∧ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) ) ) → ∃ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) )
146 145 rexlimdv3a ⊢ ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) → ( ∃ 𝑤 ∈ 𝑉 ( ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 , 𝑋 } ) ∧ ¬ 𝑤 ∈ ( 𝑁 ‘ { 𝑌 , 𝑇 } ) ) → ∃ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) ) )
147 107 146 mpd ⊢ ( ( 𝜑 ∧ ¬ 𝑌 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) → ∃ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) )
148 105 147 pm2.61dan ⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝑉 ( ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑍 , 𝑇 } ) ) )