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 ⊢ B = Base W ∖ 0 W
0prjspnlem.w ⊢ W = K freeLMod 0 … 0
0prjspnlem.1 ⊢ 1 ˙ = K unitVec 0 … 0 ⁡ 0
Assertion 0prjspnlem ⊢ K ∈ DivRing → 1 ˙ ∈ B

Proof

Step Hyp Ref Expression
1 0prjspnlem.b ⊢ B = Base W ∖ 0 W
2 0prjspnlem.w ⊢ W = K freeLMod 0 … 0
3 0prjspnlem.1 ⊢ 1 ˙ = K unitVec 0 … 0 ⁡ 0
4 drngnzr ⊢ K ∈ DivRing → K ∈ 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 ⊢ K ∈ NzRing → K ∈ Ring
11 eqid ⊢ K unitVec 0 … 0 = K unitVec 0 … 0
12 eqid ⊢ Base W = Base W
13 11 2 12 uvccl ⊢ K ∈ Ring ∧ 0 … 0 ∈ V ∧ 0 ∈ 0 … 0 → K unitVec 0 … 0 ⁡ 0 ∈ Base W
14 10 13 syl3an1 ⊢ K ∈ NzRing ∧ 0 … 0 ∈ V ∧ 0 ∈ 0 … 0 → K unitVec 0 … 0 ⁡ 0 ∈ Base W
15 eqid ⊢ 0 W = 0 W
16 11 2 12 15 uvcn0 ⊢ K ∈ NzRing ∧ 0 … 0 ∈ V ∧ 0 ∈ 0 … 0 → K unitVec 0 … 0 ⁡ 0 ≠ 0 W
17 eldifsn ⊢ K unitVec 0 … 0 ⁡ 0 ∈ Base W ∖ 0 W ↔ K unitVec 0 … 0 ⁡ 0 ∈ Base W ∧ K unitVec 0 … 0 ⁡ 0 ≠ 0 W
18 14 16 17 sylanbrc ⊢ K ∈ NzRing ∧ 0 … 0 ∈ V ∧ 0 ∈ 0 … 0 → K unitVec 0 … 0 ⁡ 0 ∈ Base W ∖ 0 W
19 5 9 18 mp3an23 ⊢ K ∈ NzRing → K unitVec 0 … 0 ⁡ 0 ∈ Base W ∖ 0 W
20 4 19 syl ⊢ K ∈ DivRing → K unitVec 0 … 0 ⁡ 0 ∈ Base W ∖ 0 W
21 20 3 1 3eltr4g ⊢ K ∈ DivRing → 1 ˙ ∈ B