pwssplit1

Description: Splitting for structure powers, part 1: restriction is an onto function. The only actual monoid law we need here is that the base set is nonempty. (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	pwssplit1	$⊢ (W \in Mnd \land U \in X \land V \subseteq U) \to F : B \underset{onto}{⟶} C$

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	1 2 3 4 5	pwssplit0	$⊢ (W \in Mnd \land U \in X \land V \subseteq U) \to F : B ⟶ C$
7		simp1	$⊢ (W \in Mnd \land U \in X \land V \subseteq U) \to W \in Mnd$
8		simp2	$⊢ (W \in Mnd \land U \in X \land V \subseteq U) \to U \in X$
9		simp3	$⊢ (W \in Mnd \land U \in X \land V \subseteq U) \to V \subseteq U$
10	8 9	ssexd	$⊢ (W \in Mnd \land U \in X \land V \subseteq U) \to V \in V$
11		eqid	$⊢ {Base}_{W} = {Base}_{W}$
12	2 11 4	pwselbasb	$⊢ (W \in Mnd \land V \in V) \to (a \in C \leftrightarrow a : V ⟶ {Base}_{W})$
13	7 10 12	syl2anc	$⊢ (W \in Mnd \land U \in X \land V \subseteq U) \to (a \in C \leftrightarrow a : V ⟶ {Base}_{W})$
14	13	biimpa	$⊢ ((W \in Mnd \land U \in X \land V \subseteq U) \land a \in C) \to a : V ⟶ {Base}_{W}$
15		fvex	$⊢ 0_{W} \in V$
16	15	fconst	$⊢ ((U ∖ V) \times \{0_{W}\}) : U ∖ V ⟶ \{0_{W}\}$
17	16	a1i	$⊢ ((W \in Mnd \land U \in X \land V \subseteq U) \land a \in C) \to ((U ∖ V) \times \{0_{W}\}) : U ∖ V ⟶ \{0_{W}\}$
18		simpl1	$⊢ ((W \in Mnd \land U \in X \land V \subseteq U) \land a \in C) \to W \in Mnd$
19		eqid	$⊢ 0_{W} = 0_{W}$
20	11 19	mndidcl	$⊢ W \in Mnd \to 0_{W} \in {Base}_{W}$
21	18 20	syl	$⊢ ((W \in Mnd \land U \in X \land V \subseteq U) \land a \in C) \to 0_{W} \in {Base}_{W}$
22	21	snssd	$⊢ ((W \in Mnd \land U \in X \land V \subseteq U) \land a \in C) \to \{0_{W}\} \subseteq {Base}_{W}$
23	17 22	fssd	$⊢ ((W \in Mnd \land U \in X \land V \subseteq U) \land a \in C) \to ((U ∖ V) \times \{0_{W}\}) : U ∖ V ⟶ {Base}_{W}$
24		disjdif	$⊢ V \cap (U ∖ V) = \emptyset$
25	24	a1i	$⊢ ((W \in Mnd \land U \in X \land V \subseteq U) \land a \in C) \to V \cap (U ∖ V) = \emptyset$
26		fun	$⊢ ((a : V ⟶ {Base}_{W} \land ((U ∖ V) \times \{0_{W}\}) : U ∖ V ⟶ {Base}_{W}) \land V \cap (U ∖ V) = \emptyset) \to (a \cup ((U ∖ V) \times \{0_{W}\})) : V \cup (U ∖ V) ⟶ {Base}_{W} \cup {Base}_{W}$
27	14 23 25 26	syl21anc	$⊢ ((W \in Mnd \land U \in X \land V \subseteq U) \land a \in C) \to (a \cup ((U ∖ V) \times \{0_{W}\})) : V \cup (U ∖ V) ⟶ {Base}_{W} \cup {Base}_{W}$
28		simpl3	$⊢ ((W \in Mnd \land U \in X \land V \subseteq U) \land a \in C) \to V \subseteq U$
29		undif	$⊢ V \subseteq U \leftrightarrow V \cup (U ∖ V) = U$
30	28 29	sylib	$⊢ ((W \in Mnd \land U \in X \land V \subseteq U) \land a \in C) \to V \cup (U ∖ V) = U$
31		unidm	$⊢ {Base}_{W} \cup {Base}_{W} = {Base}_{W}$
32	31	a1i	$⊢ ((W \in Mnd \land U \in X \land V \subseteq U) \land a \in C) \to {Base}_{W} \cup {Base}_{W} = {Base}_{W}$
33	30 32	feq23d	$⊢ ((W \in Mnd \land U \in X \land V \subseteq U) \land a \in C) \to ((a \cup ((U ∖ V) \times \{0_{W}\})) : V \cup (U ∖ V) ⟶ {Base}_{W} \cup {Base}_{W} \leftrightarrow (a \cup ((U ∖ V) \times \{0_{W}\})) : U ⟶ {Base}_{W})$
34	27 33	mpbid	$⊢ ((W \in Mnd \land U \in X \land V \subseteq U) \land a \in C) \to (a \cup ((U ∖ V) \times \{0_{W}\})) : U ⟶ {Base}_{W}$
35		simpl2	$⊢ ((W \in Mnd \land U \in X \land V \subseteq U) \land a \in C) \to U \in X$
36	1 11 3	pwselbasb	$⊢ (W \in Mnd \land U \in X) \to (a \cup ((U ∖ V) \times \{0_{W}\}) \in B \leftrightarrow (a \cup ((U ∖ V) \times \{0_{W}\})) : U ⟶ {Base}_{W})$
37	18 35 36	syl2anc	$⊢ ((W \in Mnd \land U \in X \land V \subseteq U) \land a \in C) \to (a \cup ((U ∖ V) \times \{0_{W}\}) \in B \leftrightarrow (a \cup ((U ∖ V) \times \{0_{W}\})) : U ⟶ {Base}_{W})$
38	34 37	mpbird	$⊢ ((W \in Mnd \land U \in X \land V \subseteq U) \land a \in C) \to a \cup ((U ∖ V) \times \{0_{W}\}) \in B$
39	5	fvtresfn	$⊢ a \cup ((U ∖ V) \times \{0_{W}\}) \in B \to F (a \cup ((U ∖ V) \times \{0_{W}\})) = {(a \cup ((U ∖ V) \times \{0_{W}\})) ↾}_{V}$
40	38 39	syl	$⊢ ((W \in Mnd \land U \in X \land V \subseteq U) \land a \in C) \to F (a \cup ((U ∖ V) \times \{0_{W}\})) = {(a \cup ((U ∖ V) \times \{0_{W}\})) ↾}_{V}$
41		resundir	$⊢ {(a \cup ((U ∖ V) \times \{0_{W}\})) ↾}_{V} = ({a ↾}_{V}) \cup ({((U ∖ V) \times \{0_{W}\}) ↾}_{V})$
42		ffn	$⊢ a : V ⟶ {Base}_{W} \to a Fn V$
43		fnresdm	$⊢ a Fn V \to {a ↾}_{V} = a$
44	14 42 43	3syl	$⊢ ((W \in Mnd \land U \in X \land V \subseteq U) \land a \in C) \to {a ↾}_{V} = a$
45		disjdifr	$⊢ (U ∖ V) \cap V = \emptyset$
46		fnconstg	$⊢ 0_{W} \in V \to ((U ∖ V) \times \{0_{W}\}) Fn (U ∖ V)$
47	15 46	ax-mp	$⊢ ((U ∖ V) \times \{0_{W}\}) Fn (U ∖ V)$
48		fnresdisj	$⊢ ((U ∖ V) \times \{0_{W}\}) Fn (U ∖ V) \to ((U ∖ V) \cap V = \emptyset \leftrightarrow {((U ∖ V) \times \{0_{W}\}) ↾}_{V} = \emptyset)$
49	47 48	mp1i	$⊢ ((W \in Mnd \land U \in X \land V \subseteq U) \land a \in C) \to ((U ∖ V) \cap V = \emptyset \leftrightarrow {((U ∖ V) \times \{0_{W}\}) ↾}_{V} = \emptyset)$
50	45 49	mpbii	$⊢ ((W \in Mnd \land U \in X \land V \subseteq U) \land a \in C) \to {((U ∖ V) \times \{0_{W}\}) ↾}_{V} = \emptyset$
51	44 50	uneq12d	$⊢ ((W \in Mnd \land U \in X \land V \subseteq U) \land a \in C) \to ({a ↾}_{V}) \cup ({((U ∖ V) \times \{0_{W}\}) ↾}_{V}) = a \cup \emptyset$
52	41 51	eqtrid	$⊢ ((W \in Mnd \land U \in X \land V \subseteq U) \land a \in C) \to {(a \cup ((U ∖ V) \times \{0_{W}\})) ↾}_{V} = a \cup \emptyset$
53		un0	$⊢ a \cup \emptyset = a$
54	52 53	eqtrdi	$⊢ ((W \in Mnd \land U \in X \land V \subseteq U) \land a \in C) \to {(a \cup ((U ∖ V) \times \{0_{W}\})) ↾}_{V} = a$
55	40 54	eqtr2d	$⊢ ((W \in Mnd \land U \in X \land V \subseteq U) \land a \in C) \to a = F (a \cup ((U ∖ V) \times \{0_{W}\}))$
56		fveq2	$⊢ b = a \cup ((U ∖ V) \times \{0_{W}\}) \to F (b) = F (a \cup ((U ∖ V) \times \{0_{W}\}))$
57	56	rspceeqv	$⊢ (a \cup ((U ∖ V) \times \{0_{W}\}) \in B \land a = F (a \cup ((U ∖ V) \times \{0_{W}\}))) \to \exists b \in B a = F (b)$
58	38 55 57	syl2anc	$⊢ ((W \in Mnd \land U \in X \land V \subseteq U) \land a \in C) \to \exists b \in B a = F (b)$
59	58	ralrimiva	$⊢ (W \in Mnd \land U \in X \land V \subseteq U) \to \forall a \in C \exists b \in B a = F (b)$
60		dffo3	$⊢ F : B \underset{onto}{⟶} C \leftrightarrow (F : B ⟶ C \land \forall a \in C \exists b \in B a = F (b))$
61	6 59 60	sylanbrc	$⊢ (W \in Mnd \land U \in X \land V \subseteq U) \to F : B \underset{onto}{⟶} C$

Metamath Proof Explorer

Theorem pwssplit1

Proof