Metamath Proof Explorer

Theorem prjspner01

Description: Any vector is equivalent to a vector whose zeroth coordinate is .0. or .1. (proof of the equivalence). (Contributed by SN, 13-Aug-2023)

Ref Expression
Hypotheses prjspner01.e ⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝑆 𝑥 = ( 𝑙 · 𝑦 ) ) }
prjspner01.f ⊢ 𝐹 = ( 𝑏 ∈ 𝐵 ↦ if ( ( 𝑏 ‘ 0 ) = 0 , 𝑏 , ( ( 𝐼 ‘ ( 𝑏 ‘ 0 ) ) · 𝑏 ) ) )
prjspner01.b ⊢ 𝐵 = ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } )
prjspner01.w ⊢ 𝑊 = ( 𝐾 freeLMod ( 0 ... 𝑁 ) )
prjspner01.t ⊢ · = ( ·𝑠 ‘ 𝑊 )
prjspner01.s ⊢ 𝑆 = ( Base ‘ 𝐾 )
prjspner01.0 ⊢ 0 = ( 0g ‘ 𝐾 )
prjspner01.i ⊢ 𝐼 = ( invr ‘ 𝐾 )
prjspner01.k ⊢ ( 𝜑 → 𝐾 ∈ DivRing )
prjspner01.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
prjspner01.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion prjspner01 ( 𝜑 → 𝑋 ∼ ( 𝐹 ‘ 𝑋 ) )

Proof

