Theorem lspsneleq

Description: Membership relation that implies equality of spans. ( spansneleq analog.) (Contributed by NM, 4-Jul-2014)

	Ref	Expression
Hypotheses	lspsneleq.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lspsneleq.o	⊢ 0 = ( 0g ‘ 𝑊 )
	lspsneleq.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
	lspsneleq.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
	lspsneleq.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	lspsneleq.y	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑁 ‘ { 𝑋 } ) )
	lspsneleq.z	⊢ ( 𝜑 → 𝑌 ≠ 0 )
Assertion	lspsneleq	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) = ( 𝑁 ‘ { 𝑋 } ) )

Proof

Step	Hyp	Ref	Expression
1		lspsneleq.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lspsneleq.o	⊢ 0 = ( 0g ‘ 𝑊 )
3		lspsneleq.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
4		lspsneleq.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
5		lspsneleq.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
6		lspsneleq.y	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑁 ‘ { 𝑋 } ) )
7		lspsneleq.z	⊢ ( 𝜑 → 𝑌 ≠ 0 )
8		lveclmod	⊢ ( 𝑊 ∈ LVec → 𝑊 ∈ LMod )
9	4 8	syl	⊢ ( 𝜑 → 𝑊 ∈ LMod )
10		eqid	⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
11		eqid	⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
12		eqid	⊢ ( ·𝑠 ‘ 𝑊 ) = ( ·𝑠 ‘ 𝑊 )
13	10 11 1 12 3	lspsnel	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑌 ∈ ( 𝑁 ‘ { 𝑋 } ) ↔ ∃ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑌 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) )
14	9 5 13	syl2anc	⊢ ( 𝜑 → ( 𝑌 ∈ ( 𝑁 ‘ { 𝑋 } ) ↔ ∃ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑌 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) )
15		simpr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑌 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) → 𝑌 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) )
16	15	sneqd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑌 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) → { 𝑌 } = { ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) } )
17	16	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑌 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) → ( 𝑁 ‘ { 𝑌 } ) = ( 𝑁 ‘ { ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) } ) )
18	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑌 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) → 𝑊 ∈ LVec )
19		simplr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑌 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) → 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
20	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑌 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) → 𝑌 ≠ 0 )
21		simplr	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑌 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) ∧ 𝑘 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → 𝑌 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) )
22		simpr	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑌 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) ∧ 𝑘 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → 𝑘 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
23	22	oveq1d	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑌 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) ∧ 𝑘 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) = ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑋 ) )
24		eqid	⊢ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
25	1 10 12 24 2	lmod0vs	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑋 ) = 0 )
26	9 5 25	syl2anc	⊢ ( 𝜑 → ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑋 ) = 0 )
27	26	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑌 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) ∧ 𝑘 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → ( ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ( ·𝑠 ‘ 𝑊 ) 𝑋 ) = 0 )
28	21 23 27	3eqtrd	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑌 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) ∧ 𝑘 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) → 𝑌 = 0 )
29	28	ex	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑌 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) → ( 𝑘 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) → 𝑌 = 0 ) )
30	29	necon3d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑌 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) → ( 𝑌 ≠ 0 → 𝑘 ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) )
31	20 30	mpd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑌 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) → 𝑘 ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
32	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑌 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) → 𝑋 ∈ 𝑉 )
33	1 10 12 11 24 3	lspsnvs	⊢ ( ( 𝑊 ∈ LVec ∧ ( 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑘 ≠ ( 0g ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ { ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) } ) = ( 𝑁 ‘ { 𝑋 } ) )
34	18 19 31 32 33	syl121anc	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑌 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) → ( 𝑁 ‘ { ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) } ) = ( 𝑁 ‘ { 𝑋 } ) )
35	17 34	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ∧ 𝑌 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) ) → ( 𝑁 ‘ { 𝑌 } ) = ( 𝑁 ‘ { 𝑋 } ) )
36	35	rexlimdva2	⊢ ( 𝜑 → ( ∃ 𝑘 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑌 = ( 𝑘 ( ·𝑠 ‘ 𝑊 ) 𝑋 ) → ( 𝑁 ‘ { 𝑌 } ) = ( 𝑁 ‘ { 𝑋 } ) ) )
37	14 36	sylbid	⊢ ( 𝜑 → ( 𝑌 ∈ ( 𝑁 ‘ { 𝑋 } ) → ( 𝑁 ‘ { 𝑌 } ) = ( 𝑁 ‘ { 𝑋 } ) ) )
38	6 37	mpd	⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) = ( 𝑁 ‘ { 𝑋 } ) )