Metamath Proof Explorer

Theorem uvcn0

Description: A unit vector is nonzero. (Contributed by Steven Nguyen, 16-Jul-2023)

Ref Expression
Hypotheses uvcn0.u ⊢ U = R unitVec I
uvcn0.y ⊢ Y = R freeLMod I
uvcn0.b ⊢ B = Base Y
uvcn0.0 ⊢ 0 ˙ = 0 Y
Assertion uvcn0 ⊢ R ∈ NzRing ∧ I ∈ W ∧ J ∈ I → U ⁡ J ≠ 0 ˙

Proof

Step Hyp Ref Expression
1 uvcn0.u ⊢ U = R unitVec I
2 uvcn0.y ⊢ Y = R freeLMod I
3 uvcn0.b ⊢ B = Base Y
4 uvcn0.0 ⊢ 0 ˙ = 0 Y
5 eqid ⊢ 1 R = 1 R
6 eqid ⊢ 0 R = 0 R
7 5 6 nzrnz ⊢ R ∈ NzRing → 1 R ≠ 0 R
8 7 3ad2ant1 ⊢ R ∈ NzRing ∧ I ∈ W ∧ J ∈ I → 1 R ≠ 0 R
9 simp1 ⊢ R ∈ NzRing ∧ I ∈ W ∧ J ∈ I → R ∈ NzRing
10 simp2 ⊢ R ∈ NzRing ∧ I ∈ W ∧ J ∈ I → I ∈ W
11 simp3 ⊢ R ∈ NzRing ∧ I ∈ W ∧ J ∈ I → J ∈ I
12 1 9 10 11 5 uvcvv1 ⊢ R ∈ NzRing ∧ I ∈ W ∧ J ∈ I → U ⁡ J ⁡ J = 1 R
13 nzrring ⊢ R ∈ NzRing → R ∈ Ring
14 13 3ad2ant1 ⊢ R ∈ NzRing ∧ I ∈ W ∧ J ∈ I → R ∈ Ring
15 2 6 frlm0 ⊢ R ∈ Ring ∧ I ∈ W → I × 0 R = 0 Y
16 14 10 15 syl2anc ⊢ R ∈ NzRing ∧ I ∈ W ∧ J ∈ I → I × 0 R = 0 Y
17 16 4 syl6reqr ⊢ R ∈ NzRing ∧ I ∈ W ∧ J ∈ I → 0 ˙ = I × 0 R
18 17 fveq1d ⊢ R ∈ NzRing ∧ I ∈ W ∧ J ∈ I → 0 ˙ ⁡ J = I × 0 R ⁡ J
19 fvex ⊢ 0 R ∈ V
20 19 fvconst2 ⊢ J ∈ I → I × 0 R ⁡ J = 0 R
21 11 20 syl ⊢ R ∈ NzRing ∧ I ∈ W ∧ J ∈ I → I × 0 R ⁡ J = 0 R
22 18 21 eqtrd ⊢ R ∈ NzRing ∧ I ∈ W ∧ J ∈ I → 0 ˙ ⁡ J = 0 R
23 8 12 22 3netr4d ⊢ R ∈ NzRing ∧ I ∈ W ∧ J ∈ I → U ⁡ J ⁡ J ≠ 0 ˙ ⁡ J
24 fveq1 ⊢ U ⁡ J = 0 ˙ → U ⁡ J ⁡ J = 0 ˙ ⁡ J
25 24 adantl ⊢ R ∈ NzRing ∧ I ∈ W ∧ J ∈ I ∧ U ⁡ J = 0 ˙ → U ⁡ J ⁡ J = 0 ˙ ⁡ J
26 23 25 mteqand ⊢ R ∈ NzRing ∧ I ∈ W ∧ J ∈ I → U ⁡ J ≠ 0 ˙