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 
|- Y = ( W ^s U )
pwssplit1.z 
|- Z = ( W ^s V )
pwssplit1.b 
|- B = ( Base ` Y )
pwssplit1.c 
|- C = ( Base ` Z )
pwssplit1.f 
|- F = ( x e. B |-> ( x |` V ) )
Assertion pwssplit1 
|- ( ( W e. Mnd /\ U e. X /\ V C_ U ) -> F : B -onto-> C )

Proof

Step Hyp Ref Expression
1 pwssplit1.y 
 |-  Y = ( W ^s U )
2 pwssplit1.z 
 |-  Z = ( W ^s V )
3 pwssplit1.b 
 |-  B = ( Base ` Y )
4 pwssplit1.c 
 |-  C = ( Base ` Z )
5 pwssplit1.f 
 |-  F = ( x e. B |-> ( x |` V ) )
6 1 2 3 4 5 pwssplit0 
 |-  ( ( W e. Mnd /\ U e. X /\ V C_ U ) -> F : B --> C )
7 simp1 
 |-  ( ( W e. Mnd /\ U e. X /\ V C_ U ) -> W e. Mnd )
8 simp2 
 |-  ( ( W e. Mnd /\ U e. X /\ V C_ U ) -> U e. X )
9 simp3 
 |-  ( ( W e. Mnd /\ U e. X /\ V C_ U ) -> V C_ U )
10 8 9 ssexd 
 |-  ( ( W e. Mnd /\ U e. X /\ V C_ U ) -> V e. _V )
11 eqid 
 |-  ( Base ` W ) = ( Base ` W )
12 2 11 4 pwselbasb 
 |-  ( ( W e. Mnd /\ V e. _V ) -> ( a e. C <-> a : V --> ( Base ` W ) ) )
13 7 10 12 syl2anc 
 |-  ( ( W e. Mnd /\ U e. X /\ V C_ U ) -> ( a e. C <-> a : V --> ( Base ` W ) ) )
