pwssplit2

Description: Splitting for structure powers, part 2: restriction is a group homomorphism. (Contributed by Stefan O'Rear, 24-Jan-2015)

	Ref	Expression
Hypotheses	pwssplit1.y	$⊢ Y = W ↑_{𝑠} U$
	pwssplit1.z	$⊢ Z = W ↑_{𝑠} V$
	pwssplit1.b	$⊢ B = {Base}_{Y}$
	pwssplit1.c	$⊢ C = {Base}_{Z}$
	pwssplit1.f	$⊢ F = (x \in B ⟼ {x ↾}_{V})$
Assertion	pwssplit2	$⊢ (W \in Grp \land U \in X \land V \subseteq U) \to F \in (Y GrpHom Z)$

Proof

Step	Hyp	Ref	Expression
1		pwssplit1.y	$⊢ Y = W ↑_{𝑠} U$
2		pwssplit1.z	$⊢ Z = W ↑_{𝑠} V$
3		pwssplit1.b	$⊢ B = {Base}_{Y}$
4		pwssplit1.c	$⊢ C = {Base}_{Z}$
5		pwssplit1.f	$⊢ F = (x \in B ⟼ {x ↾}_{V})$
6		eqid	$⊢ +_{Y} = +_{Y}$
7		eqid	$⊢ +_{Z} = +_{Z}$
8		simp1	$⊢ (W \in Grp \land U \in X \land V \subseteq U) \to W \in Grp$
9		simp2	$⊢ (W \in Grp \land U \in X \land V \subseteq U) \to U \in X$
10	1	pwsgrp	$⊢ (W \in Grp \land U \in X) \to Y \in Grp$
11	8 9 10	syl2anc	$⊢ (W \in Grp \land U \in X \land V \subseteq U) \to Y \in Grp$
12		simp3	$⊢ (W \in Grp \land U \in X \land V \subseteq U) \to V \subseteq U$
13	9 12	ssexd	$⊢ (W \in Grp \land U \in X \land V \subseteq U) \to V \in V$
14	2	pwsgrp	$⊢ (W \in Grp \land V \in V) \to Z \in Grp$
15	8 13 14	syl2anc	$⊢ (W \in Grp \land U \in X \land V \subseteq U) \to Z \in Grp$
16	1 2 3 4 5	pwssplit0	$⊢ (W \in Grp \land U \in X \land V \subseteq U) \to F : B ⟶ C$
17		offres	$⊢ (a \in B \land b \in B) \to {(a {+_{W}}_{f} b) ↾}_{V} = ({a ↾}_{V}) {+_{W}}_{f} ({b ↾}_{V})$
18	17	adantl	$⊢ ((W \in Grp \land U \in X \land V \subseteq U) \land (a \in B \land b \in B)) \to {(a {+_{W}}_{f} b) ↾}_{V} = ({a ↾}_{V}) {+_{W}}_{f} ({b ↾}_{V})$
19	8	adantr	$⊢ ((W \in Grp \land U \in X \land V \subseteq U) \land (a \in B \land b \in B)) \to W \in Grp$
20		simpl2	$⊢ ((W \in Grp \land U \in X \land V \subseteq U) \land (a \in B \land b \in B)) \to U \in X$
21		simprl	$⊢ ((W \in Grp \land U \in X \land V \subseteq U) \land (a \in B \land b \in B)) \to a \in B$
22		simprr	$⊢ ((W \in Grp \land U \in X \land V \subseteq U) \land (a \in B \land b \in B)) \to b \in B$
23		eqid	$⊢ +_{W} = +_{W}$
24	1 3 19 20 21 22 23 6	pwsplusgval	$⊢ ((W \in Grp \land U \in X \land V \subseteq U) \land (a \in B \land b \in B)) \to a +_{Y} b = a {+_{W}}_{f} b$
25	24	reseq1d	$⊢ ((W \in Grp \land U \in X \land V \subseteq U) \land (a \in B \land b \in B)) \to {(a +_{Y} b) ↾}_{V} = {(a {+_{W}}_{f} b) ↾}_{V}$
26	5	fvtresfn	$⊢ a \in B \to F (a) = {a ↾}_{V}$
27	5	fvtresfn	$⊢ b \in B \to F (b) = {b ↾}_{V}$
28	26 27	oveqan12d	$⊢ (a \in B \land b \in B) \to F (a) {+_{W}}_{f} F (b) = ({a ↾}_{V}) {+_{W}}_{f} ({b ↾}_{V})$
29	28	adantl	$⊢ ((W \in Grp \land U \in X \land V \subseteq U) \land (a \in B \land b \in B)) \to F (a) {+_{W}}_{f} F (b) = ({a ↾}_{V}) {+_{W}}_{f} ({b ↾}_{V})$
30	18 25 29	3eqtr4d	$⊢ ((W \in Grp \land U \in X \land V \subseteq U) \land (a \in B \land b \in B)) \to {(a +_{Y} b) ↾}_{V} = F (a) {+_{W}}_{f} F (b)$
31	3 6	grpcl	$⊢ (Y \in Grp \land a \in B \land b \in B) \to a +_{Y} b \in B$
32	31	3expb	$⊢ (Y \in Grp \land (a \in B \land b \in B)) \to a +_{Y} b \in B$
33	11 32	sylan	$⊢ ((W \in Grp \land U \in X \land V \subseteq U) \land (a \in B \land b \in B)) \to a +_{Y} b \in B$
34	5	fvtresfn	$⊢ a +_{Y} b \in B \to F (a +_{Y} b) = {(a +_{Y} b) ↾}_{V}$
35	33 34	syl	$⊢ ((W \in Grp \land U \in X \land V \subseteq U) \land (a \in B \land b \in B)) \to F (a +_{Y} b) = {(a +_{Y} b) ↾}_{V}$
36	13	adantr	$⊢ ((W \in Grp \land U \in X \land V \subseteq U) \land (a \in B \land b \in B)) \to V \in V$
37	16	ffvelcdmda	$⊢ ((W \in Grp \land U \in X \land V \subseteq U) \land a \in B) \to F (a) \in C$
38	37	adantrr	$⊢ ((W \in Grp \land U \in X \land V \subseteq U) \land (a \in B \land b \in B)) \to F (a) \in C$
39	16	ffvelcdmda	$⊢ ((W \in Grp \land U \in X \land V \subseteq U) \land b \in B) \to F (b) \in C$
40	39	adantrl	$⊢ ((W \in Grp \land U \in X \land V \subseteq U) \land (a \in B \land b \in B)) \to F (b) \in C$
41	2 4 19 36 38 40 23 7	pwsplusgval	$⊢ ((W \in Grp \land U \in X \land V \subseteq U) \land (a \in B \land b \in B)) \to F (a) +_{Z} F (b) = F (a) {+_{W}}_{f} F (b)$
42	30 35 41	3eqtr4d	$⊢ ((W \in Grp \land U \in X \land V \subseteq U) \land (a \in B \land b \in B)) \to F (a +_{Y} b) = F (a) +_{Z} F (b)$
43	3 4 6 7 11 15 16 42	isghmd	$⊢ (W \in Grp \land U \in X \land V \subseteq U) \to F \in (Y GrpHom Z)$

Metamath Proof Explorer

Theorem pwssplit2

Proof