Theorem reldmevls

Description: Well-behaved binary operation property of evalSub . (Contributed by Stefan O'Rear, 19-Mar-2015)

	Ref	Expression
Assertion	reldmevls	⊢ Rel dom evalSub

Proof

Step	Hyp	Ref	Expression
1		df-evls	⊢ evalSub = ( 𝑖 ∈ V , 𝑠 ∈ CRing ↦ ⦋ ( Base ‘ 𝑠 ) / 𝑏 ⦌ ( 𝑟 ∈ ( SubRing ‘ 𝑠 ) ↦ ⦋ ( 𝑖 mPoly ( 𝑠 ↾s 𝑟 ) ) / 𝑤 ⦌ ( ℩ 𝑓 ∈ ( 𝑤 RingHom ( 𝑠 ↑s ( 𝑏 ↑m 𝑖 ) ) ) ( ( 𝑓 ∘ ( algSc ‘ 𝑤 ) ) = ( 𝑥 ∈ 𝑟 ↦ ( ( 𝑏 ↑m 𝑖 ) × { 𝑥 } ) ) ∧ ( 𝑓 ∘ ( 𝑖 mVar ( 𝑠 ↾s 𝑟 ) ) ) = ( 𝑥 ∈ 𝑖 ↦ ( 𝑔 ∈ ( 𝑏 ↑m 𝑖 ) ↦ ( 𝑔 ‘ 𝑥 ) ) ) ) ) ) )
2	1	reldmmpo	⊢ Rel dom evalSub