Metamath Proof Explorer


Theorem symgvalstruct

Description: The value of the symmetric group function at A represented as extensible structure with three slots. This corresponds to the former definition of SymGrp . (Contributed by Paul Chapman, 25-Feb-2008) (Revised by Mario Carneiro, 12-Jan-2015) (Revised by AV, 31-Mar-2024) (Proof shortened by AV, 6-Nov-2024)

Ref Expression
Hypotheses symgvalstruct.g
|- G = ( SymGrp ` A )
symgvalstruct.b
|- B = { x | x : A -1-1-onto-> A }
symgvalstruct.m
|- M = ( A ^m A )
symgvalstruct.p
|- .+ = ( f e. M , g e. M |-> ( f o. g ) )
symgvalstruct.j
|- J = ( Xt_ ` ( A X. { ~P A } ) )
Assertion symgvalstruct
|- ( A e. V -> G = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } )

Proof

Step Hyp Ref Expression
1 symgvalstruct.g
 |-  G = ( SymGrp ` A )
2 symgvalstruct.b
 |-  B = { x | x : A -1-1-onto-> A }
3 symgvalstruct.m
 |-  M = ( A ^m A )
4 symgvalstruct.p
 |-  .+ = ( f e. M , g e. M |-> ( f o. g ) )
5 symgvalstruct.j
 |-  J = ( Xt_ ` ( A X. { ~P A } ) )
