evl1expd

Description: Polynomial evaluation builder for an exponential. (Contributed by Mario Carneiro, 12-Jun-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)$
	evl1expd.f	$⊢ \underset{˙}{∙} = \cdot_{{mulGrp}_{P}}$
	evl1expd.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{R}}$
	evl1expd.4	$⊢ φ \to N \in ℕ_{0}$
Assertion	evl1expd	$⊢ φ \to (N \underset{˙}{∙} M \in U \land O (N \underset{˙}{∙} M) (Y) = N \underset{˙}{\times} V)$

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		evl1expd.f	$⊢ \underset{˙}{∙} = \cdot_{{mulGrp}_{P}}$
9		evl1expd.e	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{R}}$
10		evl1expd.4	$⊢ φ \to N \in ℕ_{0}$
11		eqid	$⊢ {mulGrp}_{P} = {mulGrp}_{P}$
12	11 4	mgpbas	$⊢ U = {Base}_{{mulGrp}_{P}}$
13		crngring	$⊢ R \in CRing \to R \in Ring$
14	5 13	syl	$⊢ φ \to R \in Ring$
15	2	ply1ring	$⊢ R \in Ring \to P \in Ring$
16	11	ringmgp	$⊢ P \in Ring \to {mulGrp}_{P} \in Mnd$
17	14 15 16	3syl	$⊢ φ \to {mulGrp}_{P} \in Mnd$
18	7	simpld	$⊢ φ \to M \in U$
19	12 8 17 10 18	mulgnn0cld	$⊢ φ \to N \underset{˙}{∙} M \in U$
20		eqid	$⊢ R ↑_{𝑠} B = R ↑_{𝑠} B$
21	1 2 20 3	evl1rhm	$⊢ R \in CRing \to O \in (P RingHom (R ↑_{𝑠} B))$
22	5 21	syl	$⊢ φ \to O \in (P RingHom (R ↑_{𝑠} B))$
23		eqid	$⊢ {mulGrp}_{(R ↑_{𝑠} B)} = {mulGrp}_{(R ↑_{𝑠} B)}$
24	11 23	rhmmhm	$⊢ O \in (P RingHom (R ↑_{𝑠} B)) \to O \in ({mulGrp}_{P} MndHom {mulGrp}_{(R ↑_{𝑠} B)})$
25	22 24	syl	$⊢ φ \to O \in ({mulGrp}_{P} MndHom {mulGrp}_{(R ↑_{𝑠} B)})$
26		eqid	$⊢ \cdot_{{mulGrp}_{(R ↑_{𝑠} B)}} = \cdot_{{mulGrp}_{(R ↑_{𝑠} B)}}$
27	12 8 26	mhmmulg	$⊢ (O \in ({mulGrp}_{P} MndHom {mulGrp}_{(R ↑_{𝑠} B)}) \land N \in ℕ_{0} \land M \in U) \to O (N \underset{˙}{∙} M) = N \cdot_{{mulGrp}_{(R ↑_{𝑠} B)}} O (M)$
28	25 10 18 27	syl3anc	$⊢ φ \to O (N \underset{˙}{∙} M) = N \cdot_{{mulGrp}_{(R ↑_{𝑠} B)}} O (M)$
29		eqid	$⊢ \cdot_{({mulGrp}_{R} ↑_{𝑠} B)} = \cdot_{({mulGrp}_{R} ↑_{𝑠} B)}$
30		eqidd	$⊢ φ \to {Base}_{{mulGrp}_{(R ↑_{𝑠} B)}} = {Base}_{{mulGrp}_{(R ↑_{𝑠} B)}}$
31	3	fvexi	$⊢ B \in V$
32		eqid	$⊢ {mulGrp}_{R} = {mulGrp}_{R}$
33		eqid	$⊢ {mulGrp}_{R} ↑_{𝑠} B = {mulGrp}_{R} ↑_{𝑠} B$
34		eqid	$⊢ {Base}_{{mulGrp}_{(R ↑_{𝑠} B)}} = {Base}_{{mulGrp}_{(R ↑_{𝑠} B)}}$
35		eqid	$⊢ {Base}_{({mulGrp}_{R} ↑_{𝑠} B)} = {Base}_{({mulGrp}_{R} ↑_{𝑠} B)}$
36		eqid	$⊢ +_{{mulGrp}_{(R ↑_{𝑠} B)}} = +_{{mulGrp}_{(R ↑_{𝑠} B)}}$
37		eqid	$⊢ +_{({mulGrp}_{R} ↑_{𝑠} B)} = +_{({mulGrp}_{R} ↑_{𝑠} B)}$
38	20 32 33 23 34 35 36 37	pwsmgp	$⊢ (R \in CRing \land B \in V) \to ({Base}_{{mulGrp}_{(R ↑_{𝑠} B)}} = {Base}_{({mulGrp}_{R} ↑_{𝑠} B)} \land +_{{mulGrp}_{(R ↑_{𝑠} B)}} = +_{({mulGrp}_{R} ↑_{𝑠} B)})$
39	5 31 38	sylancl	$⊢ φ \to ({Base}_{{mulGrp}_{(R ↑_{𝑠} B)}} = {Base}_{({mulGrp}_{R} ↑_{𝑠} B)} \land +_{{mulGrp}_{(R ↑_{𝑠} B)}} = +_{({mulGrp}_{R} ↑_{𝑠} B)})$
40	39	simpld	$⊢ φ \to {Base}_{{mulGrp}_{(R ↑_{𝑠} B)}} = {Base}_{({mulGrp}_{R} ↑_{𝑠} B)}$
41		ssv	$⊢ {Base}_{{mulGrp}_{(R ↑_{𝑠} B)}} \subseteq V$
42	41	a1i	$⊢ φ \to {Base}_{{mulGrp}_{(R ↑_{𝑠} B)}} \subseteq V$
43		ovexd	$⊢ (φ \land (x \in V \land y \in V)) \to x +_{{mulGrp}_{(R ↑_{𝑠} B)}} y \in V$
44	39	simprd	$⊢ φ \to +_{{mulGrp}_{(R ↑_{𝑠} B)}} = +_{({mulGrp}_{R} ↑_{𝑠} B)}$
45	44	oveqdr	$⊢ (φ \land (x \in V \land y \in V)) \to x +_{{mulGrp}_{(R ↑_{𝑠} B)}} y = x +_{({mulGrp}_{R} ↑_{𝑠} B)} y$
46	26 29 30 40 42 43 45	mulgpropd	$⊢ φ \to \cdot_{{mulGrp}_{(R ↑_{𝑠} B)}} = \cdot_{({mulGrp}_{R} ↑_{𝑠} B)}$
47	46	oveqd	$⊢ φ \to N \cdot_{{mulGrp}_{(R ↑_{𝑠} B)}} O (M) = N \cdot_{({mulGrp}_{R} ↑_{𝑠} B)} O (M)$
48	28 47	eqtrd	$⊢ φ \to O (N \underset{˙}{∙} M) = N \cdot_{({mulGrp}_{R} ↑_{𝑠} B)} O (M)$
49	48	fveq1d	$⊢ φ \to O (N \underset{˙}{∙} M) (Y) = (N \cdot_{({mulGrp}_{R} ↑_{𝑠} B)} O (M)) (Y)$
50	32	ringmgp	$⊢ R \in Ring \to {mulGrp}_{R} \in Mnd$
51	14 50	syl	$⊢ φ \to {mulGrp}_{R} \in Mnd$
52	31	a1i	$⊢ φ \to B \in V$
53		eqid	$⊢ {Base}_{(R ↑_{𝑠} B)} = {Base}_{(R ↑_{𝑠} B)}$
54	4 53	rhmf	$⊢ O \in (P RingHom (R ↑_{𝑠} B)) \to O : U ⟶ {Base}_{(R ↑_{𝑠} B)}$
55	22 54	syl	$⊢ φ \to O : U ⟶ {Base}_{(R ↑_{𝑠} B)}$
56	55 18	ffvelcdmd	$⊢ φ \to O (M) \in {Base}_{(R ↑_{𝑠} B)}$
57	23 53	mgpbas	$⊢ {Base}_{(R ↑_{𝑠} B)} = {Base}_{{mulGrp}_{(R ↑_{𝑠} B)}}$
58	57 40	eqtrid	$⊢ φ \to {Base}_{(R ↑_{𝑠} B)} = {Base}_{({mulGrp}_{R} ↑_{𝑠} B)}$
59	56 58	eleqtrd	$⊢ φ \to O (M) \in {Base}_{({mulGrp}_{R} ↑_{𝑠} B)}$
60	33 35 29 9	pwsmulg	$⊢ (({mulGrp}_{R} \in Mnd \land B \in V) \land (N \in ℕ_{0} \land O (M) \in {Base}_{({mulGrp}_{R} ↑_{𝑠} B)} \land Y \in B)) \to (N \cdot_{({mulGrp}_{R} ↑_{𝑠} B)} O (M)) (Y) = N \underset{˙}{\times} O (M) (Y)$
61	51 52 10 59 6 60	syl23anc	$⊢ φ \to (N \cdot_{({mulGrp}_{R} ↑_{𝑠} B)} O (M)) (Y) = N \underset{˙}{\times} O (M) (Y)$
62	7	simprd	$⊢ φ \to O (M) (Y) = V$
63	62	oveq2d	$⊢ φ \to N \underset{˙}{\times} O (M) (Y) = N \underset{˙}{\times} V$
64	61 63	eqtrd	$⊢ φ \to (N \cdot_{({mulGrp}_{R} ↑_{𝑠} B)} O (M)) (Y) = N \underset{˙}{\times} V$
65	49 64	eqtrd	$⊢ φ \to O (N \underset{˙}{∙} M) (Y) = N \underset{˙}{\times} V$
66	19 65	jca	$⊢ φ \to (N \underset{˙}{∙} M \in U \land O (N \underset{˙}{∙} M) (Y) = N \underset{˙}{\times} V)$

Metamath Proof Explorer

Theorem evl1expd

Proof