Metamath Proof Explorer

Theorem 0prjspnlem

Description: Lemma for 0prjspn . The given unit vector is a nonzero vector. (Contributed by Steven Nguyen, 16-Jul-2023)

Ref Expression
Hypotheses 0prjspnlem.b ⊢ 𝐵 = ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } )
0prjspnlem.w ⊢ 𝑊 = ( 𝐾 freeLMod ( 0 ... 0 ) )
0prjspnlem.1 ⊢ 1 = ( ( 𝐾 unitVec ( 0 ... 0 ) ) ‘ 0 )
Assertion 0prjspnlem ( 𝐾 ∈ DivRing → 1 ∈ 𝐵 )

Proof

Step Hyp Ref Expression
1 0prjspnlem.b ⊢ 𝐵 = ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } )
2 0prjspnlem.w ⊢ 𝑊 = ( 𝐾 freeLMod ( 0 ... 0 ) )
3 0prjspnlem.1 ⊢ 1 = ( ( 𝐾 unitVec ( 0 ... 0 ) ) ‘ 0 )
4 drngnzr ⊢ ( 𝐾 ∈ DivRing → 𝐾 ∈ NzRing )
5 ovex ⊢ ( 0 ... 0 ) ∈ V
6 c0ex ⊢ 0 ∈ V
7 6 snid ⊢ 0 ∈ { 0 }
8 fz0sn ⊢ ( 0 ... 0 ) = { 0 }
9 7 8 eleqtrri ⊢ 0 ∈ ( 0 ... 0 )
10 nzrring ⊢ ( 𝐾 ∈ NzRing → 𝐾 ∈ Ring )
11 eqid ⊢ ( 𝐾 unitVec ( 0 ... 0 ) ) = ( 𝐾 unitVec ( 0 ... 0 ) )
12 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
13 11 2 12 uvccl ⊢ ( ( 𝐾 ∈ Ring ∧ ( 0 ... 0 ) ∈ V ∧ 0 ∈ ( 0 ... 0 ) ) → ( ( 𝐾 unitVec ( 0 ... 0 ) ) ‘ 0 ) ∈ ( Base ‘ 𝑊 ) )
14 10 13 syl3an1 ⊢ ( ( 𝐾 ∈ NzRing ∧ ( 0 ... 0 ) ∈ V ∧ 0 ∈ ( 0 ... 0 ) ) → ( ( 𝐾 unitVec ( 0 ... 0 ) ) ‘ 0 ) ∈ ( Base ‘ 𝑊 ) )
15 eqid ⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
16 11 2 12 15 uvcn0 ⊢ ( ( 𝐾 ∈ NzRing ∧ ( 0 ... 0 ) ∈ V ∧ 0 ∈ ( 0 ... 0 ) ) → ( ( 𝐾 unitVec ( 0 ... 0 ) ) ‘ 0 ) ≠ ( 0g ‘ 𝑊 ) )
17 eldifsn ⊢ ( ( ( 𝐾 unitVec ( 0 ... 0 ) ) ‘ 0 ) ∈ ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } ) ↔ ( ( ( 𝐾 unitVec ( 0 ... 0 ) ) ‘ 0 ) ∈ ( Base ‘ 𝑊 ) ∧ ( ( 𝐾 unitVec ( 0 ... 0 ) ) ‘ 0 ) ≠ ( 0g ‘ 𝑊 ) ) )
18 14 16 17 sylanbrc ⊢ ( ( 𝐾 ∈ NzRing ∧ ( 0 ... 0 ) ∈ V ∧ 0 ∈ ( 0 ... 0 ) ) → ( ( 𝐾 unitVec ( 0 ... 0 ) ) ‘ 0 ) ∈ ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } ) )
19 5 9 18 mp3an23 ⊢ ( 𝐾 ∈ NzRing → ( ( 𝐾 unitVec ( 0 ... 0 ) ) ‘ 0 ) ∈ ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } ) )
20 4 19 syl ⊢ ( 𝐾 ∈ DivRing → ( ( 𝐾 unitVec ( 0 ... 0 ) ) ‘ 0 ) ∈ ( ( Base ‘ 𝑊 ) ∖ { ( 0g ‘ 𝑊 ) } ) )
21 20 3 1 3eltr4g ⊢ ( 𝐾 ∈ DivRing → 1 ∈ 𝐵 )