Step Hyp Ref Expression
1 prjspner01.e ⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ∧ ∃ 𝑙 ∈ 𝑆 𝑥 = ( 𝑙 · 𝑦 ) ) }
2 prjspner01.f ⊢ 𝐹 = ( 𝑏 ∈ 𝐵 ↦ if ( ( 𝑏 ‘ 0 ) = 0 , 𝑏 , ( ( 𝐼 ‘ ( 𝑏 ‘ 0 ) ) · 𝑏 ) ) )
3 prjspner01.b ⊢ 𝐵 = ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } )
4 prjspner01.w ⊢ 𝑊 = ( 𝐾 freeLMod ( 0 ... 𝑁 ) )
5 prjspner01.t ⊢ · = ( ·𝑠 ‘ 𝑊 )
6 prjspner01.s ⊢ 𝑆 = ( Base ‘ 𝐾 )
7 prjspner01.0 ⊢ 0 = ( 0g ‘ 𝐾 )
8 prjspner01.i ⊢ 𝐼 = ( invr ‘ 𝐾 )
9 prjspner01.k ⊢ ( 𝜑 → 𝐾 ∈ DivRing )
10 prjspner01.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
11 prjspner01.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
12 1 4 3 6 5 9 prjspner ⊢ ( 𝜑 → ∼ Er 𝐵 )
13 12 11 erref ⊢ ( 𝜑 → 𝑋 ∼ 𝑋 )
14 13 adantr ⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ 0 ) = 0 ) → 𝑋 ∼ 𝑋 )
15 12 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 ‘ 0 ) = 0 ) → ∼ Er 𝐵 )
16 9 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 ‘ 0 ) = 0 ) → 𝐾 ∈ DivRing )
17 11 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 ‘ 0 ) = 0 ) → 𝑋 ∈ 𝐵 )
18 ovexd ⊢ ( 𝜑 → ( 0 ... 𝑁 ) ∈ V )
19 11 3 eleqtrdi ⊢ ( 𝜑 → 𝑋 ∈ ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } ) )
20 19 eldifad ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝑊 ) )
21 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
22 4 6 21 frlmbasf ⊢ ( ( ( 0 ... 𝑁 ) ∈ V ∧ 𝑋 ∈ ( Base ‘ 𝑊 ) ) → 𝑋 : ( 0 ... 𝑁 ) ⟶ 𝑆 )
23 18 20 22 syl2anc ⊢ ( 𝜑 → 𝑋 : ( 0 ... 𝑁 ) ⟶ 𝑆 )
24 0elfz ⊢ ( 𝑁 ∈ ℕ0 → 0 ∈ ( 0 ... 𝑁 ) )
25 10 24 syl ⊢ ( 𝜑 → 0 ∈ ( 0 ... 𝑁 ) )
26 23 25 ffvelcdmd ⊢ ( 𝜑 → ( 𝑋 ‘ 0 ) ∈ 𝑆 )
27 neqne ⊢ ( ¬ ( 𝑋 ‘ 0 ) = 0 → ( 𝑋 ‘ 0 ) ≠ 0 )
28 6 7 8 drnginvrcl ⊢ ( ( 𝐾 ∈ DivRing ∧ ( 𝑋 ‘ 0 ) ∈ 𝑆 ∧ ( 𝑋 ‘ 0 ) ≠ 0 ) → ( 𝐼 ‘ ( 𝑋 ‘ 0 ) ) ∈ 𝑆 )
29 9 26 27 28 syl2an3an ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 ‘ 0 ) = 0 ) → ( 𝐼 ‘ ( 𝑋 ‘ 0 ) ) ∈ 𝑆 )
30 6 7 8 drnginvrn0 ⊢ ( ( 𝐾 ∈ DivRing ∧ ( 𝑋 ‘ 0 ) ∈ 𝑆 ∧ ( 𝑋 ‘ 0 ) ≠ 0 ) → ( 𝐼 ‘ ( 𝑋 ‘ 0 ) ) ≠ 0 )
31 9 26 27 30 syl2an3an ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 ‘ 0 ) = 0 ) → ( 𝐼 ‘ ( 𝑋 ‘ 0 ) ) ≠ 0 )
32 1 4 3 6 5 7 16 17 29 31 prjspnvs ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 ‘ 0 ) = 0 ) → ( ( 𝐼 ‘ ( 𝑋 ‘ 0 ) ) · 𝑋 ) ∼ 𝑋 )
33 15 32 ersym ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 ‘ 0 ) = 0 ) → 𝑋 ∼ ( ( 𝐼 ‘ ( 𝑋 ‘ 0 ) ) · 𝑋 ) )
34 14 33 ifpimpda ⊢ ( 𝜑 → if- ( ( 𝑋 ‘ 0 ) = 0 , 𝑋 ∼ 𝑋 , 𝑋 ∼ ( ( 𝐼 ‘ ( 𝑋 ‘ 0 ) ) · 𝑋 ) ) )
35 brif2 ⊢ ( 𝑋 ∼ if ( ( 𝑋 ‘ 0 ) = 0 , 𝑋 , ( ( 𝐼 ‘ ( 𝑋 ‘ 0 ) ) · 𝑋 ) ) ↔ if- ( ( 𝑋 ‘ 0 ) = 0 , 𝑋 ∼ 𝑋 , 𝑋 ∼ ( ( 𝐼 ‘ ( 𝑋 ‘ 0 ) ) · 𝑋 ) ) )
36 34 35 sylibr ⊢ ( 𝜑 → 𝑋 ∼ if ( ( 𝑋 ‘ 0 ) = 0 , 𝑋 , ( ( 𝐼 ‘ ( 𝑋 ‘ 0 ) ) · 𝑋 ) ) )
37 fveq1 ⊢ ( 𝑏 = 𝑋 → ( 𝑏 ‘ 0 ) = ( 𝑋 ‘ 0 ) )
38 37 eqeq1d ⊢ ( 𝑏 = 𝑋 → ( ( 𝑏 ‘ 0 ) = 0 ↔ ( 𝑋 ‘ 0 ) = 0 ) )
39 id ⊢ ( 𝑏 = 𝑋 → 𝑏 = 𝑋 )
40 37 fveq2d ⊢ ( 𝑏 = 𝑋 → ( 𝐼 ‘ ( 𝑏 ‘ 0 ) ) = ( 𝐼 ‘ ( 𝑋 ‘ 0 ) ) )
41 40 39 oveq12d ⊢ ( 𝑏 = 𝑋 → ( ( 𝐼 ‘ ( 𝑏 ‘ 0 ) ) · 𝑏 ) = ( ( 𝐼 ‘ ( 𝑋 ‘ 0 ) ) · 𝑋 ) )
42 38 39 41 ifbieq12d ⊢ ( 𝑏 = 𝑋 → if ( ( 𝑏 ‘ 0 ) = 0 , 𝑏 , ( ( 𝐼 ‘ ( 𝑏 ‘ 0 ) ) · 𝑏 ) ) = if ( ( 𝑋 ‘ 0 ) = 0 , 𝑋 , ( ( 𝐼 ‘ ( 𝑋 ‘ 0 ) ) · 𝑋 ) ) )
43 ovexd ⊢ ( 𝜑 → ( ( 𝐼 ‘ ( 𝑋 ‘ 0 ) ) · 𝑋 ) ∈ V )
44 11 43 ifexd ⊢ ( 𝜑 → if ( ( 𝑋 ‘ 0 ) = 0 , 𝑋 , ( ( 𝐼 ‘ ( 𝑋 ‘ 0 ) ) · 𝑋 ) ) ∈ V )
45 2 42 11 44 fvmptd3 ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) = if ( ( 𝑋 ‘ 0 ) = 0 , 𝑋 , ( ( 𝐼 ‘ ( 𝑋 ‘ 0 ) ) · 𝑋 ) ) )
46 36 45 breqtrrd ⊢ ( 𝜑 → 𝑋 ∼ ( 𝐹 ‘ 𝑋 ) )