Proof of Theorem gsmsymgrfixlem1
Step | Hyp | Ref
| Expression |
1 | | lencl 13324 |
. . . . . . . 8
Word |
2 | | elnn0uz 11725 |
. . . . . . . 8
|
3 | 1, 2 | sylib 208 |
. . . . . . 7
Word |
4 | 3 | adantr 481 |
. . . . . 6
Word
|
5 | 4 | 3ad2ant1 1082 |
. . . . 5
Word
..^
g
|
6 | | fzosplitsn 12576 |
. . . . 5
..^ ..^ |
7 | 5, 6 | syl 17 |
. . . 4
Word
..^
g
..^ ..^ |
8 | 7 | raleqdv 3144 |
. . 3
Word
..^
g
..^ ++ ..^ ++ |
9 | 1 | adantr 481 |
. . . . 5
Word
|
10 | 9 | 3ad2ant1 1082 |
. . . 4
Word
..^
g
|
11 | | fveq2 6191 |
. . . . . . 7
++ ++ |
12 | 11 | fveq1d 6193 |
. . . . . 6
++ ++ |
13 | 12 | eqeq1d 2624 |
. . . . 5
++
++ |
14 | 13 | ralunsn 4422 |
. . . 4
..^ ++
..^ ++ ++ |
15 | 10, 14 | syl 17 |
. . 3
Word
..^
g
..^ ++
..^ ++ ++ |
16 | 8, 15 | bitrd 268 |
. 2
Word
..^
g
..^ ++ ..^ ++ ++ |
17 | | simpl 473 |
. . . . . . . . 9
Word
Word |
18 | | simpr 477 |
. . . . . . . . 9
Word
|
19 | | eqidd 2623 |
. . . . . . . . 9
Word
|
20 | 17, 18, 19 | 3jca 1242 |
. . . . . . . 8
Word
Word
|
21 | 20 | adantr 481 |
. . . . . . 7
Word
Word
|
22 | | ccats1val2 13404 |
. . . . . . . . 9
Word
++ |
23 | 22 | fveq1d 6193 |
. . . . . . . 8
Word
++ |
24 | 23 | eqeq1d 2624 |
. . . . . . 7
Word
++
|
25 | 21, 24 | syl 17 |
. . . . . 6
Word
++ |
26 | 25 | 3adant3 1081 |
. . . . 5
Word
..^
g
++
|
27 | | simpl 473 |
. . . . . . . . . . . 12
|
28 | 27 | adantl 482 |
. . . . . . . . . . 11
Word
|
29 | 17 | adantr 481 |
. . . . . . . . . . 11
Word
Word |
30 | 18 | adantr 481 |
. . . . . . . . . . 11
Word
|
31 | 28, 29, 30 | 3jca 1242 |
. . . . . . . . . 10
Word
Word
|
32 | 31 | 3adant3 1081 |
. . . . . . . . 9
Word
..^
g
Word |
33 | 32 | adantr 481 |
. . . . . . . 8
Word
..^
g
..^ ++ Word
|
34 | | gsmsymgrfix.s |
. . . . . . . . . 10
|
35 | | gsmsymgrfix.b |
. . . . . . . . . 10
|
36 | 34, 35 | gsumccatsymgsn 17846 |
. . . . . . . . 9
Word g ++ g |
37 | 36 | fveq1d 6193 |
. . . . . . . 8
Word g ++ g |
38 | 33, 37 | syl 17 |
. . . . . . 7
Word
..^
g
..^ ++ g ++ g |
39 | 34, 35 | symgbasf 17804 |
. . . . . . . . . . . . 13
|
40 | | ffn 6045 |
. . . . . . . . . . . . 13
|
41 | 39, 40 | syl 17 |
. . . . . . . . . . . 12
|
42 | 41 | adantl 482 |
. . . . . . . . . . 11
Word
|
43 | | simpr 477 |
. . . . . . . . . . 11
|
44 | 42, 43 | anim12i 590 |
. . . . . . . . . 10
Word
|
45 | 44 | 3adant3 1081 |
. . . . . . . . 9
Word
..^
g
|
46 | 45 | adantr 481 |
. . . . . . . 8
Word
..^
g
..^ ++
|
47 | | fvco2 6273 |
. . . . . . . 8
g g |
48 | 46, 47 | syl 17 |
. . . . . . 7
Word
..^
g
..^ ++ g g |
49 | | fveq2 6191 |
. . . . . . . . . 10
g g |
50 | 49 | adantr 481 |
. . . . . . . . 9
..^ ++ g g |
51 | 50 | adantl 482 |
. . . . . . . 8
Word
..^
g
..^ ++ g g |
52 | 29 | adantr 481 |
. . . . . . . . . . . . . . . . 17
Word
..^
Word |
53 | 30 | adantr 481 |
. . . . . . . . . . . . . . . . 17
Word
..^
|
54 | | simpr 477 |
. . . . . . . . . . . . . . . . 17
Word
..^ ..^ |
55 | | ccats1val1 13403 |
. . . . . . . . . . . . . . . . 17
Word
..^ ++ |
56 | 52, 53, 54, 55 | syl3anc 1326 |
. . . . . . . . . . . . . . . 16
Word
..^ ++ |
57 | 56 | fveq1d 6193 |
. . . . . . . . . . . . . . 15
Word
..^ ++ |
58 | 57 | eqeq1d 2624 |
. . . . . . . . . . . . . 14
Word
..^ ++ |
59 | 58 | ralbidva 2985 |
. . . . . . . . . . . . 13
Word
..^ ++
..^ |
60 | 59 | biimpd 219 |
. . . . . . . . . . . 12
Word
..^ ++
..^ |
61 | 60 | adantld 483 |
. . . . . . . . . . 11
Word
..^ ++ ..^ |
62 | 61 | 3adant3 1081 |
. . . . . . . . . 10
Word
..^
g
..^ ++ ..^ |
63 | | simp3 1063 |
. . . . . . . . . 10
Word
..^
g
..^
g |
64 | 62, 63 | syld 47 |
. . . . . . . . 9
Word
..^
g
..^ ++ g |
65 | 64 | imp 445 |
. . . . . . . 8
Word
..^
g
..^ ++ g |
66 | 51, 65 | eqtrd 2656 |
. . . . . . 7
Word
..^
g
..^ ++ g |
67 | 38, 48, 66 | 3eqtrd 2660 |
. . . . . 6
Word
..^
g
..^ ++ g ++ |
68 | 67 | exp32 631 |
. . . . 5
Word
..^
g
..^ ++
g ++ |
69 | 26, 68 | sylbid 230 |
. . . 4
Word
..^
g
++ ..^ ++ g ++ |
70 | 69 | com23 86 |
. . 3
Word
..^
g
..^ ++
++ g ++ |
71 | 70 | impd 447 |
. 2
Word
..^
g
..^ ++
++ g ++
|
72 | 16, 71 | sylbid 230 |
1
Word
..^
g
..^ ++
g ++ |