mpfmulcl

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

	Ref	Expression
Hypotheses	mpfsubrg.q	$⊢ Q = ran (I evalSub S) (R)$
	mpfmulcl.t	$⊢ \underset{˙}{\cdot} = \cdot_{S}$
Assertion	mpfmulcl	$⊢ (F \in Q \land G \in Q) \to F {\underset{˙}{\cdot}}_{f} G \in Q$

Proof

Step	Hyp	Ref	Expression
1		mpfsubrg.q	$⊢ Q = ran (I evalSub S) (R)$
2		mpfmulcl.t	$⊢ \underset{˙}{\cdot} = \cdot_{S}$
3		eqid	$⊢ S ↑_{𝑠} ({Base}_{S}^{I}) = S ↑_{𝑠} ({Base}_{S}^{I})$
4		eqid	$⊢ {Base}_{(S ↑_{𝑠} ({Base}_{S}^{I}))} = {Base}_{(S ↑_{𝑠} ({Base}_{S}^{I}))}$
5	1	mpfrcl	$⊢ F \in Q \to (I \in V \land S \in CRing \land R \in SubRing (S))$
6	5	adantr	$⊢ (F \in Q \land G \in Q) \to (I \in V \land S \in CRing \land R \in SubRing (S))$
7	6	simp2d	$⊢ (F \in Q \land G \in Q) \to S \in CRing$
8		ovexd	$⊢ (F \in Q \land G \in Q) \to {Base}_{S}^{I} \in V$
9	1	mpfsubrg	$⊢ (I \in V \land S \in CRing \land R \in SubRing (S)) \to Q \in SubRing (S ↑_{𝑠} ({Base}_{S}^{I}))$
10	6 9	syl	$⊢ (F \in Q \land G \in Q) \to Q \in SubRing (S ↑_{𝑠} ({Base}_{S}^{I}))$
11	4	subrgss	$⊢ Q \in SubRing (S ↑_{𝑠} ({Base}_{S}^{I})) \to Q \subseteq {Base}_{(S ↑_{𝑠} ({Base}_{S}^{I}))}$
12	10 11	syl	$⊢ (F \in Q \land G \in Q) \to Q \subseteq {Base}_{(S ↑_{𝑠} ({Base}_{S}^{I}))}$
13		simpl	$⊢ (F \in Q \land G \in Q) \to F \in Q$
14	12 13	sseldd	$⊢ (F \in Q \land G \in Q) \to F \in {Base}_{(S ↑_{𝑠} ({Base}_{S}^{I}))}$
15		simpr	$⊢ (F \in Q \land G \in Q) \to G \in Q$
16	12 15	sseldd	$⊢ (F \in Q \land G \in Q) \to G \in {Base}_{(S ↑_{𝑠} ({Base}_{S}^{I}))}$
17		eqid	$⊢ \cdot_{(S ↑_{𝑠} ({Base}_{S}^{I}))} = \cdot_{(S ↑_{𝑠} ({Base}_{S}^{I}))}$
18	3 4 7 8 14 16 2 17	pwsmulrval	$⊢ (F \in Q \land G \in Q) \to F \cdot_{(S ↑_{𝑠} ({Base}_{S}^{I}))} G = F {\underset{˙}{\cdot}}_{f} G$
19	17	subrgmcl	$⊢ (Q \in SubRing (S ↑_{𝑠} ({Base}_{S}^{I})) \land F \in Q \land G \in Q) \to F \cdot_{(S ↑_{𝑠} ({Base}_{S}^{I}))} G \in Q$
20	19	3expib	$⊢ Q \in SubRing (S ↑_{𝑠} ({Base}_{S}^{I})) \to ((F \in Q \land G \in Q) \to F \cdot_{(S ↑_{𝑠} ({Base}_{S}^{I}))} G \in Q)$
21	10 20	mpcom	$⊢ (F \in Q \land G \in Q) \to F \cdot_{(S ↑_{𝑠} ({Base}_{S}^{I}))} G \in Q$
22	18 21	eqeltrrd	$⊢ (F \in Q \land G \in Q) \to F {\underset{˙}{\cdot}}_{f} G \in Q$

Metamath Proof Explorer

Theorem mpfmulcl

Proof