# Metamath Proof Explorer

## Theorem evl1val

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 ‘ 𝑅 )
evl1val.m 𝑀 = ( 1o mPoly 𝑅 )
evl1val.k 𝐾 = ( Base ‘ 𝑀 )
Assertion evl1val ( ( 𝑅 ∈ CRing ∧ 𝐴𝐾 ) → ( 𝑂𝐴 ) = ( ( 𝑄𝐴 ) ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )

### Proof

Step Hyp Ref Expression
1 evl1fval.o 𝑂 = ( eval1𝑅 )
2 evl1fval.q 𝑄 = ( 1o eval 𝑅 )
3 evl1fval.b 𝐵 = ( Base ‘ 𝑅 )
4 evl1val.m 𝑀 = ( 1o mPoly 𝑅 )
5 evl1val.k 𝐾 = ( Base ‘ 𝑀 )
6 1 2 3 evl1fval 𝑂 = ( ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ 𝑄 )
7 6 fveq1i ( 𝑂𝐴 ) = ( ( ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ 𝑄 ) ‘ 𝐴 )
8 1on 1o ∈ On
9 simpl ( ( 𝑅 ∈ CRing ∧ 𝐴𝐾 ) → 𝑅 ∈ CRing )
10 eqid ( 𝑅s ( 𝐵m 1o ) ) = ( 𝑅s ( 𝐵m 1o ) )
11 2 3 4 10 evlrhm ( ( 1o ∈ On ∧ 𝑅 ∈ CRing ) → 𝑄 ∈ ( 𝑀 RingHom ( 𝑅s ( 𝐵m 1o ) ) ) )
12 8 9 11 sylancr ( ( 𝑅 ∈ CRing ∧ 𝐴𝐾 ) → 𝑄 ∈ ( 𝑀 RingHom ( 𝑅s ( 𝐵m 1o ) ) ) )
13 eqid ( Base ‘ ( 𝑅s ( 𝐵m 1o ) ) ) = ( Base ‘ ( 𝑅s ( 𝐵m 1o ) ) )
14 5 13 rhmf ( 𝑄 ∈ ( 𝑀 RingHom ( 𝑅s ( 𝐵m 1o ) ) ) → 𝑄 : 𝐾 ⟶ ( Base ‘ ( 𝑅s ( 𝐵m 1o ) ) ) )
15 12 14 syl ( ( 𝑅 ∈ CRing ∧ 𝐴𝐾 ) → 𝑄 : 𝐾 ⟶ ( Base ‘ ( 𝑅s ( 𝐵m 1o ) ) ) )
16 fvco3 ( ( 𝑄 : 𝐾 ⟶ ( Base ‘ ( 𝑅s ( 𝐵m 1o ) ) ) ∧ 𝐴𝐾 ) → ( ( ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ 𝑄 ) ‘ 𝐴 ) = ( ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ‘ ( 𝑄𝐴 ) ) )
17 15 16 sylancom ( ( 𝑅 ∈ CRing ∧ 𝐴𝐾 ) → ( ( ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∘ 𝑄 ) ‘ 𝐴 ) = ( ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ‘ ( 𝑄𝐴 ) ) )
18 7 17 syl5eq ( ( 𝑅 ∈ CRing ∧ 𝐴𝐾 ) → ( 𝑂𝐴 ) = ( ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ‘ ( 𝑄𝐴 ) ) )
19 ffvelrn ( ( 𝑄 : 𝐾 ⟶ ( Base ‘ ( 𝑅s ( 𝐵m 1o ) ) ) ∧ 𝐴𝐾 ) → ( 𝑄𝐴 ) ∈ ( Base ‘ ( 𝑅s ( 𝐵m 1o ) ) ) )
20 15 19 sylancom ( ( 𝑅 ∈ CRing ∧ 𝐴𝐾 ) → ( 𝑄𝐴 ) ∈ ( Base ‘ ( 𝑅s ( 𝐵m 1o ) ) ) )
21 crngring ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
22 21 adantr ( ( 𝑅 ∈ CRing ∧ 𝐴𝐾 ) → 𝑅 ∈ Ring )
23 ovex ( 𝐵m 1o ) ∈ V
24 10 3 pwsbas ( ( 𝑅 ∈ Ring ∧ ( 𝐵m 1o ) ∈ V ) → ( 𝐵m ( 𝐵m 1o ) ) = ( Base ‘ ( 𝑅s ( 𝐵m 1o ) ) ) )
25 22 23 24 sylancl ( ( 𝑅 ∈ CRing ∧ 𝐴𝐾 ) → ( 𝐵m ( 𝐵m 1o ) ) = ( Base ‘ ( 𝑅s ( 𝐵m 1o ) ) ) )
26 20 25 eleqtrrd ( ( 𝑅 ∈ CRing ∧ 𝐴𝐾 ) → ( 𝑄𝐴 ) ∈ ( 𝐵m ( 𝐵m 1o ) ) )
27 coeq1 ( 𝑥 = ( 𝑄𝐴 ) → ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) = ( ( 𝑄𝐴 ) ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )
28 eqid ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) = ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )
29 fvex ( 𝑄𝐴 ) ∈ V
30 3 fvexi 𝐵 ∈ V
31 30 mptex ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ∈ V
32 29 31 coex ( ( 𝑄𝐴 ) ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ∈ V
33 27 28 32 fvmpt ( ( 𝑄𝐴 ) ∈ ( 𝐵m ( 𝐵m 1o ) ) → ( ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ‘ ( 𝑄𝐴 ) ) = ( ( 𝑄𝐴 ) ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )
34 26 33 syl ( ( 𝑅 ∈ CRing ∧ 𝐴𝐾 ) → ( ( 𝑥 ∈ ( 𝐵m ( 𝐵m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ‘ ( 𝑄𝐴 ) ) = ( ( 𝑄𝐴 ) ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )
35 18 34 eqtrd ( ( 𝑅 ∈ CRing ∧ 𝐴𝐾 ) → ( 𝑂𝐴 ) = ( ( 𝑄𝐴 ) ∘ ( 𝑦𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )