uvcf1

Description: In a nonzero ring, each unit vector is different. (Contributed by Stefan O'Rear, 7-Feb-2015) (Revised by Mario Carneiro, 14-Jun-2015)

	Ref	Expression
Hypotheses	uvcff.u	$⊢ U = R unitVec I$
	uvcff.y	$⊢ Y = R freeLMod I$
	uvcff.b	$⊢ B = {Base}_{Y}$
Assertion	uvcf1	$⊢ (R \in NzRing \land I \in W) \to U : I \underset{1-1}{⟶} B$

Proof

Step	Hyp	Ref	Expression
1		uvcff.u	$⊢ U = R unitVec I$
2		uvcff.y	$⊢ Y = R freeLMod I$
3		uvcff.b	$⊢ B = {Base}_{Y}$
4		nzrring	$⊢ R \in NzRing \to R \in Ring$
5	1 2 3	uvcff	$⊢ (R \in Ring \land I \in W) \to U : I ⟶ B$
6	4 5	sylan	$⊢ (R \in NzRing \land I \in W) \to U : I ⟶ B$
7		eqid	$⊢ 1_{R} = 1_{R}$
8		eqid	$⊢ 0_{R} = 0_{R}$
9	7 8	nzrnz	$⊢ R \in NzRing \to 1_{R} \neq 0_{R}$
10	9	ad3antrrr	$⊢ (((R \in NzRing \land I \in W) \land (i \in I \land j \in I)) \land i \neq j) \to 1_{R} \neq 0_{R}$
11	4	ad3antrrr	$⊢ (((R \in NzRing \land I \in W) \land (i \in I \land j \in I)) \land i \neq j) \to R \in Ring$
12		simpllr	$⊢ (((R \in NzRing \land I \in W) \land (i \in I \land j \in I)) \land i \neq j) \to I \in W$
13		simplrl	$⊢ (((R \in NzRing \land I \in W) \land (i \in I \land j \in I)) \land i \neq j) \to i \in I$
14	1 11 12 13 7	uvcvv1	$⊢ (((R \in NzRing \land I \in W) \land (i \in I \land j \in I)) \land i \neq j) \to U (i) (i) = 1_{R}$
15		simplrr	$⊢ (((R \in NzRing \land I \in W) \land (i \in I \land j \in I)) \land i \neq j) \to j \in I$
16		simpr	$⊢ (((R \in NzRing \land I \in W) \land (i \in I \land j \in I)) \land i \neq j) \to i \neq j$
17	16	necomd	$⊢ (((R \in NzRing \land I \in W) \land (i \in I \land j \in I)) \land i \neq j) \to j \neq i$
18	1 11 12 15 13 17 8	uvcvv0	$⊢ (((R \in NzRing \land I \in W) \land (i \in I \land j \in I)) \land i \neq j) \to U (j) (i) = 0_{R}$
19	10 14 18	3netr4d	$⊢ (((R \in NzRing \land I \in W) \land (i \in I \land j \in I)) \land i \neq j) \to U (i) (i) \neq U (j) (i)$
20		fveq1	$⊢ U (i) = U (j) \to U (i) (i) = U (j) (i)$
21	20	necon3i	$⊢ U (i) (i) \neq U (j) (i) \to U (i) \neq U (j)$
22	19 21	syl	$⊢ (((R \in NzRing \land I \in W) \land (i \in I \land j \in I)) \land i \neq j) \to U (i) \neq U (j)$
23	22	ex	$⊢ ((R \in NzRing \land I \in W) \land (i \in I \land j \in I)) \to (i \neq j \to U (i) \neq U (j))$
24	23	necon4d	$⊢ ((R \in NzRing \land I \in W) \land (i \in I \land j \in I)) \to (U (i) = U (j) \to i = j)$
25	24	ralrimivva	$⊢ (R \in NzRing \land I \in W) \to \forall i \in I \forall j \in I (U (i) = U (j) \to i = j)$
26		dff13	$⊢ U : I \underset{1-1}{⟶} B \leftrightarrow (U : I ⟶ B \land \forall i \in I \forall j \in I (U (i) = U (j) \to i = j))$
27	6 25 26	sylanbrc	$⊢ (R \in NzRing \land I \in W) \to U : I \underset{1-1}{⟶} B$

Metamath Proof Explorer

Theorem uvcf1

Proof