Metamath Proof Explorer

Theorem prjspnfv01

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

Ref Expression
Hypotheses prjspnfv01.f ⊢ 𝐹 = ( 𝑏 ∈ 𝐵 ↦ if ( ( 𝑏 ‘ 0 ) = 0 , 𝑏 , ( ( 𝐼 ‘ ( 𝑏 ‘ 0 ) ) · 𝑏 ) ) )
prjspnfv01.b ⊢ 𝐵 = ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } )
prjspnfv01.w ⊢ 𝑊 = ( 𝐾 freeLMod ( 0 ... 𝑁 ) )
prjspnfv01.t ⊢ · = ( ·𝑠 ‘ 𝑊 )
prjspnfv01.0 ⊢ 0 = ( 0g ‘ 𝐾 )
prjspnfv01.1 ⊢ 1 = ( 1r ‘ 𝐾 )
prjspnfv01.i ⊢ 𝐼 = ( invr ‘ 𝐾 )
prjspnfv01.k ⊢ ( 𝜑 → 𝐾 ∈ DivRing )
prjspnfv01.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
prjspnfv01.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion prjspnfv01 ( 𝜑 → ( ( 𝐹 ‘ 𝑋 ) ‘ 0 ) = if ( ( 𝑋 ‘ 0 ) = 0 , 0 , 1 ) )

Proof

