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	$⊢ \underset{˙}{0} = 0_{Y}$
Assertion	uvcn0	$⊢ (R \in NzRing \land I \in W \land J \in I) \to U (J) \neq \underset{˙}{0}$

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	$⊢ \underset{˙}{0} = 0_{Y}$
5		eqid	$⊢ 1_{R} = 1_{R}$
6		eqid	$⊢ 0_{R} = 0_{R}$
7	5 6	nzrnz	$⊢ R \in NzRing \to 1_{R} \neq 0_{R}$
8	7	3ad2ant1	$⊢ (R \in NzRing \land I \in W \land J \in I) \to 1_{R} \neq 0_{R}$
9		simp1	$⊢ (R \in NzRing \land I \in W \land J \in I) \to R \in NzRing$
10		simp2	$⊢ (R \in NzRing \land I \in W \land J \in I) \to I \in W$
11		simp3	$⊢ (R \in NzRing \land I \in W \land J \in I) \to J \in I$
12	1 9 10 11 5	uvcvv1	$⊢ (R \in NzRing \land I \in W \land J \in I) \to U (J) (J) = 1_{R}$
13		nzrring	$⊢ R \in NzRing \to R \in Ring$
14	13	3ad2ant1	$⊢ (R \in NzRing \land I \in W \land J \in I) \to R \in Ring$
15	2 6 14 10 11	frlm0vald	$⊢ (R \in NzRing \land I \in W \land J \in I) \to 0_{Y} (J) = 0_{R}$
16	8 12 15	3netr4d	$⊢ (R \in NzRing \land I \in W \land J \in I) \to U (J) (J) \neq 0_{Y} (J)$
17		fveq1	$⊢ U (J) = 0_{Y} \to U (J) (J) = 0_{Y} (J)$
18	17	necon3i	$⊢ U (J) (J) \neq 0_{Y} (J) \to U (J) \neq 0_{Y}$
19	16 18	syl	$⊢ (R \in NzRing \land I \in W \land J \in I) \to U (J) \neq 0_{Y}$
20	4	a1i	$⊢ (R \in NzRing \land I \in W \land J \in I) \to \underset{˙}{0} = 0_{Y}$
21	19 20	neeqtrrd	$⊢ (R \in NzRing \land I \in W \land J \in I) \to U (J) \neq \underset{˙}{0}$

Metamath Proof Explorer