Theorem chrval

Description: Definition substitution of the ring characteristic. (Contributed by Stefan O'Rear, 5-Sep-2015)

	Ref	Expression
Hypotheses	chrval.o	$$⊢O=\mathrm{od}\left(R\right)$$
	chrval.u	$$⊢\underset{\dot{}}{1}=1_R$$
	chrval.c	$$⊢C=\mathrm{chr}\left(R\right)$$
Assertion	chrval	$$⊢O\left(\underset{\dot{}}{1}\right)=C$$

Proof

Step	Hyp	Ref	Expression
1		chrval.o	$$⊢O=\mathrm{od}\left(R\right)$$
2		chrval.u	$$⊢\underset{\dot{}}{1}=1_R$$
3		chrval.c	$$⊢C=\mathrm{chr}\left(R\right)$$
4		fveq2	$$⊢r=R\to \mathrm{od}\left(r\right)=\mathrm{od}\left(R\right)$$
5	4 1	eqtr4di	$$⊢r=R\to \mathrm{od}\left(r\right)=O$$
6		fveq2	$$⊢r=R\to 1_r=1_R$$
7	6 2	eqtr4di	$$⊢r=R\to 1_r=\underset{\dot{}}{1}$$
8	5 7	fveq12d	$$⊢r=R\to \mathrm{od}\left(r\right)\left(1_r\right)=O\left(\underset{\dot{}}{1}\right)$$
9		df-chr	$$⊢\mathrm{chr}=\left(r\in \mathrm{V}⟼\mathrm{od}\left(r\right)\left(1_r\right)\right)$$
10		fvex	$$⊢O\left(\underset{\dot{}}{1}\right)\in \mathrm{V}$$
11	8 9 10	fvmpt	$$⊢R\in \mathrm{V}\to \mathrm{chr}\left(R\right)=O\left(\underset{\dot{}}{1}\right)$$
12		fvprc	$$⊢\neg R\in \mathrm{V}\to \mathrm{chr}\left(R\right)=\varnothing$$
13		fvprc	$$⊢\neg R\in \mathrm{V}\to \mathrm{od}\left(R\right)=\varnothing$$
14	1 13	syl5eq	$$⊢\neg R\in \mathrm{V}\to O=\varnothing$$
15	14	fveq1d	$$⊢\neg R\in \mathrm{V}\to O\left(\underset{\dot{}}{1}\right)=\varnothing \left(\underset{\dot{}}{1}\right)$$
16		0fv	$$⊢\varnothing \left(\underset{\dot{}}{1}\right)=\varnothing$$
17	15 16	eqtrdi	$$⊢\neg R\in \mathrm{V}\to O\left(\underset{\dot{}}{1}\right)=\varnothing$$
18	12 17	eqtr4d	$$⊢\neg R\in \mathrm{V}\to \mathrm{chr}\left(R\right)=O\left(\underset{\dot{}}{1}\right)$$
19	11 18	pm2.61i	$$⊢\mathrm{chr}\left(R\right)=O\left(\underset{\dot{}}{1}\right)$$
20	3 19	eqtr2i	$$⊢O\left(\underset{\dot{}}{1}\right)=C$$