Theorem uvcfval

Description: Value of the unit-vector generator for a free module. (Contributed by Stefan O'Rear, 1-Feb-2015)

	Ref	Expression
Hypotheses	uvcfval.u	$$⊢U=R\mathrm{unitVec}I$$
	uvcfval.o	$$⊢\underset{\dot{}}{1}=1_R$$
	uvcfval.z	$$⊢\underset{\dot{}}{0}=0_R$$
Assertion	uvcfval	$$⊢\left(R\in V\wedge I\in W\right)\to U=\left(j\in I⟼\left(k\in I⟼if\left(k=j,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		uvcfval.u	$$⊢U=R\mathrm{unitVec}I$$
2		uvcfval.o	$$⊢\underset{\dot{}}{1}=1_R$$
3		uvcfval.z	$$⊢\underset{\dot{}}{0}=0_R$$
4		elex	$$⊢R\in V\to R\in \mathrm{V}$$
5		elex	$$⊢I\in W\to I\in \mathrm{V}$$
6		df-uvc	$$⊢\mathrm{unitVec}=\left(r\in \mathrm{V},i\in \mathrm{V}⟼\left(j\in i⟼\left(k\in i⟼if\left(k=j,1_r,0_r\right)\right)\right)\right)$$
7	6	a1i	$$⊢\left(R\in \mathrm{V}\wedge I\in \mathrm{V}\right)\to \mathrm{unitVec}=\left(r\in \mathrm{V},i\in \mathrm{V}⟼\left(j\in i⟼\left(k\in i⟼if\left(k=j,1_r,0_r\right)\right)\right)\right)$$
8		simpr	$$⊢\left(r=R\wedge i=I\right)\to i=I$$
9		fveq2	$$⊢r=R\to 1_r=1_R$$
10	9 2	eqtr4di	$$⊢r=R\to 1_r=\underset{\dot{}}{1}$$
11		fveq2	$$⊢r=R\to 0_r=0_R$$
12	11 3	eqtr4di	$$⊢r=R\to 0_r=\underset{\dot{}}{0}$$
13	10 12	ifeq12d	$$⊢r=R\to if\left(k=j,1_r,0_r\right)=if\left(k=j,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
14	13	adantr	$$⊢\left(r=R\wedge i=I\right)\to if\left(k=j,1_r,0_r\right)=if\left(k=j,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
15	8 14	mpteq12dv	$$⊢\left(r=R\wedge i=I\right)\to \left(k\in i⟼if\left(k=j,1_r,0_r\right)\right)=\left(k\in I⟼if\left(k=j,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
16	8 15	mpteq12dv	$$⊢\left(r=R\wedge i=I\right)\to \left(j\in i⟼\left(k\in i⟼if\left(k=j,1_r,0_r\right)\right)\right)=\left(j\in I⟼\left(k\in I⟼if\left(k=j,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)$$
17	16	adantl	$$⊢\left(\left(R\in \mathrm{V}\wedge I\in \mathrm{V}\right)\wedge \left(r=R\wedge i=I\right)\right)\to \left(j\in i⟼\left(k\in i⟼if\left(k=j,1_r,0_r\right)\right)\right)=\left(j\in I⟼\left(k\in I⟼if\left(k=j,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)$$
18		simpl	$$⊢\left(R\in \mathrm{V}\wedge I\in \mathrm{V}\right)\to R\in \mathrm{V}$$
19		simpr	$$⊢\left(R\in \mathrm{V}\wedge I\in \mathrm{V}\right)\to I\in \mathrm{V}$$
20		mptexg	$$⊢I\in \mathrm{V}\to \left(j\in I⟼\left(k\in I⟼if\left(k=j,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)\in \mathrm{V}$$
21	20	adantl	$$⊢\left(R\in \mathrm{V}\wedge I\in \mathrm{V}\right)\to \left(j\in I⟼\left(k\in I⟼if\left(k=j,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)\in \mathrm{V}$$
22	7 17 18 19 21	ovmpod	$$⊢\left(R\in \mathrm{V}\wedge I\in \mathrm{V}\right)\to R\mathrm{unitVec}I=\left(j\in I⟼\left(k\in I⟼if\left(k=j,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)$$
23	4 5 22	syl2an	$$⊢\left(R\in V\wedge I\in W\right)\to R\mathrm{unitVec}I=\left(j\in I⟼\left(k\in I⟼if\left(k=j,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)$$
24	1 23	eqtrid	$$⊢\left(R\in V\wedge I\in W\right)\to U=\left(j\in I⟼\left(k\in I⟼if\left(k=j,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\right)$$