This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 eqtrid ⊢ ( ¬ 𝑅 ∈ 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 ) = 𝐶