Theorem chrval

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

	Ref	Expression
Hypotheses	chrval.o	⊢ 𝑂 = ( od ‘ 𝑅 )
	chrval.u	⊢ 1 = ( 1r ‘ 𝑅 )
	chrval.c	⊢ 𝐶 = ( chr ‘ 𝑅 )
Assertion	chrval	⊢ ( 𝑂 ‘ 1 ) = 𝐶

Proof

Step	Hyp	Ref	Expression
1		chrval.o	⊢ 𝑂 = ( od ‘ 𝑅 )
2		chrval.u	⊢ 1 = ( 1r ‘ 𝑅 )
3		chrval.c	⊢ 𝐶 = ( chr ‘ 𝑅 )
4		fveq2	⊢ ( 𝑟 = 𝑅 → ( od ‘ 𝑟 ) = ( od ‘ 𝑅 ) )
5	4 1	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( od ‘ 𝑟 ) = 𝑂 )
6		fveq2	⊢ ( 𝑟 = 𝑅 → ( 1r ‘ 𝑟 ) = ( 1r ‘ 𝑅 ) )
7	6 2	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( 1r ‘ 𝑟 ) = 1 )
8	5 7	fveq12d	⊢ ( 𝑟 = 𝑅 → ( ( od ‘ 𝑟 ) ‘ ( 1r ‘ 𝑟 ) ) = ( 𝑂 ‘ 1 ) )
9		df-chr	⊢ chr = ( 𝑟 ∈ V ↦ ( ( od ‘ 𝑟 ) ‘ ( 1r ‘ 𝑟 ) ) )
10		fvex	⊢ ( 𝑂 ‘ 1 ) ∈ V
11	8 9 10	fvmpt	⊢ ( 𝑅 ∈ V → ( chr ‘ 𝑅 ) = ( 𝑂 ‘ 1 ) )
12		fvprc	⊢ ( ¬ 𝑅 ∈ V → ( chr ‘ 𝑅 ) = ∅ )
13		fvprc	⊢ ( ¬ 𝑅 ∈ V → ( od ‘ 𝑅 ) = ∅ )
14	1 13	syl5eq	⊢ ( ¬ 𝑅 ∈ V → 𝑂 = ∅ )
15	14	fveq1d	⊢ ( ¬ 𝑅 ∈ V → ( 𝑂 ‘ 1 ) = ( ∅ ‘ 1 ) )
16		0fv	⊢ ( ∅ ‘ 1 ) = ∅
17	15 16	eqtrdi	⊢ ( ¬ 𝑅 ∈ V → ( 𝑂 ‘ 1 ) = ∅ )
18	12 17	eqtr4d	⊢ ( ¬ 𝑅 ∈ V → ( chr ‘ 𝑅 ) = ( 𝑂 ‘ 1 ) )
19	11 18	pm2.61i	⊢ ( chr ‘ 𝑅 ) = ( 𝑂 ‘ 1 )
20	3 19	eqtr2i	⊢ ( 𝑂 ‘ 1 ) = 𝐶