Metamath Proof Explorer

Theorem evls1rhmlem

Description: Lemma for evl1rhm and evls1rhm (formerly part of the proof of evl1rhm ): The first function of the composition forming the univariate polynomial evaluation map function for a (sub)ring is a ring homomorphism. (Contributed by AV, 11-Sep-2019)

Ref Expression
Hypotheses evl1rhmlem.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
evl1rhmlem.t ⊢ 𝑇 = ( 𝑅 ↑s 𝐵 )
evl1rhmlem.f ⊢ 𝐹 = ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )
Assertion evls1rhmlem ( 𝑅 ∈ CRing → 𝐹 ∈ ( ( 𝑅 ↑s ( 𝐵 ↑m 1o ) ) RingHom 𝑇 ) )

Proof

Step Hyp Ref Expression
1 evl1rhmlem.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
2 evl1rhmlem.t ⊢ 𝑇 = ( 𝑅 ↑s 𝐵 )
3 evl1rhmlem.f ⊢ 𝐹 = ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) )
4 ovex ⊢ ( 𝐵 ↑m 1o ) ∈ V
5 eqid ⊢ ( 𝑅 ↑s ( 𝐵 ↑m 1o ) ) = ( 𝑅 ↑s ( 𝐵 ↑m 1o ) )
6 5 1 pwsbas ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝐵 ↑m 1o ) ∈ V ) → ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) = ( Base ‘ ( 𝑅 ↑s ( 𝐵 ↑m 1o ) ) ) )
7 4 6 mpan2 ⊢ ( 𝑅 ∈ CRing → ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) = ( Base ‘ ( 𝑅 ↑s ( 𝐵 ↑m 1o ) ) ) )
8 7 mpteq1d ⊢ ( 𝑅 ∈ CRing → ( 𝑥 ∈ ( 𝐵 ↑m ( 𝐵 ↑m 1o ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) = ( 𝑥 ∈ ( Base ‘ ( 𝑅 ↑s ( 𝐵 ↑m 1o ) ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) )
9 3 8 syl5eq ⊢ ( 𝑅 ∈ CRing → 𝐹 = ( 𝑥 ∈ ( Base ‘ ( 𝑅 ↑s ( 𝐵 ↑m 1o ) ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) )
10 eqid ⊢ ( Base ‘ ( 𝑅 ↑s ( 𝐵 ↑m 1o ) ) ) = ( Base ‘ ( 𝑅 ↑s ( 𝐵 ↑m 1o ) ) )
11 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
12 1 fvexi ⊢ 𝐵 ∈ V
13 12 a1i ⊢ ( 𝑅 ∈ CRing → 𝐵 ∈ V )
14 4 a1i ⊢ ( 𝑅 ∈ CRing → ( 𝐵 ↑m 1o ) ∈ V )
15 df1o2 ⊢ 1o = { ∅ }
16 0ex ⊢ ∅ ∈ V
17 eqid ⊢ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) = ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) )
18 15 12 16 17 mapsnf1o3 ⊢ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) : 𝐵 –1-1-onto→ ( 𝐵 ↑m 1o )
19 f1of ⊢ ( ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) : 𝐵 –1-1-onto→ ( 𝐵 ↑m 1o ) → ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) : 𝐵 ⟶ ( 𝐵 ↑m 1o ) )
20 18 19 mp1i ⊢ ( 𝑅 ∈ CRing → ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) : 𝐵 ⟶ ( 𝐵 ↑m 1o ) )
21 2 5 10 11 13 14 20 pwsco1rhm ⊢ ( 𝑅 ∈ CRing → ( 𝑥 ∈ ( Base ‘ ( 𝑅 ↑s ( 𝐵 ↑m 1o ) ) ) ↦ ( 𝑥 ∘ ( 𝑦 ∈ 𝐵 ↦ ( 1o × { 𝑦 } ) ) ) ) ∈ ( ( 𝑅 ↑s ( 𝐵 ↑m 1o ) ) RingHom 𝑇 ) )
22 9 21 eqeltrd ⊢ ( 𝑅 ∈ CRing → 𝐹 ∈ ( ( 𝑅 ↑s ( 𝐵 ↑m 1o ) ) RingHom 𝑇 ) )