Metamath Proof Explorer


Theorem prjspnvs

Description: A nonzero multiple of a vector is equivalent to the vector. This converts the equivalence relation used in prjspvs (see prjspnerlem ). (Contributed by SN, 8-Aug-2024)

Ref Expression
Hypotheses prjspnvs.e = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥𝐵𝑦𝐵 ) ∧ ∃ 𝑙𝑆 𝑥 = ( 𝑙 · 𝑦 ) ) }
prjspnvs.w 𝑊 = ( 𝐾 freeLMod ( 0 ... 𝑁 ) )
prjspnvs.b 𝐵 = ( ( Base ‘ 𝑊 ) ∖ { ( 0g𝑊 ) } )
prjspnvs.s 𝑆 = ( Base ‘ 𝐾 )
prjspnvs.x · = ( ·𝑠𝑊 )
prjspnvs.0 0 = ( 0g𝐾 )
prjspnvs.k ( 𝜑𝐾 ∈ DivRing )
prjspnvs.1 ( 𝜑𝑋𝐵 )
prjspnvs.2 ( 𝜑𝐶𝑆 )
prjspnvs.3 ( 𝜑𝐶0 )
Assertion prjspnvs ( 𝜑 → ( 𝐶 · 𝑋 ) 𝑋 )

Proof

Step Hyp Ref Expression
1 prjspnvs.e = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥𝐵𝑦𝐵 ) ∧ ∃ 𝑙𝑆 𝑥 = ( 𝑙 · 𝑦 ) ) }
2 prjspnvs.w 𝑊 = ( 𝐾 freeLMod ( 0 ... 𝑁 ) )
3 prjspnvs.b 𝐵 = ( ( Base ‘ 𝑊 ) ∖ { ( 0g𝑊 ) } )
4 prjspnvs.s 𝑆 = ( Base ‘ 𝐾 )
5 prjspnvs.x · = ( ·𝑠𝑊 )
6 prjspnvs.0 0 = ( 0g𝐾 )
7 prjspnvs.k ( 𝜑𝐾 ∈ DivRing )
8 prjspnvs.1 ( 𝜑𝑋𝐵 )
9 prjspnvs.2 ( 𝜑𝐶𝑆 )
10 prjspnvs.3 ( 𝜑𝐶0 )
11 ovexd ( 𝜑 → ( 0 ... 𝑁 ) ∈ V )
12 2 frlmlvec ( ( 𝐾 ∈ DivRing ∧ ( 0 ... 𝑁 ) ∈ V ) → 𝑊 ∈ LVec )
13 7 11 12 syl2anc ( 𝜑𝑊 ∈ LVec )
14 nelsn ( 𝐶0 → ¬ 𝐶 ∈ { 0 } )
15 10 14 syl ( 𝜑 → ¬ 𝐶 ∈ { 0 } )
16 9 15 eldifd ( 𝜑𝐶 ∈ ( 𝑆 ∖ { 0 } ) )
17 2 frlmsca ( ( 𝐾 ∈ DivRing ∧ ( 0 ... 𝑁 ) ∈ V ) → 𝐾 = ( Scalar ‘ 𝑊 ) )
18 7 11 17 syl2anc ( 𝜑𝐾 = ( Scalar ‘ 𝑊 ) )
19 18 fveq2d ( 𝜑 → ( Base ‘ 𝐾 ) = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
20 4 19 syl5eq ( 𝜑𝑆 = ( Base ‘ ( Scalar ‘ 𝑊 ) ) )
21 18 fveq2d ( 𝜑 → ( 0g𝐾 ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
22 6 21 syl5eq ( 𝜑0 = ( 0g ‘ ( Scalar ‘ 𝑊 ) ) )
23 22 sneqd ( 𝜑 → { 0 } = { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } )
24 20 23 difeq12d ( 𝜑 → ( 𝑆 ∖ { 0 } ) = ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) )
25 16 24 eleqtrd ( 𝜑𝐶 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) )
26 eqid { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥𝐵𝑦𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 · 𝑦 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥𝐵𝑦𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 · 𝑦 ) ) }
27 eqid ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
28 eqid ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
29 eqid ( 0g ‘ ( Scalar ‘ 𝑊 ) ) = ( 0g ‘ ( Scalar ‘ 𝑊 ) )
30 26 3 27 5 28 29 prjspvs ( ( 𝑊 ∈ LVec ∧ 𝑋𝐵𝐶 ∈ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∖ { ( 0g ‘ ( Scalar ‘ 𝑊 ) ) } ) ) → ( 𝐶 · 𝑋 ) { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥𝐵𝑦𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 · 𝑦 ) ) } 𝑋 )
31 13 8 25 30 syl3anc ( 𝜑 → ( 𝐶 · 𝑋 ) { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥𝐵𝑦𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 · 𝑦 ) ) } 𝑋 )
32 1 2 3 4 5 prjspnerlem ( 𝐾 ∈ DivRing → = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥𝐵𝑦𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 · 𝑦 ) ) } )
33 7 32 syl ( 𝜑 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥𝐵𝑦𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 · 𝑦 ) ) } )
34 33 breqd ( 𝜑 → ( ( 𝐶 · 𝑋 ) 𝑋 ↔ ( 𝐶 · 𝑋 ) { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥𝐵𝑦𝐵 ) ∧ ∃ 𝑙 ∈ ( Base ‘ ( Scalar ‘ 𝑊 ) ) 𝑥 = ( 𝑙 · 𝑦 ) ) } 𝑋 ) )
35 31 34 mpbird ( 𝜑 → ( 𝐶 · 𝑋 ) 𝑋 )