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	7 5	fexd	$⊢ φ \to F \in V$
73	72	adantr	$⊢ (φ \land (x \in C \land y \in C)) \to F \in V$
74		coexg	$⊢ (x +_{Z} y \in V \land F \in V) \to (x +_{Z} y) \circ F \in V$
75	71 73 74	sylancr	$⊢ (φ \land (x \in C \land y \in C)) \to (x +_{Z} y) \circ F \in V$
76	66 67 70 75	fvmptd3	$⊢ (φ \land (x \in C \land y \in C)) \to (g \in C ⟼ g \circ F) (x +_{Z} y) = (x +_{Z} y) \circ F$
77		coeq1	$⊢ g = x \to g \circ F = x \circ F$
78		coexg	$⊢ (x \in C \land F \in V) \to x \circ F \in V$
79	33 73 78	syl2anc	$⊢ (φ \land (x \in C \land y \in C)) \to x \circ F \in V$
80	66 77 33 79	fvmptd3	$⊢ (φ \land (x \in C \land y \in C)) \to (g \in C ⟼ g \circ F) (x) = x \circ F$
81		coeq1	$⊢ g = y \to g \circ F = y \circ F$
82		coexg	$⊢ (y \in C \land F \in V) \to y \circ F \in V$
83	38 73 82	syl2anc	$⊢ (φ \land (x \in C \land y \in C)) \to y \circ F \in V$
84	66 81 38 83	fvmptd3	$⊢ (φ \land (x \in C \land y \in C)) \to (g \in C ⟼ g \circ F) (y) = y \circ F$
85	80 84	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)$
86	65 76 85	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)$
87	86	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)$
88		coeq1	$⊢ g = 0_{Z} \to g \circ F = 0_{Z} \circ F$
89		eqid	$⊢ 0_{Z} = 0_{Z}$
90	3 89	mndidcl	$⊢ Z \in Mnd \to 0_{Z} \in C$
91	9 90	syl	$⊢ φ \to 0_{Z} \in C$
92		coexg	$⊢ (0_{Z} \in C \land F \in V) \to 0_{Z} \circ F \in V$
93	91 72 92	syl2anc	$⊢ φ \to 0_{Z} \circ F \in V$
94	66 88 91 93	fvmptd3	$⊢ φ \to (g \in C ⟼ g \circ F) (0_{Z}) = 0_{Z} \circ F$
95	2 12 3 4 6 91	pwselbas	$⊢ φ \to 0_{Z} : B ⟶ {Base}_{R}$
96		fco	$⊢ (0_{Z} : B ⟶ {Base}_{R} \land F : A ⟶ B) \to (0_{Z} \circ F) : A ⟶ {Base}_{R}$
97	95 7 96	syl2anc	$⊢ φ \to (0_{Z} \circ F) : A ⟶ {Base}_{R}$
98	97	ffnd	$⊢ φ \to (0_{Z} \circ F) Fn A$
99		fvexd	$⊢ φ \to 0_{R} \in V$
100		fnconstg	$⊢ 0_{R} \in V \to (A \times \{0_{R}\}) Fn A$
101	99 100	syl	$⊢ φ \to (A \times \{0_{R}\}) Fn A$
102		eqid	$⊢ 0_{R} = 0_{R}$
103	2 102	pws0g	$⊢ (R \in Mnd \land B \in W) \to B \times \{0_{R}\} = 0_{Z}$
104	4 6 103	syl2anc	$⊢ φ \to B \times \{0_{R}\} = 0_{Z}$
105	104	fveq1d	$⊢ φ \to (B \times \{0_{R}\}) (F (x)) = 0_{Z} (F (x))$
106	105	adantr	$⊢ (φ \land x \in A) \to (B \times \{0_{R}\}) (F (x)) = 0_{Z} (F (x))$
107		fvex	$⊢ 0_{R} \in V$
108	7	ffvelrnda	$⊢ (φ \land x \in A) \to F (x) \in B$
109		fvconst2g	$⊢ (0_{R} \in V \land F (x) \in B) \to (B \times \{0_{R}\}) (F (x)) = 0_{R}$
110	107 108 109	sylancr	$⊢ (φ \land x \in A) \to (B \times \{0_{R}\}) (F (x)) = 0_{R}$
111	106 110	eqtr3d	$⊢ (φ \land x \in A) \to 0_{Z} (F (x)) = 0_{R}$
112		fvco3	$⊢ (F : A ⟶ B \land x \in A) \to (0_{Z} \circ F) (x) = 0_{Z} (F (x))$
113	7 112	sylan	$⊢ (φ \land x \in A) \to (0_{Z} \circ F) (x) = 0_{Z} (F (x))$
114		fvconst2g	$⊢ (0_{R} \in V \land x \in A) \to (A \times \{0_{R}\}) (x) = 0_{R}$
115	99 114	sylan	$⊢ (φ \land x \in A) \to (A \times \{0_{R}\}) (x) = 0_{R}$
116	111 113 115	3eqtr4d	$⊢ (φ \land x \in A) \to (0_{Z} \circ F) (x) = (A \times \{0_{R}\}) (x)$
117	98 101 116	eqfnfvd	$⊢ φ \to 0_{Z} \circ F = A \times \{0_{R}\}$
118	1 102	pws0g	$⊢ (R \in Mnd \land A \in V) \to A \times \{0_{R}\} = 0_{Y}$
119	4 5 118	syl2anc	$⊢ φ \to A \times \{0_{R}\} = 0_{Y}$
120	94 117 119	3eqtrd	$⊢ φ \to (g \in C ⟼ g \circ F) (0_{Z}) = 0_{Y}$
121	24 87 120	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})$
122		eqid	$⊢ 0_{Y} = 0_{Y}$
123	3 19 57 55 89 122	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}))$
124	9 11 121 123	syl21anbrc	$⊢ φ \to (g \in C ⟼ g \circ F) \in (Z MndHom Y)$

Metamath Proof Explorer

Theorem pwsco1mhm

Proof