Metamath Proof Explorer

Theorem lspsolv

Description: If X is in the span of A u. { Y } but not A , then Y is in the span of A u. { X } . (Contributed by Mario Carneiro, 25-Jun-2014)

Ref Expression
Hypotheses lspsolv.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
lspsolv.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
lspsolv.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
Assertion lspsolv ( ( 𝑊 ∈ LVec ∧ ( 𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) ) ) → 𝑌 ∈ ( 𝑁 ‘ ( 𝐴 ∪ { 𝑋 } ) ) )

Proof

Step Hyp Ref Expression
1 lspsolv.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 lspsolv.s ⊢ 𝑆 = ( LSubSp ‘ 𝑊 )
3 lspsolv.n ⊢ 𝑁 = ( LSpan ‘ 𝑊 )
4 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
5 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
6 eqid ⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
7 eqid ⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
8 eqid ⊢ { 𝑧 ∈ 𝑉 ∣ ∃ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ( 𝑧 ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) } = { 𝑧 ∈ 𝑉 ∣ ∃ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ( 𝑧 ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) }
9 lveclmod ⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
10 9 adantr ⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) ) ) → 𝑊 ∈ LMod )
11 simpr1 ⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) ) ) → 𝐴 ⊆ 𝑉 )
12 simpr2 ⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) ) ) → 𝑌 ∈ 𝑉 )
13 simpr3 ⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) ) ) → 𝑋 ∈ ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) )
14 13 eldifad ⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) ) ) → 𝑋 ∈ ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) )
15 1 2 3 4 5 6 7 8 10 11 12 14 lspsolvlem ⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) ) ) → ∃ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) )
16 4 lvecdrng ⊢ ( 𝑊 ∈ LVec → ( Scalar ‘ 𝑊 ) ∈ DivRing )
17 16 ad2antrr ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) ) ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → ( Scalar ‘ 𝑊 ) ∈ DivRing )
18 simprl ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) ) ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
19 10 adantr ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) ) ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → 𝑊 ∈ LMod )
20 12 adantr ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) ) ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → 𝑌 ∈ 𝑉 )
21 eqid ⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
22 eqid ⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
23 1 4 7 21 22 lmod0vs ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) → ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) = ( 0g ‘ 𝑊 ) )
24 19 20 23 syl2anc ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) ) ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) = ( 0g ‘ 𝑊 ) )
25 24 oveq2d ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) ) ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → ( 𝑋 ( +g ‘ 𝑊 ) ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) = ( 𝑋 ( +g ‘ 𝑊 ) ( 0g ‘ 𝑊 ) ) )
26 11 adantr ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) ) ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → 𝐴 ⊆ 𝑉 )
27 20 snssd ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) ) ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → { 𝑌 } ⊆ 𝑉 )
28 26 27 unssd ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) ) ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → ( 𝐴 ∪ { 𝑌 } ) ⊆ 𝑉 )
29 1 3 lspssv ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝐴 ∪ { 𝑌 } ) ⊆ 𝑉 ) → ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ⊆ 𝑉 )
30 19 28 29 syl2anc ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) ) ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ⊆ 𝑉 )
31 30 ssdifssd ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) ) ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) ⊆ 𝑉 )
32 13 adantr ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) ) ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → 𝑋 ∈ ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) )
33 31 32 sseldd ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) ) ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → 𝑋 ∈ 𝑉 )
34 1 6 22 lmod0vrid ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑋 ( +g ‘ 𝑊 ) ( 0g ‘ 𝑊 ) ) = 𝑋 )
35 19 33 34 syl2anc ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) ) ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → ( 𝑋 ( +g ‘ 𝑊 ) ( 0g ‘ 𝑊 ) ) = 𝑋 )
36 25 35 eqtrd ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) ) ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → ( 𝑋 ( +g ‘ 𝑊 ) ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) = 𝑋 )
37 36 32 eqeltrd ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) ) ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → ( 𝑋 ( +g ‘ 𝑊 ) ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) )
38 37 eldifbd ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) ) ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → ¬ ( 𝑋 ( +g ‘ 𝑊 ) ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) )
39 simprr ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) ) ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) )
40 oveq1 ⊢ ( 𝑟 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) → ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) = ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) )
41 40 oveq2d ⊢ ( 𝑟 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) → ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) = ( 𝑋 ( +g ‘ 𝑊 ) ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) )
42 41 eleq1d ⊢ ( 𝑟 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) → ( ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ↔ ( 𝑋 ( +g ‘ 𝑊 ) ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) )
43 39 42 syl5ibcom ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) ) ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → ( 𝑟 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) → ( 𝑋 ( +g ‘ 𝑊 ) ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) )
44 43 necon3bd ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) ) ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → ( ¬ ( 𝑋 ( +g ‘ 𝑊 ) ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) → 𝑟 ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
45 38 44 mpd ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) ) ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → 𝑟 ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
46 eqid ⊢ ( .r ‘ ( Scalar ‘ 𝑊 ) ) = ( .r ‘ ( Scalar ‘ 𝑊 ) )
47 eqid ⊢ ( 1r ‘ ( Scalar ‘ 𝑊 ) ) = ( 1r ‘ ( Scalar ‘ 𝑊 ) )
48 eqid ⊢ ( invr ‘ ( Scalar ‘ 𝑊 ) ) = ( invr ‘ ( Scalar ‘ 𝑊 ) )
49 5 21 46 47 48 drnginvrl ⊢ ( ( ( Scalar ‘ 𝑊 ) ∈ DivRing ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑟 ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑟 ) ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝑟 ) = ( 1r ‘ ( Scalar ‘ 𝑊 ) ) )
50 17 18 45 49 syl3anc ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) ) ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑟 ) ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝑟 ) = ( 1r ‘ ( Scalar ‘ 𝑊 ) ) )
51 50 oveq1d ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) ) ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → ( ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑟 ) ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) = ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) )
52 5 21 48 drnginvrcl ⊢ ( ( ( Scalar ‘ 𝑊 ) ∈ DivRing ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑟 ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑟 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
53 17 18 45 52 syl3anc ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) ) ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑟 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
54 1 4 7 5 46 lmodvsass ⊢ ( ( 𝑊 ∈ LMod ∧ ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑟 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑌 ∈ 𝑉 ) ) → ( ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑟 ) ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) = ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑟 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) )
55 19 53 18 20 54 syl13anc ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) ) ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → ( ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑟 ) ( .r ‘ ( Scalar ‘ 𝑊 ) ) 𝑟 ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) = ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑟 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) )
56 1 4 7 47 lmodvs1 ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑌 ∈ 𝑉 ) → ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) = 𝑌 )
57 19 20 56 syl2anc ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) ) ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → ( ( 1r ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑌 ) = 𝑌 )
58 51 55 57 3eqtr3d ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) ) ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑟 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) = 𝑌 )
59 33 snssd ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) ) ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → { 𝑋 } ⊆ 𝑉 )
60 26 59 unssd ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) ) ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → ( 𝐴 ∪ { 𝑋 } ) ⊆ 𝑉 )
61 1 2 3 lspcl ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝐴 ∪ { 𝑋 } ) ⊆ 𝑉 ) → ( 𝑁 ‘ ( 𝐴 ∪ { 𝑋 } ) ) ∈ 𝑆 )
62 19 60 61 syl2anc ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) ) ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → ( 𝑁 ‘ ( 𝐴 ∪ { 𝑋 } ) ) ∈ 𝑆 )
63 1 4 7 5 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑌 ∈ 𝑉 ) → ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ∈ 𝑉 )
64 19 18 20 63 syl3anc ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) ) ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ∈ 𝑉 )
65 eqid ⊢ ( -g ‘ 𝑊 ) = ( -g ‘ 𝑊 )
66 1 6 65 lmodvpncan ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) → ( ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) 𝑋 ) ( -g ‘ 𝑊 ) 𝑋 ) = ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) )
67 19 64 33 66 syl3anc ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) ) ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → ( ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) 𝑋 ) ( -g ‘ 𝑊 ) 𝑋 ) = ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) )
68 1 6 lmodcom ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ∈ 𝑉 ∧ 𝑋 ∈ 𝑉 ) → ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) 𝑋 ) = ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) )
69 19 64 33 68 syl3anc ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) ) ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) 𝑋 ) = ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) )
70 ssun1 ⊢ 𝐴 ⊆ ( 𝐴 ∪ { 𝑋 } )
71 70 a1i ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) ) ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → 𝐴 ⊆ ( 𝐴 ∪ { 𝑋 } ) )
72 1 3 lspss ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝐴 ∪ { 𝑋 } ) ⊆ 𝑉 ∧ 𝐴 ⊆ ( 𝐴 ∪ { 𝑋 } ) ) → ( 𝑁 ‘ 𝐴 ) ⊆ ( 𝑁 ‘ ( 𝐴 ∪ { 𝑋 } ) ) )
73 19 60 71 72 syl3anc ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) ) ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → ( 𝑁 ‘ 𝐴 ) ⊆ ( 𝑁 ‘ ( 𝐴 ∪ { 𝑋 } ) ) )
74 73 39 sseldd ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) ) ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( 𝑁 ‘ ( 𝐴 ∪ { 𝑋 } ) ) )
75 69 74 eqeltrd ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) ) ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) 𝑋 ) ∈ ( 𝑁 ‘ ( 𝐴 ∪ { 𝑋 } ) ) )
76 1 3 lspssid ⊢ ( ( 𝑊 ∈ LMod ∧ ( 𝐴 ∪ { 𝑋 } ) ⊆ 𝑉 ) → ( 𝐴 ∪ { 𝑋 } ) ⊆ ( 𝑁 ‘ ( 𝐴 ∪ { 𝑋 } ) ) )
77 19 60 76 syl2anc ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) ) ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → ( 𝐴 ∪ { 𝑋 } ) ⊆ ( 𝑁 ‘ ( 𝐴 ∪ { 𝑋 } ) ) )
78 snidg ⊢ ( 𝑋 ∈ 𝑉 → 𝑋 ∈ { 𝑋 } )
79 elun2 ⊢ ( 𝑋 ∈ { 𝑋 } → 𝑋 ∈ ( 𝐴 ∪ { 𝑋 } ) )
80 33 78 79 3syl ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) ) ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → 𝑋 ∈ ( 𝐴 ∪ { 𝑋 } ) )
81 77 80 sseldd ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) ) ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → 𝑋 ∈ ( 𝑁 ‘ ( 𝐴 ∪ { 𝑋 } ) ) )
82 65 2 lssvsubcl ⊢ ( ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ ( 𝐴 ∪ { 𝑋 } ) ) ∈ 𝑆 ) ∧ ( ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) 𝑋 ) ∈ ( 𝑁 ‘ ( 𝐴 ∪ { 𝑋 } ) ) ∧ 𝑋 ∈ ( 𝑁 ‘ ( 𝐴 ∪ { 𝑋 } ) ) ) ) → ( ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) 𝑋 ) ( -g ‘ 𝑊 ) 𝑋 ) ∈ ( 𝑁 ‘ ( 𝐴 ∪ { 𝑋 } ) ) )
83 19 62 75 81 82 syl22anc ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) ) ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → ( ( ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ( +g ‘ 𝑊 ) 𝑋 ) ( -g ‘ 𝑊 ) 𝑋 ) ∈ ( 𝑁 ‘ ( 𝐴 ∪ { 𝑋 } ) ) )
84 67 83 eqeltrrd ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) ) ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ∈ ( 𝑁 ‘ ( 𝐴 ∪ { 𝑋 } ) ) )
85 4 7 5 2 lssvscl ⊢ ( ( ( 𝑊 ∈ LMod ∧ ( 𝑁 ‘ ( 𝐴 ∪ { 𝑋 } ) ) ∈ 𝑆 ) ∧ ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑟 ) ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ∈ ( 𝑁 ‘ ( 𝐴 ∪ { 𝑋 } ) ) ) ) → ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑟 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( 𝑁 ‘ ( 𝐴 ∪ { 𝑋 } ) ) )
86 19 62 53 84 85 syl22anc ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) ) ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → ( ( ( invr ‘ ( Scalar ‘ 𝑊 ) ) ‘ 𝑟 ) ( ·𝑠 ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( 𝑁 ‘ ( 𝐴 ∪ { 𝑋 } ) ) )
87 58 86 eqeltrrd ⊢ ( ( ( 𝑊 ∈ LVec ∧ ( 𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) ) ) ∧ ( 𝑟 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ ( 𝑋 ( +g ‘ 𝑊 ) ( 𝑟 ( ·𝑠 ‘ 𝑊 ) 𝑌 ) ) ∈ ( 𝑁 ‘ 𝐴 ) ) ) → 𝑌 ∈ ( 𝑁 ‘ ( 𝐴 ∪ { 𝑋 } ) ) )
88 15 87 rexlimddv ⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) ) ) → 𝑌 ∈ ( 𝑁 ‘ ( 𝐴 ∪ { 𝑋 } ) ) )