14 13 biimpa 
 |-  ( ( ( W e. Mnd /\ U e. X /\ V C_ U ) /\ a e. C ) -> a : V --> ( Base ` W ) )
15 fvex 
 |-  ( 0g ` W ) e. _V
16 15 fconst 
 |-  ( ( U \ V ) X. { ( 0g ` W ) } ) : ( U \ V ) --> { ( 0g ` W ) }
17 16 a1i 
 |-  ( ( ( W e. Mnd /\ U e. X /\ V C_ U ) /\ a e. C ) -> ( ( U \ V ) X. { ( 0g ` W ) } ) : ( U \ V ) --> { ( 0g ` W ) } )
18 simpl1 
 |-  ( ( ( W e. Mnd /\ U e. X /\ V C_ U ) /\ a e. C ) -> W e. Mnd )
19 eqid 
 |-  ( 0g ` W ) = ( 0g ` W )
20 11 19 mndidcl 
 |-  ( W e. Mnd -> ( 0g ` W ) e. ( Base ` W ) )
21 18 20 syl 
 |-  ( ( ( W e. Mnd /\ U e. X /\ V C_ U ) /\ a e. C ) -> ( 0g ` W ) e. ( Base ` W ) )
22 21 snssd 
 |-  ( ( ( W e. Mnd /\ U e. X /\ V C_ U ) /\ a e. C ) -> { ( 0g ` W ) } C_ ( Base ` W ) )
23 17 22 fssd 
 |-  ( ( ( W e. Mnd /\ U e. X /\ V C_ U ) /\ a e. C ) -> ( ( U \ V ) X. { ( 0g ` W ) } ) : ( U \ V ) --> ( Base ` W ) )
24 disjdif 
 |-  ( V i^i ( U \ V ) ) = (/)
25 24 a1i 
 |-  ( ( ( W e. Mnd /\ U e. X /\ V C_ U ) /\ a e. C ) -> ( V i^i ( U \ V ) ) = (/) )
26 fun 
 |-  ( ( ( a : V --> ( Base ` W ) /\ ( ( U \ V ) X. { ( 0g ` W ) } ) : ( U \ V ) --> ( Base ` W ) ) /\ ( V i^i ( U \ V ) ) = (/) ) -> ( a u. ( ( U \ V ) X. { ( 0g ` W ) } ) ) : ( V u. ( U \ V ) ) --> ( ( Base ` W ) u. ( Base ` W ) ) )
27 14 23 25 26 syl21anc 
 |-  ( ( ( W e. Mnd /\ U e. X /\ V C_ U ) /\ a e. C ) -> ( a u. ( ( U \ V ) X. { ( 0g ` W ) } ) ) : ( V u. ( U \ V ) ) --> ( ( Base ` W ) u. ( Base ` W ) ) )
28 simpl3 
 |-  ( ( ( W e. Mnd /\ U e. X /\ V C_ U ) /\ a e. C ) -> V C_ U )
29 undif 
 |-  ( V C_ U <-> ( V u. ( U \ V ) ) = U )
30 28 29 sylib 
 |-  ( ( ( W e. Mnd /\ U e. X /\ V C_ U ) /\ a e. C ) -> ( V u. ( U \ V ) ) = U )
31 unidm 
 |-  ( ( Base ` W ) u. ( Base ` W ) ) = ( Base ` W )
32 31 a1i 
 |-  ( ( ( W e. Mnd /\ U e. X /\ V C_ U ) /\ a e. C ) -> ( ( Base ` W ) u. ( Base ` W ) ) = ( Base ` W ) )
33 30 32 feq23d 
 |-  ( ( ( W e. Mnd /\ U e. X /\ V C_ U ) /\ a e. C ) -> ( ( a u. ( ( U \ V ) X. { ( 0g ` W ) } ) ) : ( V u. ( U \ V ) ) --> ( ( Base ` W ) u. ( Base ` W ) ) <-> ( a u. ( ( U \ V ) X. { ( 0g ` W ) } ) ) : U --> ( Base ` W ) ) )
34 27 33 mpbid 
 |-  ( ( ( W e. Mnd /\ U e. X /\ V C_ U ) /\ a e. C ) -> ( a u. ( ( U \ V ) X. { ( 0g ` W ) } ) ) : U --> ( Base ` W ) )
35 simpl2 
 |-  ( ( ( W e. Mnd /\ U e. X /\ V C_ U ) /\ a e. C ) -> U e. X )
36 1 11 3 pwselbasb 
 |-  ( ( W e. Mnd /\ U e. X ) -> ( ( a u. ( ( U \ V ) X. { ( 0g ` W ) } ) ) e. B <-> ( a u. ( ( U \ V ) X. { ( 0g ` W ) } ) ) : U --> ( Base ` W ) ) )
37 18 35 36 syl2anc 
 |-  ( ( ( W e. Mnd /\ U e. X /\ V C_ U ) /\ a e. C ) -> ( ( a u. ( ( U \ V ) X. { ( 0g ` W ) } ) ) e. B <-> ( a u. ( ( U \ V ) X. { ( 0g ` W ) } ) ) : U --> ( Base ` W ) ) )
38 34 37 mpbird 
 |-  ( ( ( W e. Mnd /\ U e. X /\ V C_ U ) /\ a e. C ) -> ( a u. ( ( U \ V ) X. { ( 0g ` W ) } ) ) e. B )
39 5 fvtresfn 
 |-  ( ( a u. ( ( U \ V ) X. { ( 0g ` W ) } ) ) e. B -> ( F ` ( a u. ( ( U \ V ) X. { ( 0g ` W ) } ) ) ) = ( ( a u. ( ( U \ V ) X. { ( 0g ` W ) } ) ) |` V ) )
40 38 39 syl 
 |-  ( ( ( W e. Mnd /\ U e. X /\ V C_ U ) /\ a e. C ) -> ( F ` ( a u. ( ( U \ V ) X. { ( 0g ` W ) } ) ) ) = ( ( a u. ( ( U \ V ) X. { ( 0g ` W ) } ) ) |` V ) )
41 resundir 
 |-  ( ( a u. ( ( U \ V ) X. { ( 0g ` W ) } ) ) |` V ) = ( ( a |` V ) u. ( ( ( U \ V ) X. { ( 0g ` W ) } ) |` V ) )
42 ffn 
 |-  ( a : V --> ( Base ` W ) -> a Fn V )
43 fnresdm 
 |-  ( a Fn V -> ( a |` V ) = a )
44 14 42 43 3syl 
 |-  ( ( ( W e. Mnd /\ U e. X /\ V C_ U ) /\ a e. C ) -> ( a |` V ) = a )
45 incom 
 |-  ( ( U \ V ) i^i V ) = ( V i^i ( U \ V ) )
46 45 24 eqtri 
 |-  ( ( U \ V ) i^i V ) = (/)
47 fnconstg 
 |-  ( ( 0g ` W ) e. _V -> ( ( U \ V ) X. { ( 0g ` W ) } ) Fn ( U \ V ) )
48 15 47 ax-mp 
 |-  ( ( U \ V ) X. { ( 0g ` W ) } ) Fn ( U \ V )
49 fnresdisj 
 |-  ( ( ( U \ V ) X. { ( 0g ` W ) } ) Fn ( U \ V ) -> ( ( ( U \ V ) i^i V ) = (/) <-> ( ( ( U \ V ) X. { ( 0g ` W ) } ) |` V ) = (/) ) )
50 48 49 mp1i 
 |-  ( ( ( W e. Mnd /\ U e. X /\ V C_ U ) /\ a e. C ) -> ( ( ( U \ V ) i^i V ) = (/) <-> ( ( ( U \ V ) X. { ( 0g ` W ) } ) |` V ) = (/) ) )
51 46 50 mpbii 
 |-  ( ( ( W e. Mnd /\ U e. X /\ V C_ U ) /\ a e. C ) -> ( ( ( U \ V ) X. { ( 0g ` W ) } ) |` V ) = (/) )
52 44 51 uneq12d 
 |-  ( ( ( W e. Mnd /\ U e. X /\ V C_ U ) /\ a e. C ) -> ( ( a |` V ) u. ( ( ( U \ V ) X. { ( 0g ` W ) } ) |` V ) ) = ( a u. (/) ) )
53 41 52 syl5eq 
 |-  ( ( ( W e. Mnd /\ U e. X /\ V C_ U ) /\ a e. C ) -> ( ( a u. ( ( U \ V ) X. { ( 0g ` W ) } ) ) |` V ) = ( a u. (/) ) )
54 un0 
 |-  ( a u. (/) ) = a
55 53 54 eqtrdi 
 |-  ( ( ( W e. Mnd /\ U e. X /\ V C_ U ) /\ a e. C ) -> ( ( a u. ( ( U \ V ) X. { ( 0g ` W ) } ) ) |` V ) = a )
56 40 55 eqtr2d 
 |-  ( ( ( W e. Mnd /\ U e. X /\ V C_ U ) /\ a e. C ) -> a = ( F ` ( a u. ( ( U \ V ) X. { ( 0g ` W ) } ) ) ) )
57 fveq2 
 |-  ( b = ( a u. ( ( U \ V ) X. { ( 0g ` W ) } ) ) -> ( F ` b ) = ( F ` ( a u. ( ( U \ V ) X. { ( 0g ` W ) } ) ) ) )
58 57 rspceeqv 
 |-  ( ( ( a u. ( ( U \ V ) X. { ( 0g ` W ) } ) ) e. B /\ a = ( F ` ( a u. ( ( U \ V ) X. { ( 0g ` W ) } ) ) ) ) -> E. b e. B a = ( F ` b ) )
59 38 56 58 syl2anc 
 |-  ( ( ( W e. Mnd /\ U e. X /\ V C_ U ) /\ a e. C ) -> E. b e. B a = ( F ` b ) )
60 59 ralrimiva 
 |-  ( ( W e. Mnd /\ U e. X /\ V C_ U ) -> A. a e. C E. b e. B a = ( F ` b ) )
61 dffo3 
 |-  ( F : B -onto-> C <-> ( F : B --> C /\ A. a e. C E. b e. B a = ( F ` b ) ) )
62 6 60 61 sylanbrc 
 |-  ( ( W e. Mnd /\ U e. X /\ V C_ U ) -> F : B -onto-> C )