Metamath Proof Explorer

Theorem uvcendim

Description: In a nonzero ring, the number of unit vectors of a free module corresponds to the dimension of the free module. (Contributed by AV, 10-Mar-2019)

		Ref	Expression
	Hypothesis	uvcf1o.u	$⊢ U = R unitVec I$
	Assertion	uvcendim	$⊢ (R \in NzRing \land I \in W) \to I \approx ran U$

Proof

Step	Hyp	Ref	Expression
1		uvcf1o.u	$⊢ U = R unitVec I$
2	1	ovexi	$⊢ U \in V$
3	2	a1i	$⊢ (R \in NzRing \land I \in W) \to U \in V$
4	1	uvcf1o	$⊢ (R \in NzRing \land I \in W) \to U : I \underset{1-1 onto}{⟶} ran U$
5		f1oeq1	$⊢ U = u \to (U : I \underset{1-1 onto}{⟶} ran U \leftrightarrow u : I \underset{1-1 onto}{⟶} ran U)$
6	5	eqcoms	$⊢ u = U \to (U : I \underset{1-1 onto}{⟶} ran U \leftrightarrow u : I \underset{1-1 onto}{⟶} ran U)$
7	6	biimpd	$⊢ u = U \to (U : I \underset{1-1 onto}{⟶} ran U \to u : I \underset{1-1 onto}{⟶} ran U)$
8	7	a1i	$⊢ (R \in NzRing \land I \in W) \to (u = U \to (U : I \underset{1-1 onto}{⟶} ran U \to u : I \underset{1-1 onto}{⟶} ran U))$
9	4 8	syl7	$⊢ (R \in NzRing \land I \in W) \to (u = U \to ((R \in NzRing \land I \in W) \to u : I \underset{1-1 onto}{⟶} ran U))$
10	9	imp	$⊢ ((R \in NzRing \land I \in W) \land u = U) \to ((R \in NzRing \land I \in W) \to u : I \underset{1-1 onto}{⟶} ran U)$
11	3 10	spcimedv	$⊢ (R \in NzRing \land I \in W) \to ((R \in NzRing \land I \in W) \to \exists u u : I \underset{1-1 onto}{⟶} ran U)$
12	11	pm2.43i	$⊢ (R \in NzRing \land I \in W) \to \exists u u : I \underset{1-1 onto}{⟶} ran U$
13		bren	$⊢ I \approx ran U \leftrightarrow \exists u u : I \underset{1-1 onto}{⟶} ran U$
14	12 13	sylibr	$⊢ (R \in NzRing \land I \in W) \to I \approx ran U$