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 × { 𝑦 } ) ) ) )