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 disjdifr
 |-  ( ( U \ V ) i^i V ) = (/)
46 fnconstg
 |-  ( ( 0g ` W ) e. _V -> ( ( U \ V ) X. { ( 0g ` W ) } ) Fn ( U \ V ) )
47 15 46 ax-mp
 |-  ( ( U \ V ) X. { ( 0g ` W ) } ) Fn ( U \ V )
48 fnresdisj
 |-  ( ( ( U \ V ) X. { ( 0g ` W ) } ) Fn ( U \ V ) -> ( ( ( U \ V ) i^i V ) = (/) <-> ( ( ( U \ V ) X. { ( 0g ` W ) } ) |` V ) = (/) ) )
49 47 48 mp1i
 |-  ( ( ( W e. Mnd /\ U e. X /\ V C_ U ) /\ a e. C ) -> ( ( ( U \ V ) i^i V ) = (/) <-> ( ( ( U \ V ) X. { ( 0g ` W ) } ) |` V ) = (/) ) )
50 45 49 mpbii
 |-  ( ( ( W e. Mnd /\ U e. X /\ V C_ U ) /\ a e. C ) -> ( ( ( U \ V ) X. { ( 0g ` W ) } ) |` V ) = (/) )
51 44 50 uneq12d
 |-  ( ( ( W e. Mnd /\ U e. X /\ V C_ U ) /\ a e. C ) -> ( ( a |` V ) u. ( ( ( U \ V ) X. { ( 0g ` W ) } ) |` V ) ) = ( a u. (/) ) )
52 41 51 syl5eq
 |-  ( ( ( W e. Mnd /\ U e. X /\ V C_ U ) /\ a e. C ) -> ( ( a u. ( ( U \ V ) X. { ( 0g ` W ) } ) ) |` V ) = ( a u. (/) ) )
53 un0
 |-  ( a u. (/) ) = a
54 52 53 eqtrdi
 |-  ( ( ( W e. Mnd /\ U e. X /\ V C_ U ) /\ a e. C ) -> ( ( a u. ( ( U \ V ) X. { ( 0g ` W ) } ) ) |` V ) = a )
55 40 54 eqtr2d
 |-  ( ( ( W e. Mnd /\ U e. X /\ V C_ U ) /\ a e. C ) -> a = ( F ` ( a u. ( ( U \ V ) X. { ( 0g ` W ) } ) ) ) )
56 fveq2
 |-  ( b = ( a u. ( ( U \ V ) X. { ( 0g ` W ) } ) ) -> ( F ` b ) = ( F ` ( a u. ( ( U \ V ) X. { ( 0g ` W ) } ) ) ) )
57 56 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 ) )
58 38 55 57 syl2anc
 |-  ( ( ( W e. Mnd /\ U e. X /\ V C_ U ) /\ a e. C ) -> E. b e. B a = ( F ` b ) )
59 58 ralrimiva
 |-  ( ( W e. Mnd /\ U e. X /\ V C_ U ) -> A. a e. C E. b e. B a = ( F ` b ) )
60 dffo3
 |-  ( F : B -onto-> C <-> ( F : B --> C /\ A. a e. C E. b e. B a = ( F ` b ) ) )
61 6 59 60 sylanbrc
 |-  ( ( W e. Mnd /\ U e. X /\ V C_ U ) -> F : B -onto-> C )