Theorem uvcvval

Description: Value of a unit vector coordinate in a free module. (Contributed by Stefan O'Rear, 3-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	uvcvval	$$⊢\left(\left(R\in V\wedge I\in W\wedge J\in I\right)\wedge K\in I\right)\to U\left(J\right)\left(K\right)=if\left(K=J,\underset{\dot{}}{1},\underset{\dot{}}{0}\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	1 2 3	uvcval	$$⊢\left(R\in V\wedge I\in W\wedge J\in I\right)\to U\left(J\right)=\left(k\in I⟼if\left(k=J,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
5	4	fveq1d	$$⊢\left(R\in V\wedge I\in W\wedge J\in I\right)\to U\left(J\right)\left(K\right)=\left(k\in I⟼if\left(k=J,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(K\right)$$
6	5	adantr	$$⊢\left(\left(R\in V\wedge I\in W\wedge J\in I\right)\wedge K\in I\right)\to U\left(J\right)\left(K\right)=\left(k\in I⟼if\left(k=J,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(K\right)$$
7		simpr	$$⊢\left(\left(R\in V\wedge I\in W\wedge J\in I\right)\wedge K\in I\right)\to K\in I$$
8	2	fvexi	$$⊢\underset{\dot{}}{1}\in \mathrm{V}$$
9	3	fvexi	$$⊢\underset{\dot{}}{0}\in \mathrm{V}$$
10	8 9	ifex	$$⊢if\left(K=J,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\in \mathrm{V}$$
11		eqeq1	$$⊢k=K\to \left(k=J\leftrightarrow K=J\right)$$
12	11	ifbid	$$⊢k=K\to if\left(k=J,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)=if\left(K=J,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
13		eqid	$$⊢\left(k\in I⟼if\left(k=J,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)=\left(k\in I⟼if\left(k=J,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)$$
14	12 13	fvmptg	$$⊢\left(K\in I\wedge if\left(K=J,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\in \mathrm{V}\right)\to \left(k\in I⟼if\left(k=J,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(K\right)=if\left(K=J,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
15	7 10 14	sylancl	$$⊢\left(\left(R\in V\wedge I\in W\wedge J\in I\right)\wedge K\in I\right)\to \left(k\in I⟼if\left(k=J,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)\right)\left(K\right)=if\left(K=J,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$
16	6 15	eqtrd	$$⊢\left(\left(R\in V\wedge I\in W\wedge J\in I\right)\wedge K\in I\right)\to U\left(J\right)\left(K\right)=if\left(K=J,\underset{\dot{}}{1},\underset{\dot{}}{0}\right)$$