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

Metamath Proof Explorer

Theorem evl1expd

Proof