# Metamath Proof Explorer

## Theorem evl1fval

Description: Value of the simple/same ring evaluation map. (Contributed by Mario Carneiro, 12-Jun-2015)

Ref Expression
Hypotheses evl1fval.o 𝑂 = ( eval1𝑅 )
evl1fval.q 𝑄 = ( 1o eval 𝑅 )
evl1fval.b 𝐵 = ( Base ‘ 𝑅 )
Assertion evl1fval 𝑂 = ( ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ 𝑄 )

### Proof

Step Hyp Ref Expression
1 evl1fval.o 𝑂 = ( eval1𝑅 )
2 evl1fval.q 𝑄 = ( 1o eval 𝑅 )
3 evl1fval.b 𝐵 = ( Base ‘ 𝑅 )
4 fvexd ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) ∈ V )
5 id ( 𝑏 = ( Base ‘ 𝑟 ) → 𝑏 = ( Base ‘ 𝑟 ) )
6 fveq2 ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) = ( Base ‘ 𝑅 ) )
7 6 3 eqtr4di ( 𝑟 = 𝑅 → ( Base ‘ 𝑟 ) = 𝐵 )
8 5 7 sylan9eqr ( ( 𝑟 = 𝑅𝑏 = ( Base ‘ 𝑟 ) ) → 𝑏 = 𝐵 )
9 8 oveq1d ( ( 𝑟 = 𝑅𝑏 = ( Base ‘ 𝑟 ) ) → ( 𝑏m 1o ) = ( 𝐵m 1o ) )
10 8 9 oveq12d ( ( 𝑟 = 𝑅𝑏 = ( Base ‘ 𝑟 ) ) → ( 𝑏m ( 𝑏m 1o ) ) = ( 𝐵m ( 𝐵m 1o ) ) )
11 8 mpteq1d ( ( 𝑟 = 𝑅𝑏 = ( Base ‘ 𝑟 ) ) → ( 𝑦𝑏 ↦ ( 1o × { 𝑦 } ) ) = ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) )
12 11 coeq2d ( ( 𝑟 = 𝑅𝑏 = ( Base ‘ 𝑟 ) ) → ( 𝑥 ∘ ( 𝑦𝑏 ↦ ( 1o × { 𝑦 } ) ) ) = ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )
13 10 12 mpteq12dv ( ( 𝑟 = 𝑅𝑏 = ( Base ‘ 𝑟 ) ) → ( 𝑥 ∈ ( 𝑏m ( 𝑏m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝑏 ↦ ( 1o × { 𝑦 } ) ) ) ) = ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) )
14 simpl ( ( 𝑟 = 𝑅𝑏 = ( Base ‘ 𝑟 ) ) → 𝑟 = 𝑅 )
15 14 oveq2d ( ( 𝑟 = 𝑅𝑏 = ( Base ‘ 𝑟 ) ) → ( 1o eval 𝑟 ) = ( 1o eval 𝑅 ) )
16 15 2 eqtr4di ( ( 𝑟 = 𝑅𝑏 = ( Base ‘ 𝑟 ) ) → ( 1o eval 𝑟 ) = 𝑄 )
17 13 16 coeq12d ( ( 𝑟 = 𝑅𝑏 = ( Base ‘ 𝑟 ) ) → ( ( 𝑥 ∈ ( 𝑏m ( 𝑏m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝑏 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( 1o eval 𝑟 ) ) = ( ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ 𝑄 ) )
18 4 17 csbied ( 𝑟 = 𝑅 ( Base ‘ 𝑟 ) / 𝑏 ( ( 𝑥 ∈ ( 𝑏m ( 𝑏m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝑏 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( 1o eval 𝑟 ) ) = ( ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ 𝑄 ) )
19 df-evl1 eval1 = ( 𝑟 ∈ V ↦ ( Base ‘ 𝑟 ) / 𝑏 ( ( 𝑥 ∈ ( 𝑏m ( 𝑏m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝑏 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ( 1o eval 𝑟 ) ) )
20 ovex ( 𝐵m ( 𝐵m 1o ) ) ∈ V
21 20 mptex ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∈ V
22 2 ovexi 𝑄 ∈ V
23 21 22 coex ( ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ 𝑄 ) ∈ V
24 18 19 23 fvmpt ( 𝑅 ∈ V → ( eval1𝑅 ) = ( ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ 𝑄 ) )
25 1 24 syl5eq ( 𝑅 ∈ V → 𝑂 = ( ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ 𝑄 ) )
26 fvprc ( ¬ 𝑅 ∈ V → ( eval1𝑅 ) = ∅ )
27 1 26 syl5eq ( ¬ 𝑅 ∈ V → 𝑂 = ∅ )
28 co02 ( ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ∅ ) = ∅
29 27 28 eqtr4di ( ¬ 𝑅 ∈ V → 𝑂 = ( ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ∅ ) )
30 df-evl eval = ( 𝑖 ∈ V , 𝑟 ∈ V ↦ ( ( 𝑖 evalSub 𝑟 ) ‘ ( Base ‘ 𝑟 ) ) )
31 30 reldmmpo Rel dom eval
32 31 ovprc2 ( ¬ 𝑅 ∈ V → ( 1o eval 𝑅 ) = ∅ )
33 2 32 syl5eq ( ¬ 𝑅 ∈ V → 𝑄 = ∅ )
34 33 coeq2d ( ¬ 𝑅 ∈ V → ( ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ 𝑄 ) = ( ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ ∅ ) )
35 29 34 eqtr4d ( ¬ 𝑅 ∈ V → 𝑂 = ( ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ 𝑄 ) )
36 25 35 pm2.61i 𝑂 = ( ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ 𝑄 )