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

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 eqtrid ⊢ ( ( 𝑅 ∈ CRing ∧ 𝐴 ∈ 𝐾 ) → ( 𝑂 ‘ 𝐴 ) = ( ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ‘ ( 𝑄 ‘ 𝐴 ) ) )
19 ffvelcdm ⊢ ( ( 𝑄 : 𝐾 ⟶ ( 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 × { 𝑦 } ) ) ) )