Metamath Proof Explorer


Theorem prjspner1

Description: Two vectors whose zeroth coordinate is nonzero are equivalent if and only if they have the same representative in the (n-1)-dimensional affine subspace { x_0 = 1 } . For example, vectors in 3D space whose x coordinate is nonzero are equivalent iff they intersect at the plane x = 1 at the same point (also see section header). (Contributed by SN, 13-Aug-2023)

Ref Expression
Hypotheses prjspner01.e ˙=xy|xByBlSx=l·˙y
prjspner01.f F=bBifb0=0˙bIb0·˙b
prjspner01.b B=BaseW0W
prjspner01.w W=KfreeLMod0N
prjspner01.t ·˙=W
prjspner01.s S=BaseK
prjspner01.0 0˙=0K
prjspner01.i I=invrK
prjspner01.k φKDivRing
prjspner01.n φN0
prjspner01.x φXB
prjspner1.y φYB
prjspner1.1 φX00˙
prjspner1.2 φY00˙
Assertion prjspner1 φX˙YFX=FY

Proof

Step Hyp Ref Expression
1 prjspner01.e ˙=xy|xByBlSx=l·˙y
2 prjspner01.f F=bBifb0=0˙bIb0·˙b
3 prjspner01.b B=BaseW0W
4 prjspner01.w W=KfreeLMod0N
5 prjspner01.t ·˙=W
6 prjspner01.s S=BaseK
7 prjspner01.0 0˙=0K
8 prjspner01.i I=invrK
9 prjspner01.k φKDivRing
10 prjspner01.n φN0
11 prjspner01.x φXB
12 prjspner1.y φYB
13 prjspner1.1 φX00˙
14 prjspner1.2 φY00˙
15 1 prjsprel X˙YXBYBmSX=m·˙Y
16 fveq1 X=0WX0=0W0
17 9 drngringd φKRing
18 ovexd φ0NV
19 0elfz N000N
20 10 19 syl φ00N
21 4 7 17 18 20 frlm0vald φ0W0=0˙
22 16 21 sylan9eqr φX=0WX0=0˙
23 13 22 mteqand φX0W
24 4 frlmsca KDivRing0NVK=ScalarW
25 9 18 24 syl2anc φK=ScalarW
26 25 fveq2d φ0K=0ScalarW
27 7 26 eqtrid φ0˙=0ScalarW
28 27 oveq1d φ0˙·˙Y=0ScalarW·˙Y
29 4 frlmlvec KDivRing0NVWLVec
30 9 18 29 syl2anc φWLVec
31 30 lveclmodd φWLMod
32 12 3 eleqtrdi φYBaseW0W
33 32 eldifad φYBaseW
34 eqid BaseW=BaseW
35 eqid ScalarW=ScalarW
36 eqid 0ScalarW=0ScalarW
37 eqid 0W=0W
38 34 35 5 36 37 lmod0vs WLModYBaseW0ScalarW·˙Y=0W
39 31 33 38 syl2anc φ0ScalarW·˙Y=0W
40 28 39 eqtrd φ0˙·˙Y=0W
41 23 40 neeqtrrd φX0˙·˙Y
42 41 ad2antrr φXBYBmSX0˙·˙Y
43 oveq1 m=0˙m·˙Y=0˙·˙Y
44 43 neeq2d m=0˙Xm·˙YX0˙·˙Y
45 42 44 syl5ibrcom φXBYBmSm=0˙Xm·˙Y
46 45 necon2d φXBYBmSX=m·˙Ym0˙
47 46 ancrd φXBYBmSX=m·˙Ym0˙X=m·˙Y
48 ovexd φXBYBmSm0˙0NV
49 simplr φXBYBmSm0˙mS
50 33 ad3antrrr φXBYBmSm0˙YBaseW
51 20 ad3antrrr φXBYBmSm0˙00N
52 eqid K=K
53 4 34 6 48 49 50 51 5 52 frlmvscaval φXBYBmSm0˙m·˙Y0=mKY0
54 53 fveq2d φXBYBmSm0˙Im·˙Y0=ImKY0
55 9 ad3antrrr φXBYBmSm0˙KDivRing
56 4 6 34 frlmbasf 0NVYBaseWY:0NS
57 18 33 56 syl2anc φY:0NS
58 57 20 ffvelrnd φY0S
59 58 ad3antrrr φXBYBmSm0˙Y0S
60 simpr φXBYBmSm0˙m0˙
61 14 ad3antrrr φXBYBmSm0˙Y00˙
62 6 7 52 8 55 49 59 60 61 drnginvmuld φXBYBmSm0˙ImKY0=IY0KIm
63 54 62 eqtrd φXBYBmSm0˙Im·˙Y0=IY0KIm
64 63 oveq1d φXBYBmSm0˙Im·˙Y0·˙m·˙Y=IY0KIm·˙m·˙Y
65 31 ad3antrrr φXBYBmSm0˙WLMod
66 17 ad3antrrr φXBYBmSm0˙KRing
67 6 7 8 55 59 61 drnginvrcld φXBYBmSm0˙IY0S
68 6 7 8 55 49 60 drnginvrcld φXBYBmSm0˙ImS
69 6 52 66 67 68 ringcld φXBYBmSm0˙IY0KImS
70 25 fveq2d φBaseK=BaseScalarW
71 6 70 eqtrid φS=BaseScalarW
72 71 ad3antrrr φXBYBmSm0˙S=BaseScalarW
73 69 72 eleqtrd φXBYBmSm0˙IY0KImBaseScalarW
74 49 72 eleqtrd φXBYBmSm0˙mBaseScalarW
75 eqid BaseScalarW=BaseScalarW
76 eqid ScalarW=ScalarW
77 34 35 5 75 76 lmodvsass WLModIY0KImBaseScalarWmBaseScalarWYBaseWIY0KImScalarWm·˙Y=IY0KIm·˙m·˙Y
78 65 73 74 50 77 syl13anc φXBYBmSm0˙IY0KImScalarWm·˙Y=IY0KIm·˙m·˙Y
79 6 52 66 67 68 49 ringassd φXBYBmSm0˙IY0KImKm=IY0KImKm
80 55 48 24 syl2anc φXBYBmSm0˙K=ScalarW
81 80 fveq2d φXBYBmSm0˙K=ScalarW
82 81 oveqd φXBYBmSm0˙IY0KImKm=IY0KImScalarWm
83 eqid 1K=1K
84 6 7 52 83 8 55 49 60 drnginvrld φXBYBmSm0˙ImKm=1K
85 84 oveq2d φXBYBmSm0˙IY0KImKm=IY0K1K
86 6 52 83 66 67 ringridmd φXBYBmSm0˙IY0K1K=IY0
87 85 86 eqtrd φXBYBmSm0˙IY0KImKm=IY0
88 79 82 87 3eqtr3d φXBYBmSm0˙IY0KImScalarWm=IY0
89 88 oveq1d φXBYBmSm0˙IY0KImScalarWm·˙Y=IY0·˙Y
90 64 78 89 3eqtr2d φXBYBmSm0˙Im·˙Y0·˙m·˙Y=IY0·˙Y
91 fveq1 X=m·˙YX0=m·˙Y0
92 91 fveq2d X=m·˙YIX0=Im·˙Y0
93 id X=m·˙YX=m·˙Y
94 92 93 oveq12d X=m·˙YIX0·˙X=Im·˙Y0·˙m·˙Y
95 94 eqeq1d X=m·˙YIX0·˙X=IY0·˙YIm·˙Y0·˙m·˙Y=IY0·˙Y
96 90 95 syl5ibrcom φXBYBmSm0˙X=m·˙YIX0·˙X=IY0·˙Y
97 96 expimpd φXBYBmSm0˙X=m·˙YIX0·˙X=IY0·˙Y
98 47 97 syld φXBYBmSX=m·˙YIX0·˙X=IY0·˙Y
99 98 rexlimdva φXBYBmSX=m·˙YIX0·˙X=IY0·˙Y
100 99 impr φXBYBmSX=m·˙YIX0·˙X=IY0·˙Y
101 13 neneqd φ¬X0=0˙
102 101 iffalsed φifX0=0˙XIX0·˙X=IX0·˙X
103 102 adantr φXBYBmSX=m·˙YifX0=0˙XIX0·˙X=IX0·˙X
104 14 neneqd φ¬Y0=0˙
105 104 iffalsed φifY0=0˙YIY0·˙Y=IY0·˙Y
106 105 adantr φXBYBmSX=m·˙YifY0=0˙YIY0·˙Y=IY0·˙Y
107 100 103 106 3eqtr4d φXBYBmSX=m·˙YifX0=0˙XIX0·˙X=ifY0=0˙YIY0·˙Y
108 fveq1 b=Xb0=X0
109 108 eqeq1d b=Xb0=0˙X0=0˙
110 id b=Xb=X
111 108 fveq2d b=XIb0=IX0
112 111 110 oveq12d b=XIb0·˙b=IX0·˙X
113 109 110 112 ifbieq12d b=Xifb0=0˙bIb0·˙b=ifX0=0˙XIX0·˙X
114 simprll φXBYBmSX=m·˙YXB
115 ovexd φXBYBmSX=m·˙YIX0·˙XV
116 114 115 ifexd φXBYBmSX=m·˙YifX0=0˙XIX0·˙XV
117 2 113 114 116 fvmptd3 φXBYBmSX=m·˙YFX=ifX0=0˙XIX0·˙X
118 fveq1 b=Yb0=Y0
119 118 eqeq1d b=Yb0=0˙Y0=0˙
120 id b=Yb=Y
121 118 fveq2d b=YIb0=IY0
122 121 120 oveq12d b=YIb0·˙b=IY0·˙Y
123 119 120 122 ifbieq12d b=Yifb0=0˙bIb0·˙b=ifY0=0˙YIY0·˙Y
124 simprlr φXBYBmSX=m·˙YYB
125 ovexd φXBYBmSX=m·˙YIY0·˙YV
126 124 125 ifexd φXBYBmSX=m·˙YifY0=0˙YIY0·˙YV
127 2 123 124 126 fvmptd3 φXBYBmSX=m·˙YFY=ifY0=0˙YIY0·˙Y
128 107 117 127 3eqtr4d φXBYBmSX=m·˙YFX=FY
129 15 128 sylan2b φX˙YFX=FY
130 1 4 3 6 5 9 prjspner φ˙ErB
131 130 adantr φFX=FY˙ErB
132 1 2 3 4 5 6 7 8 9 10 11 prjspner01 φX˙FX
133 132 adantr φFX=FYX˙FX
134 130 132 ercl2 φFXB
135 134 adantr φFX=FYFXB
136 131 135 erref φFX=FYFX˙FX
137 breq2 FX=FYFX˙FXFX˙FY
138 137 adantl φFX=FYFX˙FXFX˙FY
139 136 138 mpbid φFX=FYFX˙FY
140 1 2 3 4 5 6 7 8 9 10 12 prjspner01 φY˙FY
141 140 adantr φFX=FYY˙FY
142 131 139 141 ertr4d φFX=FYFX˙Y
143 131 133 142 ertrd φFX=FYX˙Y
144 129 143 impbida φX˙YFX=FY