pf1mulcl

Description: The product of multivariate polynomial functions. (Contributed by Mario Carneiro, 12-Jun-2015)

	Ref	Expression
Hypotheses	pf1rcl.q	$⊢ Q = ran {eval}_{1} (R)$
	pf1mulcl.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
Assertion	pf1mulcl	$⊢ (F \in Q \land G \in Q) \to F {\underset{˙}{\cdot}}_{f} G \in Q$

Proof

Step	Hyp	Ref	Expression
1		pf1rcl.q	$⊢ Q = ran {eval}_{1} (R)$
2		pf1mulcl.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
3		eqid	$⊢ R ↑_{𝑠} {Base}_{R} = R ↑_{𝑠} {Base}_{R}$
4		eqid	$⊢ {Base}_{(R ↑_{𝑠} {Base}_{R})} = {Base}_{(R ↑_{𝑠} {Base}_{R})}$
5	1	pf1rcl	$⊢ F \in Q \to R \in CRing$
6	5	adantr	$⊢ (F \in Q \land G \in Q) \to R \in CRing$
7		fvexd	$⊢ (F \in Q \land G \in Q) \to {Base}_{R} \in V$
8		eqid	$⊢ {Base}_{R} = {Base}_{R}$
9	1 8	pf1f	$⊢ F \in Q \to F : {Base}_{R} ⟶ {Base}_{R}$
10	9	adantr	$⊢ (F \in Q \land G \in Q) \to F : {Base}_{R} ⟶ {Base}_{R}$
11		fvex	$⊢ {Base}_{R} \in V$
12	3 8 4	pwselbasb	$⊢ (R \in CRing \land {Base}_{R} \in V) \to (F \in {Base}_{(R ↑_{𝑠} {Base}_{R})} \leftrightarrow F : {Base}_{R} ⟶ {Base}_{R})$
13	6 11 12	sylancl	$⊢ (F \in Q \land G \in Q) \to (F \in {Base}_{(R ↑_{𝑠} {Base}_{R})} \leftrightarrow F : {Base}_{R} ⟶ {Base}_{R})$
14	10 13	mpbird	$⊢ (F \in Q \land G \in Q) \to F \in {Base}_{(R ↑_{𝑠} {Base}_{R})}$
15	1 8	pf1f	$⊢ G \in Q \to G : {Base}_{R} ⟶ {Base}_{R}$
16	15	adantl	$⊢ (F \in Q \land G \in Q) \to G : {Base}_{R} ⟶ {Base}_{R}$
17	3 8 4	pwselbasb	$⊢ (R \in CRing \land {Base}_{R} \in V) \to (G \in {Base}_{(R ↑_{𝑠} {Base}_{R})} \leftrightarrow G : {Base}_{R} ⟶ {Base}_{R})$
18	6 11 17	sylancl	$⊢ (F \in Q \land G \in Q) \to (G \in {Base}_{(R ↑_{𝑠} {Base}_{R})} \leftrightarrow G : {Base}_{R} ⟶ {Base}_{R})$
19	16 18	mpbird	$⊢ (F \in Q \land G \in Q) \to G \in {Base}_{(R ↑_{𝑠} {Base}_{R})}$
20		eqid	$⊢ \cdot_{(R ↑_{𝑠} {Base}_{R})} = \cdot_{(R ↑_{𝑠} {Base}_{R})}$
21	3 4 6 7 14 19 2 20	pwsmulrval	$⊢ (F \in Q \land G \in Q) \to F \cdot_{(R ↑_{𝑠} {Base}_{R})} G = F {\underset{˙}{\cdot}}_{f} G$
22	8 1	pf1subrg	$⊢ R \in CRing \to Q \in SubRing (R ↑_{𝑠} {Base}_{R})$
23	6 22	syl	$⊢ (F \in Q \land G \in Q) \to Q \in SubRing (R ↑_{𝑠} {Base}_{R})$
24	20	subrgmcl	$⊢ (Q \in SubRing (R ↑_{𝑠} {Base}_{R}) \land F \in Q \land G \in Q) \to F \cdot_{(R ↑_{𝑠} {Base}_{R})} G \in Q$
25	24	3expib	$⊢ Q \in SubRing (R ↑_{𝑠} {Base}_{R}) \to ((F \in Q \land G \in Q) \to F \cdot_{(R ↑_{𝑠} {Base}_{R})} G \in Q)$
26	23 25	mpcom	$⊢ (F \in Q \land G \in Q) \to F \cdot_{(R ↑_{𝑠} {Base}_{R})} G \in Q$
27	21 26	eqeltrrd	$⊢ (F \in Q \land G \in Q) \to F {\underset{˙}{\cdot}}_{f} G \in Q$

Metamath Proof Explorer

Theorem pf1mulcl

Proof