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 vsnex 
 |-  { 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 biimtrdi 
 |-  ( 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 dfss2 
 |-  ( 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 >. } )