6 hashv01gt1
 |-  ( A e. V -> ( ( # ` A ) = 0 \/ ( # ` A ) = 1 \/ 1 < ( # ` A ) ) )
7 hasheq0
 |-  ( A e. V -> ( ( # ` A ) = 0 <-> A = (/) ) )
8 0symgefmndeq
 |-  ( EndoFMnd ` (/) ) = ( SymGrp ` (/) )
9 8 eqcomi
 |-  ( SymGrp ` (/) ) = ( EndoFMnd ` (/) )
10 fveq2
 |-  ( A = (/) -> ( SymGrp ` A ) = ( SymGrp ` (/) ) )
11 1 10 eqtrid
 |-  ( A = (/) -> G = ( SymGrp ` (/) ) )
12 fveq2
 |-  ( A = (/) -> ( EndoFMnd ` A ) = ( EndoFMnd ` (/) ) )
13 9 11 12 3eqtr4a
 |-  ( A = (/) -> G = ( EndoFMnd ` A ) )
14 13 adantl
 |-  ( ( A e. V /\ A = (/) ) -> G = ( EndoFMnd ` A ) )
15 eqid
 |-  ( EndoFMnd ` A ) = ( EndoFMnd ` A )
16 15 3 4 5 efmnd
 |-  ( A e. V -> ( EndoFMnd ` A ) = { <. ( Base ` ndx ) , M >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } )
17 16 adantr
 |-  ( ( A e. V /\ A = (/) ) -> ( EndoFMnd ` A ) = { <. ( Base ` ndx ) , M >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } )
18 0map0sn0
 |-  ( (/) ^m (/) ) = { (/) }
19 id
 |-  ( A = (/) -> A = (/) )
20 19 19 oveq12d
 |-  ( A = (/) -> ( A ^m A ) = ( (/) ^m (/) ) )
21 11 fveq2d
 |-  ( A = (/) -> ( Base ` G ) = ( Base ` ( SymGrp ` (/) ) ) )
22 eqid
 |-  ( Base ` G ) = ( Base ` G )
23 1 22 symgbas
 |-  ( Base ` G ) = { x | x : A -1-1-onto-> A }
24 symgbas0
 |-  ( Base ` ( SymGrp ` (/) ) ) = { (/) }
25 21 23 24 3eqtr3g
 |-  ( A = (/) -> { x | x : A -1-1-onto-> A } = { (/) } )
26 2 25 eqtrid
 |-  ( A = (/) -> B = { (/) } )
27 18 20 26 3eqtr4a
 |-  ( A = (/) -> ( A ^m A ) = B )
28 27 adantl
 |-  ( ( A e. V /\ A = (/) ) -> ( A ^m A ) = B )
29 3 28 eqtrid
 |-  ( ( A e. V /\ A = (/) ) -> M = B )
30 29 opeq2d
 |-  ( ( A e. V /\ A = (/) ) -> <. ( Base ` ndx ) , M >. = <. ( Base ` ndx ) , B >. )
31 30 tpeq1d
 |-  ( ( A e. V /\ A = (/) ) -> { <. ( Base ` ndx ) , M >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } )
32 14 17 31 3eqtrd
 |-  ( ( A e. V /\ A = (/) ) -> G = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } )
33 32 ex
 |-  ( A e. V -> ( A = (/) -> G = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } ) )
34 7 33 sylbid
 |-  ( A e. V -> ( ( # ` A ) = 0 -> G = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } ) )
35 hash1snb
 |-  ( A e. V -> ( ( # ` A ) = 1 <-> E. x A = { x } ) )
36 snex
 |-  { x } e. _V
37 eleq1
 |-  ( A = { x } -> ( A e. _V <-> { x } e. _V ) )
38 36 37 mpbiri
 |-  ( A = { x } -> A e. _V )
39 15 3 4 5 efmnd
 |-  ( A e. _V -> ( EndoFMnd ` A ) = { <. ( Base ` ndx ) , M >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } )
40 38 39 syl
 |-  ( A = { x } -> ( EndoFMnd ` A ) = { <. ( Base ` ndx ) , M >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } )
41 snsymgefmndeq
 |-  ( A = { x } -> ( EndoFMnd ` A ) = ( SymGrp ` A ) )
42 41 1 eqtr4di
 |-  ( A = { x } -> ( EndoFMnd ` A ) = G )
43 42 fveq2d
 |-  ( A = { x } -> ( Base ` ( EndoFMnd ` A ) ) = ( Base ` G ) )
44 eqid
 |-  ( Base ` ( EndoFMnd ` A ) ) = ( Base ` ( EndoFMnd ` A ) )
45 15 44 efmndbas
 |-  ( Base ` ( EndoFMnd ` A ) ) = ( A ^m A )
46 45 3 eqtr4i
 |-  ( Base ` ( EndoFMnd ` A ) ) = M
47 23 2 eqtr4i
 |-  ( Base ` G ) = B
48 43 46 47 3eqtr3g
 |-  ( A = { x } -> M = B )
49 48 opeq2d
 |-  ( A = { x } -> <. ( Base ` ndx ) , M >. = <. ( Base ` ndx ) , B >. )
50 49 tpeq1d
 |-  ( A = { x } -> { <. ( Base ` ndx ) , M >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } )
51 40 42 50 3eqtr3d
 |-  ( A = { x } -> G = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } )
52 51 exlimiv
 |-  ( E. x A = { x } -> G = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } )
53 35 52 syl6bi
 |-  ( A e. V -> ( ( # ` A ) = 1 -> G = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } ) )
54 ssnpss
 |-  ( ( A ^m A ) C_ B -> -. B C. ( A ^m A ) )
55 15 1 symgpssefmnd
 |-  ( ( A e. V /\ 1 < ( # ` A ) ) -> ( Base ` G ) C. ( Base ` ( EndoFMnd ` A ) ) )
56 2 23 eqtr4i
 |-  B = ( Base ` G )
57 45 eqcomi
 |-  ( A ^m A ) = ( Base ` ( EndoFMnd ` A ) )
58 56 57 psseq12i
 |-  ( B C. ( A ^m A ) <-> ( Base ` G ) C. ( Base ` ( EndoFMnd ` A ) ) )
59 55 58 sylibr
 |-  ( ( A e. V /\ 1 < ( # ` A ) ) -> B C. ( A ^m A ) )
60 54 59 nsyl3
 |-  ( ( A e. V /\ 1 < ( # ` A ) ) -> -. ( A ^m A ) C_ B )
61 fvexd
 |-  ( ( A e. V /\ 1 < ( # ` A ) ) -> ( EndoFMnd ` A ) e. _V )
62 f1osetex
 |-  { x | x : A -1-1-onto-> A } e. _V
63 2 62 eqeltri
 |-  B e. _V
64 63 a1i
 |-  ( ( A e. V /\ 1 < ( # ` A ) ) -> B e. _V )
65 1 2 symgval
 |-  G = ( ( EndoFMnd ` A ) |`s B )
66 65 57 ressval2
 |-  ( ( -. ( A ^m A ) C_ B /\ ( EndoFMnd ` A ) e. _V /\ B e. _V ) -> G = ( ( EndoFMnd ` A ) sSet <. ( Base ` ndx ) , ( B i^i ( A ^m A ) ) >. ) )
67 60 61 64 66 syl3anc
 |-  ( ( A e. V /\ 1 < ( # ` A ) ) -> G = ( ( EndoFMnd ` A ) sSet <. ( Base ` ndx ) , ( B i^i ( A ^m A ) ) >. ) )
68 ovex
 |-  ( A ^m A ) e. _V
69 68 inex2
 |-  ( B i^i ( A ^m A ) ) e. _V
70 setsval
 |-  ( ( ( EndoFMnd ` A ) e. _V /\ ( B i^i ( A ^m A ) ) e. _V ) -> ( ( EndoFMnd ` A ) sSet <. ( Base ` ndx ) , ( B i^i ( A ^m A ) ) >. ) = ( ( ( EndoFMnd ` A ) |` ( _V \ { ( Base ` ndx ) } ) ) u. { <. ( Base ` ndx ) , ( B i^i ( A ^m A ) ) >. } ) )
71 61 69 70 sylancl
 |-  ( ( A e. V /\ 1 < ( # ` A ) ) -> ( ( EndoFMnd ` A ) sSet <. ( Base ` ndx ) , ( B i^i ( A ^m A ) ) >. ) = ( ( ( EndoFMnd ` A ) |` ( _V \ { ( Base ` ndx ) } ) ) u. { <. ( Base ` ndx ) , ( B i^i ( A ^m A ) ) >. } ) )
72 16 adantr
 |-  ( ( A e. V /\ 1 < ( # ` A ) ) -> ( EndoFMnd ` A ) = { <. ( Base ` ndx ) , M >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } )
73 72 reseq1d
 |-  ( ( A e. V /\ 1 < ( # ` A ) ) -> ( ( EndoFMnd ` A ) |` ( _V \ { ( Base ` ndx ) } ) ) = ( { <. ( Base ` ndx ) , M >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } |` ( _V \ { ( Base ` ndx ) } ) ) )
74 73 uneq1d
 |-  ( ( A e. V /\ 1 < ( # ` A ) ) -> ( ( ( EndoFMnd ` A ) |` ( _V \ { ( Base ` ndx ) } ) ) u. { <. ( Base ` ndx ) , ( B i^i ( A ^m A ) ) >. } ) = ( ( { <. ( Base ` ndx ) , M >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } |` ( _V \ { ( Base ` ndx ) } ) ) u. { <. ( Base ` ndx ) , ( B i^i ( A ^m A ) ) >. } ) )
75 eqidd
 |-  ( ( A e. V /\ 1 < ( # ` A ) ) -> { <. ( Base ` ndx ) , M >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } = { <. ( Base ` ndx ) , M >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } )
76 fvexd
 |-  ( ( A e. V /\ 1 < ( # ` A ) ) -> ( +g ` ndx ) e. _V )
77 fvexd
 |-  ( ( A e. V /\ 1 < ( # ` A ) ) -> ( TopSet ` ndx ) e. _V )
78 3 68 eqeltri
 |-  M e. _V
79 78 78 mpoex
 |-  ( f e. M , g e. M |-> ( f o. g ) ) e. _V
80 4 79 eqeltri
 |-  .+ e. _V
81 80 a1i
 |-  ( ( A e. V /\ 1 < ( # ` A ) ) -> .+ e. _V )
82 5 fvexi
 |-  J e. _V
83 82 a1i
 |-  ( ( A e. V /\ 1 < ( # ` A ) ) -> J e. _V )
84 basendxnplusgndx
 |-  ( Base ` ndx ) =/= ( +g ` ndx )
85 84 necomi
 |-  ( +g ` ndx ) =/= ( Base ` ndx )
86 85 a1i
 |-  ( ( A e. V /\ 1 < ( # ` A ) ) -> ( +g ` ndx ) =/= ( Base ` ndx ) )
87 tsetndxnbasendx
 |-  ( TopSet ` ndx ) =/= ( Base ` ndx )
88 87 a1i
 |-  ( ( A e. V /\ 1 < ( # ` A ) ) -> ( TopSet ` ndx ) =/= ( Base ` ndx ) )
89 75 76 77 81 83 86 88 tpres
 |-  ( ( A e. V /\ 1 < ( # ` A ) ) -> ( { <. ( Base ` ndx ) , M >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } |` ( _V \ { ( Base ` ndx ) } ) ) = { <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } )
90 89 uneq1d
 |-  ( ( A e. V /\ 1 < ( # ` A ) ) -> ( ( { <. ( Base ` ndx ) , M >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } |` ( _V \ { ( Base ` ndx ) } ) ) u. { <. ( Base ` ndx ) , ( B i^i ( A ^m A ) ) >. } ) = ( { <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } u. { <. ( Base ` ndx ) , ( B i^i ( A ^m A ) ) >. } ) )
91 uncom
 |-  ( { <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } u. { <. ( Base ` ndx ) , ( B i^i ( A ^m A ) ) >. } ) = ( { <. ( Base ` ndx ) , ( B i^i ( A ^m A ) ) >. } u. { <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } )
92 tpass
 |-  { <. ( Base ` ndx ) , ( B i^i ( A ^m A ) ) >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } = ( { <. ( Base ` ndx ) , ( B i^i ( A ^m A ) ) >. } u. { <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } )
93 91 92 eqtr4i
 |-  ( { <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } u. { <. ( Base ` ndx ) , ( B i^i ( A ^m A ) ) >. } ) = { <. ( Base ` ndx ) , ( B i^i ( A ^m A ) ) >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. }
94 1 56 symgbasmap
 |-  ( x e. B -> x e. ( A ^m A ) )
95 94 a1i
 |-  ( ( A e. V /\ 1 < ( # ` A ) ) -> ( x e. B -> x e. ( A ^m A ) ) )
96 95 ssrdv
 |-  ( ( A e. V /\ 1 < ( # ` A ) ) -> B C_ ( A ^m A ) )
97 df-ss
 |-  ( B C_ ( A ^m A ) <-> ( B i^i ( A ^m A ) ) = B )
98 96 97 sylib
 |-  ( ( A e. V /\ 1 < ( # ` A ) ) -> ( B i^i ( A ^m A ) ) = B )
99 98 opeq2d
 |-  ( ( A e. V /\ 1 < ( # ` A ) ) -> <. ( Base ` ndx ) , ( B i^i ( A ^m A ) ) >. = <. ( Base ` ndx ) , B >. )
100 99 tpeq1d
 |-  ( ( A e. V /\ 1 < ( # ` A ) ) -> { <. ( Base ` ndx ) , ( B i^i ( A ^m A ) ) >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } )
101 93 100 eqtrid
 |-  ( ( A e. V /\ 1 < ( # ` A ) ) -> ( { <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } u. { <. ( Base ` ndx ) , ( B i^i ( A ^m A ) ) >. } ) = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } )
102 74 90 101 3eqtrd
 |-  ( ( A e. V /\ 1 < ( # ` A ) ) -> ( ( ( EndoFMnd ` A ) |` ( _V \ { ( Base ` ndx ) } ) ) u. { <. ( Base ` ndx ) , ( B i^i ( A ^m A ) ) >. } ) = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } )
103 67 71 102 3eqtrd
 |-  ( ( A e. V /\ 1 < ( # ` A ) ) -> G = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } )
104 103 ex
 |-  ( A e. V -> ( 1 < ( # ` A ) -> G = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } ) )
105 34 53 104 3jaod
 |-  ( A e. V -> ( ( ( # ` A ) = 0 \/ ( # ` A ) = 1 \/ 1 < ( # ` A ) ) -> G = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } ) )
106 6 105 mpd
 |-  ( A e. V -> G = { <. ( Base ` ndx ) , B >. , <. ( +g ` ndx ) , .+ >. , <. ( TopSet ` ndx ) , J >. } )