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 ∧ ( 𝐴 ⊆ 𝑉 ∧ 𝑌 ∈ 𝑉 ∧ 𝑋 ∈ ( ( 𝑁 ‘ ( 𝐴 ∪ { 𝑌 } ) ) ∖ ( 𝑁 ‘ 𝐴 ) ) ) ) → 𝑌 ∈ ( 𝑁 ‘ ( 𝐴 ∪ { 𝑋 } ) ) )