Metamath Proof Explorer


Theorem prjspeclsp

Description: The vectors equivalent to a vector X are the nonzero vectors in the span of X . (Contributed by Steven Nguyen, 6-Jun-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 prjspeclsp V LVec X B X ˙ = N X 0 V

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 1 cnveqi ˙ -1 = x y | x B y B l K x = l · ˙ y -1
8 cnvopab x y | x B y B l K x = l · ˙ y -1 = y x | x B y B l K x = l · ˙ y
9 7 8 eqtri ˙ -1 = y x | x B y B l K x = l · ˙ y
10 9 eceq2i X ˙ -1 = X y x | x B y B l K x = l · ˙ y
11 df-ec X y x | x B y B l K x = l · ˙ y = y x | x B y B l K x = l · ˙ y X
12 11 a1i V LVec X B X y x | x B y B l K x = l · ˙ y = y x | x B y B l K x = l · ˙ y X
13 imaopab y x | x B y B l K x = l · ˙ y X = x | y X x B y B l K x = l · ˙ y
14 13 a1i V LVec X B y x | x B y B l K x = l · ˙ y X = x | y X x B y B l K x = l · ˙ y
15 df-rex y X x B y B l K x = l · ˙ y y y X x B y B l K x = l · ˙ y
16 velsn y X y = X
17 16 anbi1i y X x B y B l K x = l · ˙ y y = X x B y B l K x = l · ˙ y
18 eleq1 y = X y B X B
19 18 anbi2d y = X x B y B x B X B
20 oveq2 y = X l · ˙ y = l · ˙ X
21 20 eqeq2d y = X x = l · ˙ y x = l · ˙ X
22 21 rexbidv y = X l K x = l · ˙ y l K x = l · ˙ X
23 19 22 anbi12d y = X x B y B l K x = l · ˙ y x B X B l K x = l · ˙ X
24 23 pm5.32i y = X x B y B l K x = l · ˙ y y = X x B X B l K x = l · ˙ X
25 17 24 bitri y X x B y B l K x = l · ˙ y y = X x B X B l K x = l · ˙ X
26 25 exbii y y X x B y B l K x = l · ˙ y y y = X x B X B l K x = l · ˙ X
27 19.41v y y = X x B X B l K x = l · ˙ X y y = X x B X B l K x = l · ˙ X
28 elisset X B y y = X
29 28 ad2antlr x B X B l K x = l · ˙ X y y = X
30 29 pm4.71ri x B X B l K x = l · ˙ X y y = X x B X B l K x = l · ˙ X
31 27 30 bitr4i y y = X x B X B l K x = l · ˙ X x B X B l K x = l · ˙ X
32 15 26 31 3bitri y X x B y B l K x = l · ˙ y x B X B l K x = l · ˙ X
33 32 abbii x | y X x B y B l K x = l · ˙ y = x | x B X B l K x = l · ˙ X
34 iba X B x B x B X B
35 34 bicomd X B x B X B x B
36 35 anbi1d X B x B X B l K x = l · ˙ X x B l K x = l · ˙ X
37 36 abbidv X B x | x B X B l K x = l · ˙ X = x | x B l K x = l · ˙ X
38 33 37 syl5eq X B x | y X x B y B l K x = l · ˙ y = x | x B l K x = l · ˙ X
39 38 adantl V LVec X B x | y X x B y B l K x = l · ˙ y = x | x B l K x = l · ˙ X
40 12 14 39 3eqtrd V LVec X B X y x | x B y B l K x = l · ˙ y = x | x B l K x = l · ˙ X
41 10 40 syl5eq V LVec X B X ˙ -1 = x | x B l K x = l · ˙ X
42 df-rab x B | l K x = l · ˙ X = x | x B l K x = l · ˙ X
43 42 a1i V LVec X B x B | l K x = l · ˙ X = x | x B l K x = l · ˙ X
44 2 rabeqi x B | l K x = l · ˙ X = x Base V 0 V | l K x = l · ˙ X
45 rabdif x Base V | l K x = l · ˙ X 0 V = x Base V 0 V | l K x = l · ˙ X
46 45 a1i V LVec X B x Base V | l K x = l · ˙ X 0 V = x Base V 0 V | l K x = l · ˙ X
47 44 46 eqtr4id V LVec X B x B | l K x = l · ˙ X = x Base V | l K x = l · ˙ X 0 V
48 41 43 47 3eqtr2d V LVec X B X ˙ -1 = x Base V | l K x = l · ˙ X 0 V
49 1 2 3 4 5 prjsper V LVec ˙ Er B
50 49 adantr V LVec X B ˙ Er B
51 ercnv ˙ Er B ˙ -1 = ˙
52 51 eqcomd ˙ Er B ˙ = ˙ -1
53 50 52 syl V LVec X B ˙ = ˙ -1
54 53 eceq2d V LVec X B X ˙ = X ˙ -1
55 lveclmod V LVec V LMod
56 difss Base V 0 V Base V
57 2 56 eqsstri B Base V
58 57 sseli X B X Base V
59 eqid Base V = Base V
60 3 5 59 4 6 lspsn V LMod X Base V N X = x | l K x = l · ˙ X
61 55 58 60 syl2an V LVec X B N X = x | l K x = l · ˙ X
62 simpr V LVec X B l K x = l · ˙ X x = l · ˙ X
63 55 adantr V LVec X B V LMod
64 63 adantr V LVec X B l K V LMod
65 simpr V LVec X B l K l K
66 58 ad2antlr V LVec X B l K X Base V
67 59 3 4 5 lmodvscl V LMod l K X Base V l · ˙ X Base V
68 64 65 66 67 syl3anc V LVec X B l K l · ˙ X Base V
69 68 adantr V LVec X B l K x = l · ˙ X l · ˙ X Base V
70 62 69 eqeltrd V LVec X B l K x = l · ˙ X x Base V
71 70 rexlimdva2 V LVec X B l K x = l · ˙ X x Base V
72 71 pm4.71rd V LVec X B l K x = l · ˙ X x Base V l K x = l · ˙ X
73 72 abbidv V LVec X B x | l K x = l · ˙ X = x | x Base V l K x = l · ˙ X
74 df-rab x Base V | l K x = l · ˙ X = x | x Base V l K x = l · ˙ X
75 73 74 eqtr4di V LVec X B x | l K x = l · ˙ X = x Base V | l K x = l · ˙ X
76 61 75 eqtrd V LVec X B N X = x Base V | l K x = l · ˙ X
77 76 difeq1d V LVec X B N X 0 V = x Base V | l K x = l · ˙ X 0 V
78 48 54 77 3eqtr4d V LVec X B X ˙ = N X 0 V