pwssplit3

Description: Splitting for structure powers, part 3: restriction is a module 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	pwssplit3	$⊢ (W \in LMod \land U \in X \land V \subseteq U) \to F \in (Y LMHom 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	$⊢ \cdot_{Y} = \cdot_{Y}$
7		eqid	$⊢ \cdot_{Z} = \cdot_{Z}$
8		eqid	$⊢ Scalar (Y) = Scalar (Y)$
9		eqid	$⊢ Scalar (Z) = Scalar (Z)$
10		eqid	$⊢ {Base}_{Scalar (Y)} = {Base}_{Scalar (Y)}$
11		simp1	$⊢ (W \in LMod \land U \in X \land V \subseteq U) \to W \in LMod$
12		simp2	$⊢ (W \in LMod \land U \in X \land V \subseteq U) \to U \in X$
13	1	pwslmod	$⊢ (W \in LMod \land U \in X) \to Y \in LMod$
14	11 12 13	syl2anc	$⊢ (W \in LMod \land U \in X \land V \subseteq U) \to Y \in LMod$
15		simp3	$⊢ (W \in LMod \land U \in X \land V \subseteq U) \to V \subseteq U$
16	12 15	ssexd	$⊢ (W \in LMod \land U \in X \land V \subseteq U) \to V \in V$
17	2	pwslmod	$⊢ (W \in LMod \land V \in V) \to Z \in LMod$
18	11 16 17	syl2anc	$⊢ (W \in LMod \land U \in X \land V \subseteq U) \to Z \in LMod$
19		eqid	$⊢ Scalar (W) = Scalar (W)$
20	2 19	pwssca	$⊢ (W \in LMod \land V \in V) \to Scalar (W) = Scalar (Z)$
21	11 16 20	syl2anc	$⊢ (W \in LMod \land U \in X \land V \subseteq U) \to Scalar (W) = Scalar (Z)$
22	1 19	pwssca	$⊢ (W \in LMod \land U \in X) \to Scalar (W) = Scalar (Y)$
23	11 12 22	syl2anc	$⊢ (W \in LMod \land U \in X \land V \subseteq U) \to Scalar (W) = Scalar (Y)$
24	21 23	eqtr3d	$⊢ (W \in LMod \land U \in X \land V \subseteq U) \to Scalar (Z) = Scalar (Y)$
25		lmodgrp	$⊢ W \in LMod \to W \in Grp$
26	1 2 3 4 5	pwssplit2	$⊢ (W \in Grp \land U \in X \land V \subseteq U) \to F \in (Y GrpHom Z)$
27	25 26	syl3an1	$⊢ (W \in LMod \land U \in X \land V \subseteq U) \to F \in (Y GrpHom Z)$
28		snex	$⊢ \{a\} \in V$
29		xpexg	$⊢ (U \in X \land \{a\} \in V) \to U \times \{a\} \in V$
30	12 28 29	sylancl	$⊢ (W \in LMod \land U \in X \land V \subseteq U) \to U \times \{a\} \in V$
31		vex	$⊢ b \in V$
32		offres	$⊢ (U \times \{a\} \in V \land b \in V) \to {((U \times \{a\}) {\cdot_{W}}_{f} b) ↾}_{V} = ({(U \times \{a\}) ↾}_{V}) {\cdot_{W}}_{f} ({b ↾}_{V})$
33	30 31 32	sylancl	$⊢ (W \in LMod \land U \in X \land V \subseteq U) \to {((U \times \{a\}) {\cdot_{W}}_{f} b) ↾}_{V} = ({(U \times \{a\}) ↾}_{V}) {\cdot_{W}}_{f} ({b ↾}_{V})$
34	33	adantr	$⊢ ((W \in LMod \land U \in X \land V \subseteq U) \land (a \in {Base}_{Scalar (Y)} \land b \in B)) \to {((U \times \{a\}) {\cdot_{W}}_{f} b) ↾}_{V} = ({(U \times \{a\}) ↾}_{V}) {\cdot_{W}}_{f} ({b ↾}_{V})$
35		xpssres	$⊢ V \subseteq U \to {(U \times \{a\}) ↾}_{V} = V \times \{a\}$
36	35	3ad2ant3	$⊢ (W \in LMod \land U \in X \land V \subseteq U) \to {(U \times \{a\}) ↾}_{V} = V \times \{a\}$
37	36	adantr	$⊢ ((W \in LMod \land U \in X \land V \subseteq U) \land (a \in {Base}_{Scalar (Y)} \land b \in B)) \to {(U \times \{a\}) ↾}_{V} = V \times \{a\}$
38	37	oveq1d	$⊢ ((W \in LMod \land U \in X \land V \subseteq U) \land (a \in {Base}_{Scalar (Y)} \land b \in B)) \to ({(U \times \{a\}) ↾}_{V}) {\cdot_{W}}_{f} ({b ↾}_{V}) = (V \times \{a\}) {\cdot_{W}}_{f} ({b ↾}_{V})$
39	34 38	eqtrd	$⊢ ((W \in LMod \land U \in X \land V \subseteq U) \land (a \in {Base}_{Scalar (Y)} \land b \in B)) \to {((U \times \{a\}) {\cdot_{W}}_{f} b) ↾}_{V} = (V \times \{a\}) {\cdot_{W}}_{f} ({b ↾}_{V})$
40		eqid	$⊢ \cdot_{W} = \cdot_{W}$
41		eqid	$⊢ {Base}_{Scalar (W)} = {Base}_{Scalar (W)}$
42		simpl1	$⊢ ((W \in LMod \land U \in X \land V \subseteq U) \land (a \in {Base}_{Scalar (Y)} \land b \in B)) \to W \in LMod$
43		simpl2	$⊢ ((W \in LMod \land U \in X \land V \subseteq U) \land (a \in {Base}_{Scalar (Y)} \land b \in B)) \to U \in X$
44	23	fveq2d	$⊢ (W \in LMod \land U \in X \land V \subseteq U) \to {Base}_{Scalar (W)} = {Base}_{Scalar (Y)}$
45	44	eleq2d	$⊢ (W \in LMod \land U \in X \land V \subseteq U) \to (a \in {Base}_{Scalar (W)} \leftrightarrow a \in {Base}_{Scalar (Y)})$
46	45	biimpar	$⊢ ((W \in LMod \land U \in X \land V \subseteq U) \land a \in {Base}_{Scalar (Y)}) \to a \in {Base}_{Scalar (W)}$
47	46	adantrr	$⊢ ((W \in LMod \land U \in X \land V \subseteq U) \land (a \in {Base}_{Scalar (Y)} \land b \in B)) \to a \in {Base}_{Scalar (W)}$
48		simprr	$⊢ ((W \in LMod \land U \in X \land V \subseteq U) \land (a \in {Base}_{Scalar (Y)} \land b \in B)) \to b \in B$
49	1 3 40 6 19 41 42 43 47 48	pwsvscafval	$⊢ ((W \in LMod \land U \in X \land V \subseteq U) \land (a \in {Base}_{Scalar (Y)} \land b \in B)) \to a \cdot_{Y} b = (U \times \{a\}) {\cdot_{W}}_{f} b$
50	49	reseq1d	$⊢ ((W \in LMod \land U \in X \land V \subseteq U) \land (a \in {Base}_{Scalar (Y)} \land b \in B)) \to {(a \cdot_{Y} b) ↾}_{V} = {((U \times \{a\}) {\cdot_{W}}_{f} b) ↾}_{V}$
51	5	fvtresfn	$⊢ b \in B \to F (b) = {b ↾}_{V}$
52	51	ad2antll	$⊢ ((W \in LMod \land U \in X \land V \subseteq U) \land (a \in {Base}_{Scalar (Y)} \land b \in B)) \to F (b) = {b ↾}_{V}$
53	52	oveq2d	$⊢ ((W \in LMod \land U \in X \land V \subseteq U) \land (a \in {Base}_{Scalar (Y)} \land b \in B)) \to (V \times \{a\}) {\cdot_{W}}_{f} F (b) = (V \times \{a\}) {\cdot_{W}}_{f} ({b ↾}_{V})$
54	39 50 53	3eqtr4d	$⊢ ((W \in LMod \land U \in X \land V \subseteq U) \land (a \in {Base}_{Scalar (Y)} \land b \in B)) \to {(a \cdot_{Y} b) ↾}_{V} = (V \times \{a\}) {\cdot_{W}}_{f} F (b)$
55	3 8 6 10	lmodvscl	$⊢ (Y \in LMod \land a \in {Base}_{Scalar (Y)} \land b \in B) \to a \cdot_{Y} b \in B$
56	55	3expb	$⊢ (Y \in LMod \land (a \in {Base}_{Scalar (Y)} \land b \in B)) \to a \cdot_{Y} b \in B$
57	14 56	sylan	$⊢ ((W \in LMod \land U \in X \land V \subseteq U) \land (a \in {Base}_{Scalar (Y)} \land b \in B)) \to a \cdot_{Y} b \in B$
58	5	fvtresfn	$⊢ a \cdot_{Y} b \in B \to F (a \cdot_{Y} b) = {(a \cdot_{Y} b) ↾}_{V}$
59	57 58	syl	$⊢ ((W \in LMod \land U \in X \land V \subseteq U) \land (a \in {Base}_{Scalar (Y)} \land b \in B)) \to F (a \cdot_{Y} b) = {(a \cdot_{Y} b) ↾}_{V}$
60	16	adantr	$⊢ ((W \in LMod \land U \in X \land V \subseteq U) \land (a \in {Base}_{Scalar (Y)} \land b \in B)) \to V \in V$
61	1 2 3 4 5	pwssplit0	$⊢ (W \in LMod \land U \in X \land V \subseteq U) \to F : B ⟶ C$
62	61	ffvelrnda	$⊢ ((W \in LMod \land U \in X \land V \subseteq U) \land b \in B) \to F (b) \in C$
63	62	adantrl	$⊢ ((W \in LMod \land U \in X \land V \subseteq U) \land (a \in {Base}_{Scalar (Y)} \land b \in B)) \to F (b) \in C$
64	2 4 40 7 19 41 42 60 47 63	pwsvscafval	$⊢ ((W \in LMod \land U \in X \land V \subseteq U) \land (a \in {Base}_{Scalar (Y)} \land b \in B)) \to a \cdot_{Z} F (b) = (V \times \{a\}) {\cdot_{W}}_{f} F (b)$
65	54 59 64	3eqtr4d	$⊢ ((W \in LMod \land U \in X \land V \subseteq U) \land (a \in {Base}_{Scalar (Y)} \land b \in B)) \to F (a \cdot_{Y} b) = a \cdot_{Z} F (b)$
66	3 6 7 8 9 10 14 18 24 27 65	islmhmd	$⊢ (W \in LMod \land U \in X \land V \subseteq U) \to F \in (Y LMHom Z)$

Metamath Proof Explorer

Theorem pwssplit3

Proof