pwsco1mhm

Description: Right composition with a function on the index sets yields a monoid homomorphism of structure powers. (Contributed by Mario Carneiro, 12-Jun-2015)

	Ref	Expression
Hypotheses	pwsco1mhm.y	$⊢ Y = R ↑_{𝑠} A$
	pwsco1mhm.z	$⊢ Z = R ↑_{𝑠} B$
	pwsco1mhm.c	$⊢ C = {Base}_{Z}$
	pwsco1mhm.r	$⊢ φ \to R \in Mnd$
	pwsco1mhm.a	$⊢ φ \to A \in V$
	pwsco1mhm.b	$⊢ φ \to B \in W$
	pwsco1mhm.f	$⊢ φ \to F : A ⟶ B$
Assertion	pwsco1mhm	$⊢ φ \to (g \in C ⟼ g \circ F) \in (Z MndHom Y)$

Proof

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

Metamath Proof Explorer

Theorem pwsco1mhm

Proof