Theorem subrgmvrf

Description: The variables in a polynomial algebra are contained in every subring algebra. (Contributed by Mario Carneiro, 4-Jul-2015)

	Ref	Expression
Hypotheses	subrgmvr.v	⊢ 𝑉 = ( 𝐼 mVar 𝑅 )
	subrgmvr.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
	subrgmvr.r	⊢ ( 𝜑 → 𝑇 ∈ ( SubRing ‘ 𝑅 ) )
	subrgmvr.h	⊢ 𝐻 = ( 𝑅 ↾s 𝑇 )
	subrgmvrf.u	⊢ 𝑈 = ( 𝐼 mPoly 𝐻 )
	subrgmvrf.b	⊢ 𝐵 = ( Base ‘ 𝑈 )
Assertion	subrgmvrf	⊢ ( 𝜑 → 𝑉 : 𝐼 ⟶ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		subrgmvr.v	⊢ 𝑉 = ( 𝐼 mVar 𝑅 )
2		subrgmvr.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
3		subrgmvr.r	⊢ ( 𝜑 → 𝑇 ∈ ( SubRing ‘ 𝑅 ) )
4		subrgmvr.h	⊢ 𝐻 = ( 𝑅 ↾s 𝑇 )
5		subrgmvrf.u	⊢ 𝑈 = ( 𝐼 mPoly 𝐻 )
6		subrgmvrf.b	⊢ 𝐵 = ( Base ‘ 𝑈 )
7		eqid	⊢ ( 𝐼 mPwSer 𝑅 ) = ( 𝐼 mPwSer 𝑅 )
8		eqid	⊢ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝑅 ) )
9		subrgrcl	⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → 𝑅 ∈ Ring )
10	3 9	syl	⊢ ( 𝜑 → 𝑅 ∈ Ring )
11	7 1 8 2 10	mvrf	⊢ ( 𝜑 → 𝑉 : 𝐼 ⟶ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) )
12	11	ffnd	⊢ ( 𝜑 → 𝑉 Fn 𝐼 )
13	1 2 3 4	subrgmvr	⊢ ( 𝜑 → 𝑉 = ( 𝐼 mVar 𝐻 ) )
14	13	fveq1d	⊢ ( 𝜑 → ( 𝑉 ‘ 𝑥 ) = ( ( 𝐼 mVar 𝐻 ) ‘ 𝑥 ) )
15	14	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑉 ‘ 𝑥 ) = ( ( 𝐼 mVar 𝐻 ) ‘ 𝑥 ) )
16		eqid	⊢ ( 𝐼 mVar 𝐻 ) = ( 𝐼 mVar 𝐻 )
17	2	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐼 ∈ 𝑊 )
18	4	subrgring	⊢ ( 𝑇 ∈ ( SubRing ‘ 𝑅 ) → 𝐻 ∈ Ring )
19	3 18	syl	⊢ ( 𝜑 → 𝐻 ∈ Ring )
20	19	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝐻 ∈ Ring )
21		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑥 ∈ 𝐼 )
22	5 16 6 17 20 21	mvrcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( ( 𝐼 mVar 𝐻 ) ‘ 𝑥 ) ∈ 𝐵 )
23	15 22	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → ( 𝑉 ‘ 𝑥 ) ∈ 𝐵 )
24	23	ralrimiva	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐼 ( 𝑉 ‘ 𝑥 ) ∈ 𝐵 )
25		ffnfv	⊢ ( 𝑉 : 𝐼 ⟶ 𝐵 ↔ ( 𝑉 Fn 𝐼 ∧ ∀ 𝑥 ∈ 𝐼 ( 𝑉 ‘ 𝑥 ) ∈ 𝐵 ) )
26	12 24 25	sylanbrc	⊢ ( 𝜑 → 𝑉 : 𝐼 ⟶ 𝐵 )