Metamath Proof Explorer

Theorem lspfixed

Description: Show membership in the span of the sum of two vectors, one of which ( Y ) is fixed in advance. (Contributed by NM, 27-May-2015) (Revised by AV, 12-Jul-2022)

Ref Expression
Hypotheses lspfixed.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lspfixed.p ⊢ + = ( +g ‘ 𝑊 )
lspfixed.o ⊢ 0 = ( 0g ‘ 𝑊 )
lspfixed.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
lspfixed.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
lspfixed.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
lspfixed.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
lspfixed.e ⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) )
lspfixed.f ⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑍 } ) )
lspfixed.g ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) )
Assertion lspfixed ( 𝜑 → ∃ 𝑧 ∈ ( ( 𝑁 ‘ { 𝑍 } ) ∖ { 0 } ) 𝑋 ∈ ( 𝑁 ‘ { ( 𝑌 + 𝑧 ) } ) )

Proof

Step Hyp Ref Expression
1 lspfixed.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lspfixed.p ⊢ + = ( +g ‘ 𝑊 )
3 lspfixed.o ⊢ 0 = ( 0g ‘ 𝑊 )
4 lspfixed.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
5 lspfixed.w ⊢ ( 𝜑 → 𝑊 ∈ LVec )
6 lspfixed.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
7 lspfixed.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑉 )
8 lspfixed.e ⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) )
9 lspfixed.f ⊢ ( 𝜑 → ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑍 } ) )
10 lspfixed.g ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) )
11 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
12 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
13 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
14 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
15 5 14 syl ⊢ ( 𝜑 → 𝑊 ∈ LMod )
16 1 2 11 12 13 4 15 6 7 lspprel ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) ↔ ∃ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) )
17 10 16 mpbid ⊢ ( 𝜑 → ∃ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) )
18 15 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → 𝑊 ∈ LMod )
19 eqid ⊢ ( LSubSp ‘ 𝑊 ) = ( LSubSp ‘ 𝑊 )
20 1 19 4 lspsncl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑍 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑍 } ) ∈ ( LSubSp ‘ 𝑊 ) )
21 15 7 20 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑍 } ) ∈ ( LSubSp ‘ 𝑊 ) )
22 21 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( 𝑁 ‘ { 𝑍 } ) ∈ ( LSubSp ‘ 𝑊 ) )
23 5 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → 𝑊 ∈ LVec )
24 11 lvecdrng ⊢ ( 𝑊 ∈ LVec → ( Scalar ‘ 𝑊 ) ∈ DivRing )
25 23 24 syl ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( Scalar ‘ 𝑊 ) ∈ DivRing )
26 simp2l ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
27 9 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑍 } ) )
28 simpl3 ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) ∧ 𝑘 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) )
29 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) ∧ 𝑘 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → 𝑘 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
30 29 oveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) ∧ 𝑘 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) = ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) )
31 simpl1 ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) ∧ 𝑘 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → 𝜑 )
32 31 15 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) ∧ 𝑘 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → 𝑊 ∈ LMod )
33 31 6 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) ∧ 𝑘 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → 𝑌 ∈ 𝑉 )
34 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
35 1 11 13 34 3 lmod0vs ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) → ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) = 0 )
36 32 33 35 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) ∧ 𝑘 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) = 0 )
37 30 36 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) ∧ 𝑘 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) = 0 )
38 37 oveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) ∧ 𝑘 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) = ( 0 + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) )
39 simp2r ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
40 7 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → 𝑍 ∈ 𝑉 )
41 1 11 13 12 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑍 ∈ 𝑉 ) → ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ∈ 𝑉 )
42 18 39 40 41 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ∈ 𝑉 )
43 42 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) ∧ 𝑘 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ∈ 𝑉 )
44 1 2 3 lmod0vlid ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ∈ 𝑉 ) → ( 0 + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) )
45 32 43 44 syl2anc ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) ∧ 𝑘 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → ( 0 + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) )
46 28 38 45 3eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) ∧ 𝑘 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → 𝑋 = ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) )
47 31 21 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) ∧ 𝑘 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → ( 𝑁 ‘ { 𝑍 } ) ∈ ( LSubSp ‘ 𝑊 ) )
48 simpl2r ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) ∧ 𝑘 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
49 1 4 lspsnid ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑍 ∈ 𝑉 ) → 𝑍 ∈ ( 𝑁 ‘ { 𝑍 } ) )
50 15 7 49 syl2anc ⊢ ( 𝜑 → 𝑍 ∈ ( 𝑁 ‘ { 𝑍 } ) )
51 31 50 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) ∧ 𝑘 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → 𝑍 ∈ ( 𝑁 ‘ { 𝑍 } ) )
52 11 13 12 19 lssvscl ⊢ ( ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ { 𝑍 } ) ∈ ( LSubSp ‘ 𝑊 ) ) ∧ ( 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑍 ∈ ( 𝑁 ‘ { 𝑍 } ) ) ) → ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ∈ ( 𝑁 ‘ { 𝑍 } ) )
53 32 47 48 51 52 syl22anc ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) ∧ 𝑘 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ∈ ( 𝑁 ‘ { 𝑍 } ) )
54 46 53 eqeltrd ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) ∧ 𝑘 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → 𝑋 ∈ ( 𝑁 ‘ { 𝑍 } ) )
55 54 ex ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( 𝑘 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) → 𝑋 ∈ ( 𝑁 ‘ { 𝑍 } ) ) )
56 55 necon3bd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑍 } ) → 𝑘 ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
57 27 56 mpd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → 𝑘 ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
58 eqid ⊢ ( invr ‘ ( Scalar ‘ 𝑊 ) ) = ( invr ‘ ( Scalar ‘ 𝑊 ) )
59 12 34 58 drnginvrcl ⊢ ( ( ( Scalar ‘ 𝑊 ) ∈ DivRing ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
60 25 26 57 59 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
61 50 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → 𝑍 ∈ ( 𝑁 ‘ { 𝑍 } ) )
62 18 22 39 61 52 syl22anc ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ∈ ( 𝑁 ‘ { 𝑍 } ) )
63 11 13 12 19 lssvscl ⊢ ( ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ { 𝑍 } ) ∈ ( LSubSp ‘ 𝑊 ) ) ∧ ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ∈ ( 𝑁 ‘ { 𝑍 } ) ) ) → ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ∈ ( 𝑁 ‘ { 𝑍 } ) )
64 18 22 60 62 63 syl22anc ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ∈ ( 𝑁 ‘ { 𝑍 } ) )
65 12 34 58 drnginvrn0 ⊢ ( ( ( Scalar ‘ 𝑊 ) ∈ DivRing ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
66 25 26 57 65 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
67 8 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) )
68 simpl3 ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) ∧ 𝑙 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) )
69 oveq1 ⊢ ( 𝑙 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) → ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) = ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑍 ) )
70 1 11 13 34 3 lmod0vs ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑍 ∈ 𝑉 ) → ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑍 ) = 0 )
71 18 40 70 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑍 ) = 0 )
72 69 71 sylan9eqr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) ∧ 𝑙 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) = 0 )
73 72 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) ∧ 𝑙 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + 0 ) )
74 6 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → 𝑌 ∈ 𝑉 )
75 1 11 13 12 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑌 ∈ 𝑉 ) → ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ∈ 𝑉 )
76 18 26 74 75 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ∈ 𝑉 )
77 1 2 3 lmod0vrid ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ∈ 𝑉 ) → ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + 0 ) = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) )
78 18 76 77 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + 0 ) = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) )
79 78 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) ∧ 𝑙 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + 0 ) = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) )
80 68 73 79 3eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) ∧ 𝑙 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → 𝑋 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) )
81 1 19 4 lspsncl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) → ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑊 ) )
82 15 6 81 syl2anc ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑊 ) )
83 82 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑊 ) )
84 1 4 lspsnid ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) → 𝑌 ∈ ( 𝑁 ‘ { 𝑌 } ) )
85 15 6 84 syl2anc ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑁 ‘ { 𝑌 } ) )
86 85 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → 𝑌 ∈ ( 𝑁 ‘ { 𝑌 } ) )
87 11 13 12 19 lssvscl ⊢ ( ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ { 𝑌 } ) ∈ ( LSubSp ‘ 𝑊 ) ) ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑌 ∈ ( 𝑁 ‘ { 𝑌 } ) ) ) → ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ∈ ( 𝑁 ‘ { 𝑌 } ) )
88 18 83 26 86 87 syl22anc ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ∈ ( 𝑁 ‘ { 𝑌 } ) )
89 88 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) ∧ 𝑙 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ∈ ( 𝑁 ‘ { 𝑌 } ) )
90 80 89 eqeltrd ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) ∧ 𝑙 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) )
91 90 ex ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( 𝑙 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) → 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) ) )
92 91 necon3bd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) → 𝑙 ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
93 67 92 mpd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → 𝑙 ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
94 simpl1 ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) ∧ 𝑍 = 0 ) → 𝜑 )
95 94 10 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) ∧ 𝑍 = 0 ) → 𝑋 ∈ ( 𝑁 ‘ { 𝑌 , 𝑍 } ) )
96 preq2 ⊢ ( 𝑍 = 0 → { 𝑌 , 𝑍 } = { 𝑌 , 0 } )
97 96 fveq2d ⊢ ( 𝑍 = 0 → ( 𝑁 ‘ { 𝑌 , 𝑍 } ) = ( 𝑁 ‘ { 𝑌 , 0 } ) )
98 1 3 4 18 74 lsppr0 ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( 𝑁 ‘ { 𝑌 , 0 } ) = ( 𝑁 ‘ { 𝑌 } ) )
99 97 98 sylan9eqr ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) ∧ 𝑍 = 0 ) → ( 𝑁 ‘ { 𝑌 , 𝑍 } ) = ( 𝑁 ‘ { 𝑌 } ) )
100 95 99 eleqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) ∧ 𝑍 = 0 ) → 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) )
101 100 ex ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( 𝑍 = 0 → 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) ) )
102 101 necon3bd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( ¬ 𝑋 ∈ ( 𝑁 ‘ { 𝑌 } ) → 𝑍 ≠ 0 ) )
103 67 102 mpd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → 𝑍 ≠ 0 )
104 1 13 11 12 34 3 23 39 40 lvecvsn0 ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ≠ 0 ↔ ( 𝑙 ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑍 ≠ 0 ) ) )
105 93 103 104 mpbir2and ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ≠ 0 )
106 1 13 11 12 34 3 23 60 42 lvecvsn0 ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ≠ 0 ↔ ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ≠ 0 ) ) )
107 66 105 106 mpbir2and ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ≠ 0 )
108 eldifsn ⊢ ( ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ∈ ( ( 𝑁 ‘ { 𝑍 } ) ∖ { 0 } ) ↔ ( ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ∈ ( 𝑁 ‘ { 𝑍 } ) ∧ ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ≠ 0 ) )
109 64 107 108 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ∈ ( ( 𝑁 ‘ { 𝑍 } ) ∖ { 0 } ) )
110 simp3 ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) )
111 1 2 lmodvacl ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ∈ 𝑉 ∧ ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ∈ 𝑉 ) → ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ∈ 𝑉 )
112 18 76 42 111 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ∈ 𝑉 )
113 1 4 lspsnid ⊢ ( ( 𝑊 ∈ LMod ∧ ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ∈ 𝑉 ) → ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ∈ ( 𝑁 ‘ { ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) } ) )
114 18 112 113 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ∈ ( 𝑁 ‘ { ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) } ) )
115 110 114 eqeltrd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → 𝑋 ∈ ( 𝑁 ‘ { ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) } ) )
116 1 11 13 12 34 4 lspsnvs ⊢ ( ( 𝑊 ∈ LVec ∧ ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ∈ 𝑉 ) → ( 𝑁 ‘ { ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) } ) = ( 𝑁 ‘ { ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) } ) )
117 23 60 66 112 116 syl121anc ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( 𝑁 ‘ { ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) } ) = ( 𝑁 ‘ { ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) } ) )
118 1 2 11 13 12 lmodvsdi ⊢ ( ( 𝑊 ∈ LMod ∧ ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ∈ 𝑉 ∧ ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ∈ 𝑉 ) ) → ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) = ( ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) + ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) )
119 18 60 76 42 118 syl13anc ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) = ( ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) + ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) )
120 eqid ⊢ ( .r ‘ ( Scalar ‘ 𝑊 ) ) = ( .r ‘ ( Scalar ‘ 𝑊 ) )
121 eqid ⊢ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) = ( 1r ‘ ( Scalar ‘ 𝑊 ) )
122 12 34 120 121 58 drnginvrl ⊢ ( ( ( Scalar ‘ 𝑊 ) ∈ DivRing ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝑘 ) = ( 1r ‘ ( Scalar ‘ 𝑊 ) ) )
123 25 26 57 122 syl3anc ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝑘 ) = ( 1r ‘ ( Scalar ‘ 𝑊 ) ) )
124 123 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝑘 ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) = ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) )
125 1 11 13 12 120 lmodvsass ⊢ ( ( 𝑊 ∈ LMod ∧ ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑌 ∈ 𝑉 ) ) → ( ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝑘 ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) = ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) )
126 18 60 26 74 125 syl13anc ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝑘 ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) = ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) )
127 1 11 13 121 lmodvs1 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) → ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) = 𝑌 )
128 18 74 127 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) = 𝑌 )
129 124 126 128 3eqtr3d ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) = 𝑌 )
130 129 oveq1d ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) + ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) = ( 𝑌 + ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) )
131 119 130 eqtrd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) = ( 𝑌 + ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) )
132 131 sneqd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → { ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) } = { ( 𝑌 + ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) } )
133 132 fveq2d ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( 𝑁 ‘ { ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) } ) = ( 𝑁 ‘ { ( 𝑌 + ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) } ) )
134 117 133 eqtr3d ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ( 𝑁 ‘ { ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) } ) = ( 𝑁 ‘ { ( 𝑌 + ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) } ) )
135 115 134 eleqtrd ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → 𝑋 ∈ ( 𝑁 ‘ { ( 𝑌 + ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) } ) )
136 oveq2 ⊢ ( 𝑧 = ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) → ( 𝑌 + 𝑧 ) = ( 𝑌 + ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) )
137 136 sneqd ⊢ ( 𝑧 = ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) → { ( 𝑌 + 𝑧 ) } = { ( 𝑌 + ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) } )
138 137 fveq2d ⊢ ( 𝑧 = ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) → ( 𝑁 ‘ { ( 𝑌 + 𝑧 ) } ) = ( 𝑁 ‘ { ( 𝑌 + ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) } ) )
139 138 eleq2d ⊢ ( 𝑧 = ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) → ( 𝑋 ∈ ( 𝑁 ‘ { ( 𝑌 + 𝑧 ) } ) ↔ 𝑋 ∈ ( 𝑁 ‘ { ( 𝑌 + ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) } ) ) )
140 139 rspcev ⊢ ( ( ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ∈ ( ( 𝑁 ‘ { 𝑍 } ) ∖ { 0 } ) ∧ 𝑋 ∈ ( 𝑁 ‘ { ( 𝑌 + ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑘 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) } ) ) → ∃ 𝑧 ∈ ( ( 𝑁 ‘ { 𝑍 } ) ∖ { 0 } ) 𝑋 ∈ ( 𝑁 ‘ { ( 𝑌 + 𝑧 ) } ) )
141 109 135 140 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) ) → ∃ 𝑧 ∈ ( ( 𝑁 ‘ { 𝑍 } ) ∖ { 0 } ) 𝑋 ∈ ( 𝑁 ‘ { ( 𝑌 + 𝑧 ) } ) )
142 141 3exp ⊢ ( 𝜑 → ( ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) → ( 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) → ∃ 𝑧 ∈ ( ( 𝑁 ‘ { 𝑍 } ) ∖ { 0 } ) 𝑋 ∈ ( 𝑁 ‘ { ( 𝑌 + 𝑧 ) } ) ) ) )
143 142 rexlimdvv ⊢ ( 𝜑 → ( ∃ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑋 = ( ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) + ( 𝑙 ( ·𝑠 ‘ 𝑊 ) 𝑍 ) ) → ∃ 𝑧 ∈ ( ( 𝑁 ‘ { 𝑍 } ) ∖ { 0 } ) 𝑋 ∈ ( 𝑁 ‘ { ( 𝑌 + 𝑧 ) } ) ) )
144 17 143 mpd ⊢ ( 𝜑 → ∃ 𝑧 ∈ ( ( 𝑁 ‘ { 𝑍 } ) ∖ { 0 } ) 𝑋 ∈ ( 𝑁 ‘ { ( 𝑌 + 𝑧 ) } ) )