Metamath Proof Explorer

Theorem 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 ⊢ 𝑌 = ( 𝑊 ↑s 𝑈 )
pwssplit1.z ⊢ 𝑍 = ( 𝑊 ↑s 𝑉 )
pwssplit1.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
pwssplit1.c ⊢ 𝐶 = ( Base ‘ 𝑍 )
pwssplit1.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ↾ 𝑉 ) )
Assertion pwssplit1 ( ( 𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → 𝐹 : 𝐵 –onto→ 𝐶 )

Proof

Step Hyp Ref Expression
1 pwssplit1.y ⊢ 𝑌 = ( 𝑊 ↑s 𝑈 )
2 pwssplit1.z ⊢ 𝑍 = ( 𝑊 ↑s 𝑉 )
3 pwssplit1.b ⊢ 𝐵 = ( Base ‘ 𝑌 )
4 pwssplit1.c ⊢ 𝐶 = ( Base ‘ 𝑍 )
5 pwssplit1.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ( 𝑥 ↾ 𝑉 ) )
6 1 2 3 4 5 pwssplit0 ⊢ ( ( 𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → 𝐹 : 𝐵 ⟶ 𝐶 )
7 simp1 ⊢ ( ( 𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → 𝑊 ∈ Mnd )
8 simp2 ⊢ ( ( 𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → 𝑈 ∈ 𝑋 )
9 simp3 ⊢ ( ( 𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → 𝑉 ⊆ 𝑈 )
10 8 9 ssexd ⊢ ( ( 𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → 𝑉 ∈ V )
11 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
12 2 11 4 pwselbasb ⊢ ( ( 𝑊 ∈ Mnd ∧ 𝑉 ∈ V ) → ( 𝑎 ∈ 𝐶 ↔ 𝑎 : 𝑉 ⟶ ( Base ‘ 𝑊 ) ) )
13 7 10 12 syl2anc ⊢ ( ( 𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → ( 𝑎 ∈ 𝐶 ↔ 𝑎 : 𝑉 ⟶ ( Base ‘ 𝑊 ) ) )
14 13 biimpa ⊢ ( ( ( 𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑎 ∈ 𝐶 ) → 𝑎 : 𝑉 ⟶ ( Base ‘ 𝑊 ) )
15 fvex ⊢ ( 0g ‘ 𝑊 ) ∈ V
16 15 fconst ⊢ ( ( 𝑈 ∖ 𝑉 ) × { ( 0g ‘ 𝑊 ) } ) : ( 𝑈 ∖ 𝑉 ) ⟶ { ( 0g ‘ 𝑊 ) }
17 16 a1i ⊢ ( ( ( 𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑎 ∈ 𝐶 ) → ( ( 𝑈 ∖ 𝑉 ) × { ( 0g ‘ 𝑊 ) } ) : ( 𝑈 ∖ 𝑉 ) ⟶ { ( 0g ‘ 𝑊 ) } )
18 simpl1 ⊢ ( ( ( 𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑎 ∈ 𝐶 ) → 𝑊 ∈ Mnd )
19 eqid ⊢ ( 0g ‘ 𝑊 ) = ( 0g ‘ 𝑊 )
20 11 19 mndidcl ⊢ ( 𝑊 ∈ Mnd → ( 0g ‘ 𝑊 ) ∈ ( Base ‘ 𝑊 ) )
21 18 20 syl ⊢ ( ( ( 𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑎 ∈ 𝐶 ) → ( 0g ‘ 𝑊 ) ∈ ( Base ‘ 𝑊 ) )
22 21 snssd ⊢ ( ( ( 𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑎 ∈ 𝐶 ) → { ( 0g ‘ 𝑊 ) } ⊆ ( Base ‘ 𝑊 ) )
23 17 22 fssd ⊢ ( ( ( 𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑎 ∈ 𝐶 ) → ( ( 𝑈 ∖ 𝑉 ) × { ( 0g ‘ 𝑊 ) } ) : ( 𝑈 ∖ 𝑉 ) ⟶ ( Base ‘ 𝑊 ) )
24 disjdif ⊢ ( 𝑉 ∩ ( 𝑈 ∖ 𝑉 ) ) = ∅
25 24 a1i ⊢ ( ( ( 𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑎 ∈ 𝐶 ) → ( 𝑉 ∩ ( 𝑈 ∖ 𝑉 ) ) = ∅ )
26 fun ⊢ ( ( ( 𝑎 : 𝑉 ⟶ ( Base ‘ 𝑊 ) ∧ ( ( 𝑈 ∖ 𝑉 ) × { ( 0g ‘ 𝑊 ) } ) : ( 𝑈 ∖ 𝑉 ) ⟶ ( Base ‘ 𝑊 ) ) ∧ ( 𝑉 ∩ ( 𝑈 ∖ 𝑉 ) ) = ∅ ) → ( 𝑎 ∪ ( ( 𝑈 ∖ 𝑉 ) × { ( 0g ‘ 𝑊 ) } ) ) : ( 𝑉 ∪ ( 𝑈 ∖ 𝑉 ) ) ⟶ ( ( Base ‘ 𝑊 ) ∪ ( Base ‘ 𝑊 ) ) )
27 14 23 25 26 syl21anc ⊢ ( ( ( 𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑎 ∈ 𝐶 ) → ( 𝑎 ∪ ( ( 𝑈 ∖ 𝑉 ) × { ( 0g ‘ 𝑊 ) } ) ) : ( 𝑉 ∪ ( 𝑈 ∖ 𝑉 ) ) ⟶ ( ( Base ‘ 𝑊 ) ∪ ( Base ‘ 𝑊 ) ) )
28 simpl3 ⊢ ( ( ( 𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑎 ∈ 𝐶 ) → 𝑉 ⊆ 𝑈 )
29 undif ⊢ ( 𝑉 ⊆ 𝑈 ↔ ( 𝑉 ∪ ( 𝑈 ∖ 𝑉 ) ) = 𝑈 )
30 28 29 sylib ⊢ ( ( ( 𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑎 ∈ 𝐶 ) → ( 𝑉 ∪ ( 𝑈 ∖ 𝑉 ) ) = 𝑈 )
31 unidm ⊢ ( ( Base ‘ 𝑊 ) ∪ ( Base ‘ 𝑊 ) ) = ( Base ‘ 𝑊 )
32 31 a1i ⊢ ( ( ( 𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑎 ∈ 𝐶 ) → ( ( Base ‘ 𝑊 ) ∪ ( Base ‘ 𝑊 ) ) = ( Base ‘ 𝑊 ) )
33 30 32 feq23d ⊢ ( ( ( 𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑎 ∈ 𝐶 ) → ( ( 𝑎 ∪ ( ( 𝑈 ∖ 𝑉 ) × { ( 0g ‘ 𝑊 ) } ) ) : ( 𝑉 ∪ ( 𝑈 ∖ 𝑉 ) ) ⟶ ( ( Base ‘ 𝑊 ) ∪ ( Base ‘ 𝑊 ) ) ↔ ( 𝑎 ∪ ( ( 𝑈 ∖ 𝑉 ) × { ( 0g ‘ 𝑊 ) } ) ) : 𝑈 ⟶ ( Base ‘ 𝑊 ) ) )
34 27 33 mpbid ⊢ ( ( ( 𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑎 ∈ 𝐶 ) → ( 𝑎 ∪ ( ( 𝑈 ∖ 𝑉 ) × { ( 0g ‘ 𝑊 ) } ) ) : 𝑈 ⟶ ( Base ‘ 𝑊 ) )
35 simpl2 ⊢ ( ( ( 𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑎 ∈ 𝐶 ) → 𝑈 ∈ 𝑋 )
36 1 11 3 pwselbasb ⊢ ( ( 𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ) → ( ( 𝑎 ∪ ( ( 𝑈 ∖ 𝑉 ) × { ( 0g ‘ 𝑊 ) } ) ) ∈ 𝐵 ↔ ( 𝑎 ∪ ( ( 𝑈 ∖ 𝑉 ) × { ( 0g ‘ 𝑊 ) } ) ) : 𝑈 ⟶ ( Base ‘ 𝑊 ) ) )
37 18 35 36 syl2anc ⊢ ( ( ( 𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑎 ∈ 𝐶 ) → ( ( 𝑎 ∪ ( ( 𝑈 ∖ 𝑉 ) × { ( 0g ‘ 𝑊 ) } ) ) ∈ 𝐵 ↔ ( 𝑎 ∪ ( ( 𝑈 ∖ 𝑉 ) × { ( 0g ‘ 𝑊 ) } ) ) : 𝑈 ⟶ ( Base ‘ 𝑊 ) ) )
38 34 37 mpbird ⊢ ( ( ( 𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑎 ∈ 𝐶 ) → ( 𝑎 ∪ ( ( 𝑈 ∖ 𝑉 ) × { ( 0g ‘ 𝑊 ) } ) ) ∈ 𝐵 )
39 5 fvtresfn ⊢ ( ( 𝑎 ∪ ( ( 𝑈 ∖ 𝑉 ) × { ( 0g ‘ 𝑊 ) } ) ) ∈ 𝐵 → ( 𝐹 ‘ ( 𝑎 ∪ ( ( 𝑈 ∖ 𝑉 ) × { ( 0g ‘ 𝑊 ) } ) ) ) = ( ( 𝑎 ∪ ( ( 𝑈 ∖ 𝑉 ) × { ( 0g ‘ 𝑊 ) } ) ) ↾ 𝑉 ) )
40 38 39 syl ⊢ ( ( ( 𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑎 ∈ 𝐶 ) → ( 𝐹 ‘ ( 𝑎 ∪ ( ( 𝑈 ∖ 𝑉 ) × { ( 0g ‘ 𝑊 ) } ) ) ) = ( ( 𝑎 ∪ ( ( 𝑈 ∖ 𝑉 ) × { ( 0g ‘ 𝑊 ) } ) ) ↾ 𝑉 ) )
41 resundir ⊢ ( ( 𝑎 ∪ ( ( 𝑈 ∖ 𝑉 ) × { ( 0g ‘ 𝑊 ) } ) ) ↾ 𝑉 ) = ( ( 𝑎 ↾ 𝑉 ) ∪ ( ( ( 𝑈 ∖ 𝑉 ) × { ( 0g ‘ 𝑊 ) } ) ↾ 𝑉 ) )
42 ffn ⊢ ( 𝑎 : 𝑉 ⟶ ( Base ‘ 𝑊 ) → 𝑎 Fn 𝑉 )
43 fnresdm ⊢ ( 𝑎 Fn 𝑉 → ( 𝑎 ↾ 𝑉 ) = 𝑎 )
44 14 42 43 3syl ⊢ ( ( ( 𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑎 ∈ 𝐶 ) → ( 𝑎 ↾ 𝑉 ) = 𝑎 )
45 disjdifr ⊢ ( ( 𝑈 ∖ 𝑉 ) ∩ 𝑉 ) = ∅
46 fnconstg ⊢ ( ( 0g ‘ 𝑊 ) ∈ V → ( ( 𝑈 ∖ 𝑉 ) × { ( 0g ‘ 𝑊 ) } ) Fn ( 𝑈 ∖ 𝑉 ) )
47 15 46 ax-mp ⊢ ( ( 𝑈 ∖ 𝑉 ) × { ( 0g ‘ 𝑊 ) } ) Fn ( 𝑈 ∖ 𝑉 )
48 fnresdisj ⊢ ( ( ( 𝑈 ∖ 𝑉 ) × { ( 0g ‘ 𝑊 ) } ) Fn ( 𝑈 ∖ 𝑉 ) → ( ( ( 𝑈 ∖ 𝑉 ) ∩ 𝑉 ) = ∅ ↔ ( ( ( 𝑈 ∖ 𝑉 ) × { ( 0g ‘ 𝑊 ) } ) ↾ 𝑉 ) = ∅ ) )
49 47 48 mp1i ⊢ ( ( ( 𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑎 ∈ 𝐶 ) → ( ( ( 𝑈 ∖ 𝑉 ) ∩ 𝑉 ) = ∅ ↔ ( ( ( 𝑈 ∖ 𝑉 ) × { ( 0g ‘ 𝑊 ) } ) ↾ 𝑉 ) = ∅ ) )
50 45 49 mpbii ⊢ ( ( ( 𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑎 ∈ 𝐶 ) → ( ( ( 𝑈 ∖ 𝑉 ) × { ( 0g ‘ 𝑊 ) } ) ↾ 𝑉 ) = ∅ )
51 44 50 uneq12d ⊢ ( ( ( 𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑎 ∈ 𝐶 ) → ( ( 𝑎 ↾ 𝑉 ) ∪ ( ( ( 𝑈 ∖ 𝑉 ) × { ( 0g ‘ 𝑊 ) } ) ↾ 𝑉 ) ) = ( 𝑎 ∪ ∅ ) )
52 41 51 eqtrid ⊢ ( ( ( 𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑎 ∈ 𝐶 ) → ( ( 𝑎 ∪ ( ( 𝑈 ∖ 𝑉 ) × { ( 0g ‘ 𝑊 ) } ) ) ↾ 𝑉 ) = ( 𝑎 ∪ ∅ ) )
53 un0 ⊢ ( 𝑎 ∪ ∅ ) = 𝑎
54 52 53 eqtrdi ⊢ ( ( ( 𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑎 ∈ 𝐶 ) → ( ( 𝑎 ∪ ( ( 𝑈 ∖ 𝑉 ) × { ( 0g ‘ 𝑊 ) } ) ) ↾ 𝑉 ) = 𝑎 )
55 40 54 eqtr2d ⊢ ( ( ( 𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑎 ∈ 𝐶 ) → 𝑎 = ( 𝐹 ‘ ( 𝑎 ∪ ( ( 𝑈 ∖ 𝑉 ) × { ( 0g ‘ 𝑊 ) } ) ) ) )
56 fveq2 ⊢ ( 𝑏 = ( 𝑎 ∪ ( ( 𝑈 ∖ 𝑉 ) × { ( 0g ‘ 𝑊 ) } ) ) → ( 𝐹 ‘ 𝑏 ) = ( 𝐹 ‘ ( 𝑎 ∪ ( ( 𝑈 ∖ 𝑉 ) × { ( 0g ‘ 𝑊 ) } ) ) ) )
57 56 rspceeqv ⊢ ( ( ( 𝑎 ∪ ( ( 𝑈 ∖ 𝑉 ) × { ( 0g ‘ 𝑊 ) } ) ) ∈ 𝐵 ∧ 𝑎 = ( 𝐹 ‘ ( 𝑎 ∪ ( ( 𝑈 ∖ 𝑉 ) × { ( 0g ‘ 𝑊 ) } ) ) ) ) → ∃ 𝑏 ∈ 𝐵 𝑎 = ( 𝐹 ‘ 𝑏 ) )
58 38 55 57 syl2anc ⊢ ( ( ( 𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) ∧ 𝑎 ∈ 𝐶 ) → ∃ 𝑏 ∈ 𝐵 𝑎 = ( 𝐹 ‘ 𝑏 ) )
59 58 ralrimiva ⊢ ( ( 𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → ∀ 𝑎 ∈ 𝐶 ∃ 𝑏 ∈ 𝐵 𝑎 = ( 𝐹 ‘ 𝑏 ) )
60 dffo3 ⊢ ( 𝐹 : 𝐵 –onto→ 𝐶 ↔ ( 𝐹 : 𝐵 ⟶ 𝐶 ∧ ∀ 𝑎 ∈ 𝐶 ∃ 𝑏 ∈ 𝐵 𝑎 = ( 𝐹 ‘ 𝑏 ) ) )
61 6 59 60 sylanbrc ⊢ ( ( 𝑊 ∈ Mnd ∧ 𝑈 ∈ 𝑋 ∧ 𝑉 ⊆ 𝑈 ) → 𝐹 : 𝐵 –onto→ 𝐶 )