Metamath Proof Explorer

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 ellspsn ⊢ ( ( 𝑊 ∈ 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 ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑌 } ) = ( 𝑁 ‘ { 𝑋 } ) )