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 >. } ) |