Step Hyp Ref Expression
1 prjspnfv01.f ⊢ 𝐹 = ( 𝑏 ∈ 𝐵 ↦ if ( ( 𝑏 ‘ 0 ) = 0 , 𝑏 , ( ( 𝐼 ‘ ( 𝑏 ‘ 0 ) ) · 𝑏 ) ) )
2 prjspnfv01.b ⊢ 𝐵 = ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } )
3 prjspnfv01.w ⊢ 𝑊 = ( 𝐾 freeLMod ( 0 ... 𝑁 ) )
4 prjspnfv01.t ⊢ · = ( ·𝑠 ‘ 𝑊 )
5 prjspnfv01.0 ⊢ 0 = ( 0g ‘ 𝐾 )
6 prjspnfv01.1 ⊢ 1 = ( 1r ‘ 𝐾 )
7 prjspnfv01.i ⊢ 𝐼 = ( invr ‘ 𝐾 )
8 prjspnfv01.k ⊢ ( 𝜑 → 𝐾 ∈ DivRing )
9 prjspnfv01.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
10 prjspnfv01.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
11 fveq1 ⊢ ( 𝑏 = 𝑋 → ( 𝑏 ‘ 0 ) = ( 𝑋 ‘ 0 ) )
12 11 eqeq1d ⊢ ( 𝑏 = 𝑋 → ( ( 𝑏 ‘ 0 ) = 0 ↔ ( 𝑋 ‘ 0 ) = 0 ) )
13 id ⊢ ( 𝑏 = 𝑋 → 𝑏 = 𝑋 )
14 11 fveq2d ⊢ ( 𝑏 = 𝑋 → ( 𝐼 ‘ ( 𝑏 ‘ 0 ) ) = ( 𝐼 ‘ ( 𝑋 ‘ 0 ) ) )
15 14 13 oveq12d ⊢ ( 𝑏 = 𝑋 → ( ( 𝐼 ‘ ( 𝑏 ‘ 0 ) ) · 𝑏 ) = ( ( 𝐼 ‘ ( 𝑋 ‘ 0 ) ) · 𝑋 ) )
16 12 13 15 ifbieq12d ⊢ ( 𝑏 = 𝑋 → if ( ( 𝑏 ‘ 0 ) = 0 , 𝑏 , ( ( 𝐼 ‘ ( 𝑏 ‘ 0 ) ) · 𝑏 ) ) = if ( ( 𝑋 ‘ 0 ) = 0 , 𝑋 , ( ( 𝐼 ‘ ( 𝑋 ‘ 0 ) ) · 𝑋 ) ) )
17 ovexd ⊢ ( 𝜑 → ( ( 𝐼 ‘ ( 𝑋 ‘ 0 ) ) · 𝑋 ) ∈ V )
18 10 17 ifexd ⊢ ( 𝜑 → if ( ( 𝑋 ‘ 0 ) = 0 , 𝑋 , ( ( 𝐼 ‘ ( 𝑋 ‘ 0 ) ) · 𝑋 ) ) ∈ V )
19 1 16 10 18 fvmptd3 ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑋 ) = if ( ( 𝑋 ‘ 0 ) = 0 , 𝑋 , ( ( 𝐼 ‘ ( 𝑋 ‘ 0 ) ) · 𝑋 ) ) )
20 19 fveq1d ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑋 ) ‘ 0 ) = ( if ( ( 𝑋 ‘ 0 ) = 0 , 𝑋 , ( ( 𝐼 ‘ ( 𝑋 ‘ 0 ) ) · 𝑋 ) ) ‘ 0 ) )
21 iffv ⊢ ( if ( ( 𝑋 ‘ 0 ) = 0 , 𝑋 , ( ( 𝐼 ‘ ( 𝑋 ‘ 0 ) ) · 𝑋 ) ) ‘ 0 ) = if ( ( 𝑋 ‘ 0 ) = 0 , ( 𝑋 ‘ 0 ) , ( ( ( 𝐼 ‘ ( 𝑋 ‘ 0 ) ) · 𝑋 ) ‘ 0 ) )
22 21 a1i ⊢ ( 𝜑 → ( if ( ( 𝑋 ‘ 0 ) = 0 , 𝑋 , ( ( 𝐼 ‘ ( 𝑋 ‘ 0 ) ) · 𝑋 ) ) ‘ 0 ) = if ( ( 𝑋 ‘ 0 ) = 0 , ( 𝑋 ‘ 0 ) , ( ( ( 𝐼 ‘ ( 𝑋 ‘ 0 ) ) · 𝑋 ) ‘ 0 ) ) )
23 simpr ⊢ ( ( 𝜑 ∧ ( 𝑋 ‘ 0 ) = 0 ) → ( 𝑋 ‘ 0 ) = 0 )
24 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
25 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
26 ovexd ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 ‘ 0 ) = 0 ) → ( 0 ... 𝑁 ) ∈ V )
27 ovexd ⊢ ( 𝜑 → ( 0 ... 𝑁 ) ∈ V )
28 10 2 eleqtrdi ⊢ ( 𝜑 → 𝑋 ∈ ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } ) )
29 28 eldifad ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝑊 ) )
30 3 25 24 frlmbasf ⊢ ( ( ( 0 ... 𝑁 ) ∈ V ∧ 𝑋 ∈ ( Base ‘ 𝑊 ) ) → 𝑋 : ( 0 ... 𝑁 ) ⟶ ( Base ‘ 𝐾 ) )
31 27 29 30 syl2anc ⊢ ( 𝜑 → 𝑋 : ( 0 ... 𝑁 ) ⟶ ( Base ‘ 𝐾 ) )
32 0elfz ⊢ ( 𝑁 ∈ ℕ0 → 0 ∈ ( 0 ... 𝑁 ) )
33 9 32 syl ⊢ ( 𝜑 → 0 ∈ ( 0 ... 𝑁 ) )
34 31 33 ffvelcdmd ⊢ ( 𝜑 → ( 𝑋 ‘ 0 ) ∈ ( Base ‘ 𝐾 ) )
35 neqne ⊢ ( ¬ ( 𝑋 ‘ 0 ) = 0 → ( 𝑋 ‘ 0 ) ≠ 0 )
36 25 5 7 drnginvrcl ⊢ ( ( 𝐾 ∈ DivRing ∧ ( 𝑋 ‘ 0 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑋 ‘ 0 ) ≠ 0 ) → ( 𝐼 ‘ ( 𝑋 ‘ 0 ) ) ∈ ( Base ‘ 𝐾 ) )
37 8 34 35 36 syl2an3an ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 ‘ 0 ) = 0 ) → ( 𝐼 ‘ ( 𝑋 ‘ 0 ) ) ∈ ( Base ‘ 𝐾 ) )
38 29 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 ‘ 0 ) = 0 ) → 𝑋 ∈ ( Base ‘ 𝑊 ) )
39 33 adantr ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 ‘ 0 ) = 0 ) → 0 ∈ ( 0 ... 𝑁 ) )
40 eqid ⊢ ( .r ‘ 𝐾 ) = ( .r ‘ 𝐾 )
41 3 24 25 26 37 38 39 4 40 frlmvscaval ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 ‘ 0 ) = 0 ) → ( ( ( 𝐼 ‘ ( 𝑋 ‘ 0 ) ) · 𝑋 ) ‘ 0 ) = ( ( 𝐼 ‘ ( 𝑋 ‘ 0 ) ) ( .r ‘ 𝐾 ) ( 𝑋 ‘ 0 ) ) )
42 25 5 40 6 7 drnginvrl ⊢ ( ( 𝐾 ∈ DivRing ∧ ( 𝑋 ‘ 0 ) ∈ ( Base ‘ 𝐾 ) ∧ ( 𝑋 ‘ 0 ) ≠ 0 ) → ( ( 𝐼 ‘ ( 𝑋 ‘ 0 ) ) ( .r ‘ 𝐾 ) ( 𝑋 ‘ 0 ) ) = 1 )
43 8 34 35 42 syl2an3an ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 ‘ 0 ) = 0 ) → ( ( 𝐼 ‘ ( 𝑋 ‘ 0 ) ) ( .r ‘ 𝐾 ) ( 𝑋 ‘ 0 ) ) = 1 )
44 41 43 eqtrd ⊢ ( ( 𝜑 ∧ ¬ ( 𝑋 ‘ 0 ) = 0 ) → ( ( ( 𝐼 ‘ ( 𝑋 ‘ 0 ) ) · 𝑋 ) ‘ 0 ) = 1 )
45 23 44 ifeq12da ⊢ ( 𝜑 → if ( ( 𝑋 ‘ 0 ) = 0 , ( 𝑋 ‘ 0 ) , ( ( ( 𝐼 ‘ ( 𝑋 ‘ 0 ) ) · 𝑋 ) ‘ 0 ) ) = if ( ( 𝑋 ‘ 0 ) = 0 , 0 , 1 ) )
46 20 22 45 3eqtrd ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑋 ) ‘ 0 ) = if ( ( 𝑋 ‘ 0 ) = 0 , 0 , 1 ) )