evl1muld

Description: Polynomial evaluation builder for multiplication of polynomials. (Contributed by Mario Carneiro, 4-Jul-2015)

	Ref	Expression
Hypotheses	evl1addd.q	$⊢ O = {eval}_{1} (R)$
	evl1addd.p	$⊢ P = {Poly}_{1} (R)$
	evl1addd.b	$⊢ B = {Base}_{R}$
	evl1addd.u	$⊢ U = {Base}_{P}$
	evl1addd.1	$⊢ φ \to R \in CRing$
	evl1addd.2	$⊢ φ \to Y \in B$
	evl1addd.3	$⊢ φ \to (M \in U \land O (M) (Y) = V)$
	evl1addd.4	$⊢ φ \to (N \in U \land O (N) (Y) = W)$
	evl1muld.t	$⊢ \underset{˙}{∙} = \cdot_{P}$
	evl1muld.s	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
Assertion	evl1muld	$⊢ φ \to (M \underset{˙}{∙} N \in U \land O (M \underset{˙}{∙} N) (Y) = V \underset{˙}{\cdot} W)$

Proof

Step	Hyp	Ref	Expression
1		evl1addd.q	$⊢ O = {eval}_{1} (R)$
2		evl1addd.p	$⊢ P = {Poly}_{1} (R)$
3		evl1addd.b	$⊢ B = {Base}_{R}$
4		evl1addd.u	$⊢ U = {Base}_{P}$
5		evl1addd.1	$⊢ φ \to R \in CRing$
6		evl1addd.2	$⊢ φ \to Y \in B$
7		evl1addd.3	$⊢ φ \to (M \in U \land O (M) (Y) = V)$
8		evl1addd.4	$⊢ φ \to (N \in U \land O (N) (Y) = W)$
9		evl1muld.t	$⊢ \underset{˙}{∙} = \cdot_{P}$
10		evl1muld.s	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
11		eqid	$⊢ R ↑_{𝑠} B = R ↑_{𝑠} B$
12	1 2 11 3	evl1rhm	$⊢ R \in CRing \to O \in (P RingHom (R ↑_{𝑠} B))$
13	5 12	syl	$⊢ φ \to O \in (P RingHom (R ↑_{𝑠} B))$
14		rhmrcl1	$⊢ O \in (P RingHom (R ↑_{𝑠} B)) \to P \in Ring$
15	13 14	syl	$⊢ φ \to P \in Ring$
16	7	simpld	$⊢ φ \to M \in U$
17	8	simpld	$⊢ φ \to N \in U$
18	4 9	ringcl	$⊢ (P \in Ring \land M \in U \land N \in U) \to M \underset{˙}{∙} N \in U$
19	15 16 17 18	syl3anc	$⊢ φ \to M \underset{˙}{∙} N \in U$
20		eqid	$⊢ \cdot_{(R ↑_{𝑠} B)} = \cdot_{(R ↑_{𝑠} B)}$
21	4 9 20	rhmmul	$⊢ (O \in (P RingHom (R ↑_{𝑠} B)) \land M \in U \land N \in U) \to O (M \underset{˙}{∙} N) = O (M) \cdot_{(R ↑_{𝑠} B)} O (N)$
22	13 16 17 21	syl3anc	$⊢ φ \to O (M \underset{˙}{∙} N) = O (M) \cdot_{(R ↑_{𝑠} B)} O (N)$
23		eqid	$⊢ {Base}_{(R ↑_{𝑠} B)} = {Base}_{(R ↑_{𝑠} B)}$
24	3	fvexi	$⊢ B \in V$
25	24	a1i	$⊢ φ \to B \in V$
26	4 23	rhmf	$⊢ O \in (P RingHom (R ↑_{𝑠} B)) \to O : U ⟶ {Base}_{(R ↑_{𝑠} B)}$
27	13 26	syl	$⊢ φ \to O : U ⟶ {Base}_{(R ↑_{𝑠} B)}$
28	27 16	ffvelrnd	$⊢ φ \to O (M) \in {Base}_{(R ↑_{𝑠} B)}$
29	27 17	ffvelrnd	$⊢ φ \to O (N) \in {Base}_{(R ↑_{𝑠} B)}$
30	11 23 5 25 28 29 10 20	pwsmulrval	$⊢ φ \to O (M) \cdot_{(R ↑_{𝑠} B)} O (N) = O (M) {\underset{˙}{\cdot}}_{f} O (N)$
31	22 30	eqtrd	$⊢ φ \to O (M \underset{˙}{∙} N) = O (M) {\underset{˙}{\cdot}}_{f} O (N)$
32	31	fveq1d	$⊢ φ \to O (M \underset{˙}{∙} N) (Y) = (O (M) {\underset{˙}{\cdot}}_{f} O (N)) (Y)$
33	11 3 23 5 25 28	pwselbas	$⊢ φ \to O (M) : B ⟶ B$
34	33	ffnd	$⊢ φ \to O (M) Fn B$
35	11 3 23 5 25 29	pwselbas	$⊢ φ \to O (N) : B ⟶ B$
36	35	ffnd	$⊢ φ \to O (N) Fn B$
37		fnfvof	$⊢ ((O (M) Fn B \land O (N) Fn B) \land (B \in V \land Y \in B)) \to (O (M) {\underset{˙}{\cdot}}_{f} O (N)) (Y) = O (M) (Y) \underset{˙}{\cdot} O (N) (Y)$
38	34 36 25 6 37	syl22anc	$⊢ φ \to (O (M) {\underset{˙}{\cdot}}_{f} O (N)) (Y) = O (M) (Y) \underset{˙}{\cdot} O (N) (Y)$
39	7	simprd	$⊢ φ \to O (M) (Y) = V$
40	8	simprd	$⊢ φ \to O (N) (Y) = W$
41	39 40	oveq12d	$⊢ φ \to O (M) (Y) \underset{˙}{\cdot} O (N) (Y) = V \underset{˙}{\cdot} W$
42	32 38 41	3eqtrd	$⊢ φ \to O (M \underset{˙}{∙} N) (Y) = V \underset{˙}{\cdot} W$
43	19 42	jca	$⊢ φ \to (M \underset{˙}{∙} N \in U \land O (M \underset{˙}{∙} N) (Y) = V \underset{˙}{\cdot} W)$

Metamath Proof Explorer

Theorem evl1muld

Proof