uvcff

Description: Domain and codomain of the unit vector generator; ring condition required to be sure 1 and 0 are actually in the ring. (Contributed by Stefan O'Rear, 1-Feb-2015) (Proof shortened by AV, 21-Jul-2019)

	Ref	Expression
Hypotheses	uvcff.u	$⊢ U = R unitVec I$
	uvcff.y	$⊢ Y = R freeLMod I$
	uvcff.b	$⊢ B = {Base}_{Y}$
Assertion	uvcff	$⊢ (R \in Ring \land I \in W) \to U : I ⟶ 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		eqid	$⊢ 1_{R} = 1_{R}$
5		eqid	$⊢ 0_{R} = 0_{R}$
6	1 4 5	uvcfval	$⊢ (R \in Ring \land I \in W) \to U = (i \in I ⟼ (j \in I ⟼ if (j = i, 1_{R}, 0_{R})))$
7		eqid	$⊢ {Base}_{R} = {Base}_{R}$
8	7 4	ringidcl	$⊢ R \in Ring \to 1_{R} \in {Base}_{R}$
9	7 5	ring0cl	$⊢ R \in Ring \to 0_{R} \in {Base}_{R}$
10	8 9	ifcld	$⊢ R \in Ring \to if (j = i, 1_{R}, 0_{R}) \in {Base}_{R}$
11	10	ad3antrrr	$⊢ (((R \in Ring \land I \in W) \land i \in I) \land j \in I) \to if (j = i, 1_{R}, 0_{R}) \in {Base}_{R}$
12	11	fmpttd	$⊢ ((R \in Ring \land I \in W) \land i \in I) \to (j \in I ⟼ if (j = i, 1_{R}, 0_{R})) : I ⟶ {Base}_{R}$
13		fvex	$⊢ {Base}_{R} \in V$
14		elmapg	$⊢ ({Base}_{R} \in V \land I \in W) \to ((j \in I ⟼ if (j = i, 1_{R}, 0_{R})) \in ({Base}_{R}^{I}) \leftrightarrow (j \in I ⟼ if (j = i, 1_{R}, 0_{R})) : I ⟶ {Base}_{R})$
15	13 14	mpan	$⊢ I \in W \to ((j \in I ⟼ if (j = i, 1_{R}, 0_{R})) \in ({Base}_{R}^{I}) \leftrightarrow (j \in I ⟼ if (j = i, 1_{R}, 0_{R})) : I ⟶ {Base}_{R})$
16	15	ad2antlr	$⊢ ((R \in Ring \land I \in W) \land i \in I) \to ((j \in I ⟼ if (j = i, 1_{R}, 0_{R})) \in ({Base}_{R}^{I}) \leftrightarrow (j \in I ⟼ if (j = i, 1_{R}, 0_{R})) : I ⟶ {Base}_{R})$
17	12 16	mpbird	$⊢ ((R \in Ring \land I \in W) \land i \in I) \to (j \in I ⟼ if (j = i, 1_{R}, 0_{R})) \in ({Base}_{R}^{I})$
18		mptexg	$⊢ I \in W \to (j \in I ⟼ if (j = i, 1_{R}, 0_{R})) \in V$
19	18	ad2antlr	$⊢ ((R \in Ring \land I \in W) \land i \in I) \to (j \in I ⟼ if (j = i, 1_{R}, 0_{R})) \in V$
20		funmpt	$⊢ Fun (j \in I ⟼ if (j = i, 1_{R}, 0_{R}))$
21	20	a1i	$⊢ ((R \in Ring \land I \in W) \land i \in I) \to Fun (j \in I ⟼ if (j = i, 1_{R}, 0_{R}))$
22		fvex	$⊢ 0_{R} \in V$
23	22	a1i	$⊢ ((R \in Ring \land I \in W) \land i \in I) \to 0_{R} \in V$
24		snfi	$⊢ \{i\} \in Fin$
25	24	a1i	$⊢ ((R \in Ring \land I \in W) \land i \in I) \to \{i\} \in Fin$
26		eldifsni	$⊢ j \in (I ∖ \{i\}) \to j \neq i$
27	26	adantl	$⊢ (((R \in Ring \land I \in W) \land i \in I) \land j \in (I ∖ \{i\})) \to j \neq i$
28	27	neneqd	$⊢ (((R \in Ring \land I \in W) \land i \in I) \land j \in (I ∖ \{i\})) \to \neg j = i$
29	28	iffalsed	$⊢ (((R \in Ring \land I \in W) \land i \in I) \land j \in (I ∖ \{i\})) \to if (j = i, 1_{R}, 0_{R}) = 0_{R}$
30		simplr	$⊢ ((R \in Ring \land I \in W) \land i \in I) \to I \in W$
31	29 30	suppss2	$⊢ ((R \in Ring \land I \in W) \land i \in I) \to (j \in I ⟼ if (j = i, 1_{R}, 0_{R})) supp 0_{R} \subseteq \{i\}$
32		suppssfifsupp	$⊢ (((j \in I ⟼ if (j = i, 1_{R}, 0_{R})) \in V \land Fun (j \in I ⟼ if (j = i, 1_{R}, 0_{R})) \land 0_{R} \in V) \land (\{i\} \in Fin \land (j \in I ⟼ if (j = i, 1_{R}, 0_{R})) supp 0_{R} \subseteq \{i\})) \to {finSupp}_{0_{R}} ((j \in I ⟼ if (j = i, 1_{R}, 0_{R})))$
33	19 21 23 25 31 32	syl32anc	$⊢ ((R \in Ring \land I \in W) \land i \in I) \to {finSupp}_{0_{R}} ((j \in I ⟼ if (j = i, 1_{R}, 0_{R})))$
34	2 7 5 3	frlmelbas	$⊢ (R \in Ring \land I \in W) \to ((j \in I ⟼ if (j = i, 1_{R}, 0_{R})) \in B \leftrightarrow ((j \in I ⟼ if (j = i, 1_{R}, 0_{R})) \in ({Base}_{R}^{I}) \land {finSupp}_{0_{R}} ((j \in I ⟼ if (j = i, 1_{R}, 0_{R})))))$
35	34	adantr	$⊢ ((R \in Ring \land I \in W) \land i \in I) \to ((j \in I ⟼ if (j = i, 1_{R}, 0_{R})) \in B \leftrightarrow ((j \in I ⟼ if (j = i, 1_{R}, 0_{R})) \in ({Base}_{R}^{I}) \land {finSupp}_{0_{R}} ((j \in I ⟼ if (j = i, 1_{R}, 0_{R})))))$
36	17 33 35	mpbir2and	$⊢ ((R \in Ring \land I \in W) \land i \in I) \to (j \in I ⟼ if (j = i, 1_{R}, 0_{R})) \in B$
37	6 36	fmpt3d	$⊢ (R \in Ring \land I \in W) \to U : I ⟶ B$

Metamath Proof Explorer

Theorem uvcff

Proof