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 } ) 𝑋 ∈ ( 𝑁 ‘ { ( 𝑌 + 𝑧 ) } ) )