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 ⊢V=BaseW
lspsneleq.o ⊢0˙=0W
lspsneleq.n ⊢N=LSpan⁡W
lspsneleq.w ⊢φ→W∈LVec
lspsneleq.x ⊢φ→X∈V
lspsneleq.y ⊢φ→Y∈N⁡X
lspsneleq.z ⊢φ→Y≠0˙
Assertion lspsneleq ⊢φ→N⁡Y=N⁡X

Proof

Step Hyp Ref Expression
1 lspsneleq.v ⊢V=BaseW
2 lspsneleq.o ⊢0˙=0W
3 lspsneleq.n ⊢N=LSpan⁡W
4 lspsneleq.w ⊢φ→W∈LVec
5 lspsneleq.x ⊢φ→X∈V
6 lspsneleq.y ⊢φ→Y∈N⁡X
7 lspsneleq.z ⊢φ→Y≠0˙
8 lveclmod ⊢W∈LVec→W∈LMod
9 4 8 syl ⊢φ→W∈LMod
10 eqid ⊢Scalar⁡W=Scalar⁡W
11 eqid ⊢BaseScalar⁡W=BaseScalar⁡W
12 eqid ⊢⋅W=⋅W
13 10 11 1 12 3 lspsnel ⊢W∈LMod∧X∈V→Y∈N⁡X↔∃k∈BaseScalar⁡WY=k⋅WX
14 9 5 13 syl2anc ⊢φ→Y∈N⁡X↔∃k∈BaseScalar⁡WY=k⋅WX
15 simpr ⊢φ∧k∈BaseScalar⁡W∧Y=k⋅WX→Y=k⋅WX
16 15 sneqd ⊢φ∧k∈BaseScalar⁡W∧Y=k⋅WX→Y=k⋅WX
17 16 fveq2d ⊢φ∧k∈BaseScalar⁡W∧Y=k⋅WX→N⁡Y=N⁡k⋅WX
18 4 ad2antrr ⊢φ∧k∈BaseScalar⁡W∧Y=k⋅WX→W∈LVec
19 simplr ⊢φ∧k∈BaseScalar⁡W∧Y=k⋅WX→k∈BaseScalar⁡W
20 7 ad2antrr ⊢φ∧k∈BaseScalar⁡W∧Y=k⋅WX→Y≠0˙
21 simplr ⊢φ∧k∈BaseScalar⁡W∧Y=k⋅WX∧k=0Scalar⁡W→Y=k⋅WX
22 simpr ⊢φ∧k∈BaseScalar⁡W∧Y=k⋅WX∧k=0Scalar⁡W→k=0Scalar⁡W
23 22 oveq1d ⊢φ∧k∈BaseScalar⁡W∧Y=k⋅WX∧k=0Scalar⁡W→k⋅WX=0Scalar⁡W⋅WX
24 eqid ⊢0Scalar⁡W=0Scalar⁡W
25 1 10 12 24 2 lmod0vs ⊢W∈LMod∧X∈V→0Scalar⁡W⋅WX=0˙
26 9 5 25 syl2anc ⊢φ→0Scalar⁡W⋅WX=0˙
27 26 ad3antrrr ⊢φ∧k∈BaseScalar⁡W∧Y=k⋅WX∧k=0Scalar⁡W→0Scalar⁡W⋅WX=0˙
28 21 23 27 3eqtrd ⊢φ∧k∈BaseScalar⁡W∧Y=k⋅WX∧k=0Scalar⁡W→Y=0˙
29 28 ex ⊢φ∧k∈BaseScalar⁡W∧Y=k⋅WX→k=0Scalar⁡W→Y=0˙
30 29 necon3d ⊢φ∧k∈BaseScalar⁡W∧Y=k⋅WX→Y≠0˙→k≠0Scalar⁡W
31 20 30 mpd ⊢φ∧k∈BaseScalar⁡W∧Y=k⋅WX→k≠0Scalar⁡W
32 5 ad2antrr ⊢φ∧k∈BaseScalar⁡W∧Y=k⋅WX→X∈V
33 1 10 12 11 24 3 lspsnvs ⊢W∈LVec∧k∈BaseScalar⁡W∧k≠0Scalar⁡W∧X∈V→N⁡k⋅WX=N⁡X
34 18 19 31 32 33 syl121anc ⊢φ∧k∈BaseScalar⁡W∧Y=k⋅WX→N⁡k⋅WX=N⁡X
35 17 34 eqtrd ⊢φ∧k∈BaseScalar⁡W∧Y=k⋅WX→N⁡Y=N⁡X
36 35 rexlimdva2 ⊢φ→∃k∈BaseScalar⁡WY=k⋅WX→N⁡Y=N⁡X
37 14 36 sylbid ⊢φ→Y∈N⁡X→N⁡Y=N⁡X
38 6 37 mpd ⊢φ→N⁡Y=N⁡X