pwsco2mhm

Description: Left composition with a monoid homomorphism yields a monoid homomorphism of structure powers. (Contributed by Mario Carneiro, 12-Jun-2015)

	Ref	Expression
Hypotheses	pwsco2mhm.y	$⊢ Y = R ↑_{𝑠} A$
	pwsco2mhm.z	$⊢ Z = S ↑_{𝑠} A$
	pwsco2mhm.b	$⊢ B = {Base}_{Y}$
	pwsco2mhm.a	$⊢ φ \to A \in V$
	pwsco2mhm.f	$⊢ φ \to F \in (R MndHom S)$
Assertion	pwsco2mhm	$⊢ φ \to (g \in B ⟼ F \circ g) \in (Y MndHom Z)$

Proof

Step	Hyp	Ref	Expression
1		pwsco2mhm.y	$⊢ Y = R ↑_{𝑠} A$
2		pwsco2mhm.z	$⊢ Z = S ↑_{𝑠} A$
3		pwsco2mhm.b	$⊢ B = {Base}_{Y}$
4		pwsco2mhm.a	$⊢ φ \to A \in V$
5		pwsco2mhm.f	$⊢ φ \to F \in (R MndHom S)$
6		mhmrcl1	$⊢ F \in (R MndHom S) \to R \in Mnd$
7	5 6	syl	$⊢ φ \to R \in Mnd$
8	1	pwsmnd	$⊢ (R \in Mnd \land A \in V) \to Y \in Mnd$
9	7 4 8	syl2anc	$⊢ φ \to Y \in Mnd$
10		mhmrcl2	$⊢ F \in (R MndHom S) \to S \in Mnd$
11	5 10	syl	$⊢ φ \to S \in Mnd$
12	2	pwsmnd	$⊢ (S \in Mnd \land A \in V) \to Z \in Mnd$
13	11 4 12	syl2anc	$⊢ φ \to Z \in Mnd$
14		eqid	$⊢ {Base}_{R} = {Base}_{R}$
15		eqid	$⊢ {Base}_{S} = {Base}_{S}$
16	14 15	mhmf	$⊢ F \in (R MndHom S) \to F : {Base}_{R} ⟶ {Base}_{S}$
17	5 16	syl	$⊢ φ \to F : {Base}_{R} ⟶ {Base}_{S}$
18	7	adantr	$⊢ (φ \land g \in B) \to R \in Mnd$
19	4	adantr	$⊢ (φ \land g \in B) \to A \in V$
20		simpr	$⊢ (φ \land g \in B) \to g \in B$
21	1 14 3 18 19 20	pwselbas	$⊢ (φ \land g \in B) \to g : A ⟶ {Base}_{R}$
22		fco	$⊢ (F : {Base}_{R} ⟶ {Base}_{S} \land g : A ⟶ {Base}_{R}) \to (F \circ g) : A ⟶ {Base}_{S}$
23	17 21 22	syl2an2r	$⊢ (φ \land g \in B) \to (F \circ g) : A ⟶ {Base}_{S}$
24		eqid	$⊢ {Base}_{Z} = {Base}_{Z}$
25	2 15 24	pwselbasb	$⊢ (S \in Mnd \land A \in V) \to (F \circ g \in {Base}_{Z} \leftrightarrow (F \circ g) : A ⟶ {Base}_{S})$
26	11 19 25	syl2an2r	$⊢ (φ \land g \in B) \to (F \circ g \in {Base}_{Z} \leftrightarrow (F \circ g) : A ⟶ {Base}_{S})$
27	23 26	mpbird	$⊢ (φ \land g \in B) \to F \circ g \in {Base}_{Z}$
28	27	fmpttd	$⊢ φ \to (g \in B ⟼ F \circ g) : B ⟶ {Base}_{Z}$
29	5	adantr	$⊢ (φ \land (x \in B \land y \in B)) \to F \in (R MndHom S)$
30	29	adantr	$⊢ ((φ \land (x \in B \land y \in B)) \land w \in A) \to F \in (R MndHom S)$
31	29 6	syl	$⊢ (φ \land (x \in B \land y \in B)) \to R \in Mnd$
32	4	adantr	$⊢ (φ \land (x \in B \land y \in B)) \to A \in V$
33		simprl	$⊢ (φ \land (x \in B \land y \in B)) \to x \in B$
34	1 14 3 31 32 33	pwselbas	$⊢ (φ \land (x \in B \land y \in B)) \to x : A ⟶ {Base}_{R}$
35	34	ffvelrnda	$⊢ ((φ \land (x \in B \land y \in B)) \land w \in A) \to x (w) \in {Base}_{R}$
36		simprr	$⊢ (φ \land (x \in B \land y \in B)) \to y \in B$
37	1 14 3 31 32 36	pwselbas	$⊢ (φ \land (x \in B \land y \in B)) \to y : A ⟶ {Base}_{R}$
38	37	ffvelrnda	$⊢ ((φ \land (x \in B \land y \in B)) \land w \in A) \to y (w) \in {Base}_{R}$
39		eqid	$⊢ +_{R} = +_{R}$
40		eqid	$⊢ +_{S} = +_{S}$
41	14 39 40	mhmlin	$⊢ (F \in (R MndHom S) \land x (w) \in {Base}_{R} \land y (w) \in {Base}_{R}) \to F (x (w) +_{R} y (w)) = F (x (w)) +_{S} F (y (w))$
42	30 35 38 41	syl3anc	$⊢ ((φ \land (x \in B \land y \in B)) \land w \in A) \to F (x (w) +_{R} y (w)) = F (x (w)) +_{S} F (y (w))$
43	42	mpteq2dva	$⊢ (φ \land (x \in B \land y \in B)) \to (w \in A ⟼ F (x (w) +_{R} y (w))) = (w \in A ⟼ F (x (w)) +_{S} F (y (w)))$
44		fvexd	$⊢ ((φ \land (x \in B \land y \in B)) \land w \in A) \to F (x (w)) \in V$
45		fvexd	$⊢ ((φ \land (x \in B \land y \in B)) \land w \in A) \to F (y (w)) \in V$
46	34	feqmptd	$⊢ (φ \land (x \in B \land y \in B)) \to x = (w \in A ⟼ x (w))$
47	29 16	syl	$⊢ (φ \land (x \in B \land y \in B)) \to F : {Base}_{R} ⟶ {Base}_{S}$
48	47	feqmptd	$⊢ (φ \land (x \in B \land y \in B)) \to F = (z \in {Base}_{R} ⟼ F (z))$
49		fveq2	$⊢ z = x (w) \to F (z) = F (x (w))$
50	35 46 48 49	fmptco	$⊢ (φ \land (x \in B \land y \in B)) \to F \circ x = (w \in A ⟼ F (x (w)))$
51	37	feqmptd	$⊢ (φ \land (x \in B \land y \in B)) \to y = (w \in A ⟼ y (w))$
52		fveq2	$⊢ z = y (w) \to F (z) = F (y (w))$
53	38 51 48 52	fmptco	$⊢ (φ \land (x \in B \land y \in B)) \to F \circ y = (w \in A ⟼ F (y (w)))$
54	32 44 45 50 53	offval2	$⊢ (φ \land (x \in B \land y \in B)) \to (F \circ x) {+_{S}}_{f} (F \circ y) = (w \in A ⟼ F (x (w)) +_{S} F (y (w)))$
55	43 54	eqtr4d	$⊢ (φ \land (x \in B \land y \in B)) \to (w \in A ⟼ F (x (w) +_{R} y (w))) = (F \circ x) {+_{S}}_{f} (F \circ y)$
56	31	adantr	$⊢ ((φ \land (x \in B \land y \in B)) \land w \in A) \to R \in Mnd$
57	14 39	mndcl	$⊢ (R \in Mnd \land x (w) \in {Base}_{R} \land y (w) \in {Base}_{R}) \to x (w) +_{R} y (w) \in {Base}_{R}$
58	56 35 38 57	syl3anc	$⊢ ((φ \land (x \in B \land y \in B)) \land w \in A) \to x (w) +_{R} y (w) \in {Base}_{R}$
59		eqid	$⊢ +_{Y} = +_{Y}$
60	1 3 31 32 33 36 39 59	pwsplusgval	$⊢ (φ \land (x \in B \land y \in B)) \to x +_{Y} y = x {+_{R}}_{f} y$
61		fvexd	$⊢ ((φ \land (x \in B \land y \in B)) \land w \in A) \to x (w) \in V$
62		fvexd	$⊢ ((φ \land (x \in B \land y \in B)) \land w \in A) \to y (w) \in V$
63	32 61 62 46 51	offval2	$⊢ (φ \land (x \in B \land y \in B)) \to x {+_{R}}_{f} y = (w \in A ⟼ x (w) +_{R} y (w))$
64	60 63	eqtrd	$⊢ (φ \land (x \in B \land y \in B)) \to x +_{Y} y = (w \in A ⟼ x (w) +_{R} y (w))$
65		fveq2	$⊢ z = x (w) +_{R} y (w) \to F (z) = F (x (w) +_{R} y (w))$
66	58 64 48 65	fmptco	$⊢ (φ \land (x \in B \land y \in B)) \to F \circ (x +_{Y} y) = (w \in A ⟼ F (x (w) +_{R} y (w)))$
67	29 10	syl	$⊢ (φ \land (x \in B \land y \in B)) \to S \in Mnd$
68		fco	$⊢ (F : {Base}_{R} ⟶ {Base}_{S} \land x : A ⟶ {Base}_{R}) \to (F \circ x) : A ⟶ {Base}_{S}$
69	47 34 68	syl2anc	$⊢ (φ \land (x \in B \land y \in B)) \to (F \circ x) : A ⟶ {Base}_{S}$
70	2 15 24	pwselbasb	$⊢ (S \in Mnd \land A \in V) \to (F \circ x \in {Base}_{Z} \leftrightarrow (F \circ x) : A ⟶ {Base}_{S})$
71	67 32 70	syl2anc	$⊢ (φ \land (x \in B \land y \in B)) \to (F \circ x \in {Base}_{Z} \leftrightarrow (F \circ x) : A ⟶ {Base}_{S})$
72	69 71	mpbird	$⊢ (φ \land (x \in B \land y \in B)) \to F \circ x \in {Base}_{Z}$
73		fco	$⊢ (F : {Base}_{R} ⟶ {Base}_{S} \land y : A ⟶ {Base}_{R}) \to (F \circ y) : A ⟶ {Base}_{S}$
74	47 37 73	syl2anc	$⊢ (φ \land (x \in B \land y \in B)) \to (F \circ y) : A ⟶ {Base}_{S}$
75	2 15 24	pwselbasb	$⊢ (S \in Mnd \land A \in V) \to (F \circ y \in {Base}_{Z} \leftrightarrow (F \circ y) : A ⟶ {Base}_{S})$
76	67 32 75	syl2anc	$⊢ (φ \land (x \in B \land y \in B)) \to (F \circ y \in {Base}_{Z} \leftrightarrow (F \circ y) : A ⟶ {Base}_{S})$
77	74 76	mpbird	$⊢ (φ \land (x \in B \land y \in B)) \to F \circ y \in {Base}_{Z}$
78		eqid	$⊢ +_{Z} = +_{Z}$
79	2 24 67 32 72 77 40 78	pwsplusgval	$⊢ (φ \land (x \in B \land y \in B)) \to (F \circ x) +_{Z} (F \circ y) = (F \circ x) {+_{S}}_{f} (F \circ y)$
80	55 66 79	3eqtr4d	$⊢ (φ \land (x \in B \land y \in B)) \to F \circ (x +_{Y} y) = (F \circ x) +_{Z} (F \circ y)$
81		eqid	$⊢ (g \in B ⟼ F \circ g) = (g \in B ⟼ F \circ g)$
82		coeq2	$⊢ g = x +_{Y} y \to F \circ g = F \circ (x +_{Y} y)$
83	3 59	mndcl	$⊢ (Y \in Mnd \land x \in B \land y \in B) \to x +_{Y} y \in B$
84	83	3expb	$⊢ (Y \in Mnd \land (x \in B \land y \in B)) \to x +_{Y} y \in B$
85	9 84	sylan	$⊢ (φ \land (x \in B \land y \in B)) \to x +_{Y} y \in B$
86		coexg	$⊢ (F \in (R MndHom S) \land x +_{Y} y \in B) \to F \circ (x +_{Y} y) \in V$
87	5 85 86	syl2an2r	$⊢ (φ \land (x \in B \land y \in B)) \to F \circ (x +_{Y} y) \in V$
88	81 82 85 87	fvmptd3	$⊢ (φ \land (x \in B \land y \in B)) \to (g \in B ⟼ F \circ g) (x +_{Y} y) = F \circ (x +_{Y} y)$
89		coeq2	$⊢ g = x \to F \circ g = F \circ x$
90	81 89 33 72	fvmptd3	$⊢ (φ \land (x \in B \land y \in B)) \to (g \in B ⟼ F \circ g) (x) = F \circ x$
91		coeq2	$⊢ g = y \to F \circ g = F \circ y$
92	81 91 36 77	fvmptd3	$⊢ (φ \land (x \in B \land y \in B)) \to (g \in B ⟼ F \circ g) (y) = F \circ y$
93	90 92	oveq12d	$⊢ (φ \land (x \in B \land y \in B)) \to (g \in B ⟼ F \circ g) (x) +_{Z} (g \in B ⟼ F \circ g) (y) = (F \circ x) +_{Z} (F \circ y)$
94	80 88 93	3eqtr4d	$⊢ (φ \land (x \in B \land y \in B)) \to (g \in B ⟼ F \circ g) (x +_{Y} y) = (g \in B ⟼ F \circ g) (x) +_{Z} (g \in B ⟼ F \circ g) (y)$
95	94	ralrimivva	$⊢ φ \to \forall x \in B \forall y \in B (g \in B ⟼ F \circ g) (x +_{Y} y) = (g \in B ⟼ F \circ g) (x) +_{Z} (g \in B ⟼ F \circ g) (y)$
96		coeq2	$⊢ g = 0_{Y} \to F \circ g = F \circ 0_{Y}$
97		eqid	$⊢ 0_{Y} = 0_{Y}$
98	3 97	mndidcl	$⊢ Y \in Mnd \to 0_{Y} \in B$
99	9 98	syl	$⊢ φ \to 0_{Y} \in B$
100		coexg	$⊢ (F \in (R MndHom S) \land 0_{Y} \in B) \to F \circ 0_{Y} \in V$
101	5 99 100	syl2anc	$⊢ φ \to F \circ 0_{Y} \in V$
102	81 96 99 101	fvmptd3	$⊢ φ \to (g \in B ⟼ F \circ g) (0_{Y}) = F \circ 0_{Y}$
103	17	ffnd	$⊢ φ \to F Fn {Base}_{R}$
104		eqid	$⊢ 0_{R} = 0_{R}$
105	14 104	mndidcl	$⊢ R \in Mnd \to 0_{R} \in {Base}_{R}$
106	7 105	syl	$⊢ φ \to 0_{R} \in {Base}_{R}$
107		fcoconst	$⊢ (F Fn {Base}_{R} \land 0_{R} \in {Base}_{R}) \to F \circ (A \times \{0_{R}\}) = A \times \{F (0_{R})\}$
108	103 106 107	syl2anc	$⊢ φ \to F \circ (A \times \{0_{R}\}) = A \times \{F (0_{R})\}$
109	1 104	pws0g	$⊢ (R \in Mnd \land A \in V) \to A \times \{0_{R}\} = 0_{Y}$
110	7 4 109	syl2anc	$⊢ φ \to A \times \{0_{R}\} = 0_{Y}$
111	110	coeq2d	$⊢ φ \to F \circ (A \times \{0_{R}\}) = F \circ 0_{Y}$
112		eqid	$⊢ 0_{S} = 0_{S}$
113	104 112	mhm0	$⊢ F \in (R MndHom S) \to F (0_{R}) = 0_{S}$
114	5 113	syl	$⊢ φ \to F (0_{R}) = 0_{S}$
115	114	sneqd	$⊢ φ \to \{F (0_{R})\} = \{0_{S}\}$
116	115	xpeq2d	$⊢ φ \to A \times \{F (0_{R})\} = A \times \{0_{S}\}$
117	108 111 116	3eqtr3d	$⊢ φ \to F \circ 0_{Y} = A \times \{0_{S}\}$
118	2 112	pws0g	$⊢ (S \in Mnd \land A \in V) \to A \times \{0_{S}\} = 0_{Z}$
119	11 4 118	syl2anc	$⊢ φ \to A \times \{0_{S}\} = 0_{Z}$
120	102 117 119	3eqtrd	$⊢ φ \to (g \in B ⟼ F \circ g) (0_{Y}) = 0_{Z}$
121	28 95 120	3jca	$⊢ φ \to ((g \in B ⟼ F \circ g) : B ⟶ {Base}_{Z} \land \forall x \in B \forall y \in B (g \in B ⟼ F \circ g) (x +_{Y} y) = (g \in B ⟼ F \circ g) (x) +_{Z} (g \in B ⟼ F \circ g) (y) \land (g \in B ⟼ F \circ g) (0_{Y}) = 0_{Z})$
122		eqid	$⊢ 0_{Z} = 0_{Z}$
123	3 24 59 78 97 122	ismhm	$⊢ (g \in B ⟼ F \circ g) \in (Y MndHom Z) \leftrightarrow ((Y \in Mnd \land Z \in Mnd) \land ((g \in B ⟼ F \circ g) : B ⟶ {Base}_{Z} \land \forall x \in B \forall y \in B (g \in B ⟼ F \circ g) (x +_{Y} y) = (g \in B ⟼ F \circ g) (x) +_{Z} (g \in B ⟼ F \circ g) (y) \land (g \in B ⟼ F \circ g) (0_{Y}) = 0_{Z}))$
124	9 13 121 123	syl21anbrc	$⊢ φ \to (g \in B ⟼ F \circ g) \in (Y MndHom Z)$

Metamath Proof Explorer

Theorem pwsco2mhm

Proof