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