Metamath Proof Explorer


Theorem prjsprellsp

Description: Two vectors are equivalent iff their spans are equal. (Contributed by Steven Nguyen, 31-May-2023)

Ref Expression
Hypotheses prjsprel.1 ˙ = x y | x B y B l K x = l · ˙ y
prjspertr.b B = Base V 0 V
prjspertr.s S = Scalar V
prjspertr.x · ˙ = V
prjspertr.k K = Base S
prjsprellsp.n N = LSpan V
Assertion prjsprellsp V LVec X B Y B X ˙ Y N X = N Y

Proof

Step Hyp Ref Expression
1 prjsprel.1 ˙ = x y | x B y B l K x = l · ˙ y
2 prjspertr.b B = Base V 0 V
3 prjspertr.s S = Scalar V
4 prjspertr.x · ˙ = V
5 prjspertr.k K = Base S
6 prjsprellsp.n N = LSpan V
7 ibar X B Y B m K 0 S X = m · ˙ Y X B Y B m K 0 S X = m · ˙ Y
8 7 bicomd X B Y B X B Y B m K 0 S X = m · ˙ Y m K 0 S X = m · ˙ Y
9 8 adantl V LVec X B Y B X B Y B m K 0 S X = m · ˙ Y m K 0 S X = m · ˙ Y
10 eqid 0 S = 0 S
11 1 2 3 4 5 10 prjspreln0 V LVec X ˙ Y X B Y B m K 0 S X = m · ˙ Y
12 11 adantr V LVec X B Y B X ˙ Y X B Y B m K 0 S X = m · ˙ Y
13 eqid Base V = Base V
14 simpl V LVec X B Y B V LVec
15 eldifi X Base V 0 V X Base V
16 15 2 eleq2s X B X Base V
17 16 ad2antrl V LVec X B Y B X Base V
18 eldifi Y Base V 0 V Y Base V
19 18 2 eleq2s Y B Y Base V
20 19 ad2antll V LVec X B Y B Y Base V
21 13 3 5 10 4 6 14 17 20 lspsneq V LVec X B Y B N X = N Y m K 0 S X = m · ˙ Y
22 9 12 21 3bitr4d V LVec X B Y B X ˙ Y N X = N Y