Step | Hyp | Ref
| Expression |
1 | | ccatmulgnn0dir.a |
. . . . . . . . 9
  ..^     |
2 | 1 | fveq2i 5873 |
. . . . . . . 8
         ..^      |
3 | | fzofi 12194 |
. . . . . . . . 9
 ..^  |
4 | | snfi 7655 |
. . . . . . . . 9
 
 |
5 | | hashxp 12613 |
. . . . . . . . 9
   ..^  
      ..^          ..^           |
6 | 3, 4, 5 | mp2an 679 |
. . . . . . . 8
     ..^          ..^          |
7 | 2, 6 | eqtri 2475 |
. . . . . . 7
         ..^          |
8 | | ccatmulgnn0dir.m |
. . . . . . . . 9
   |
9 | | hashfzo0 12609 |
. . . . . . . . 9

    ..^    |
10 | 8, 9 | syl 17 |
. . . . . . . 8
     ..^    |
11 | | ccatmulgnn0dir.k |
. . . . . . . . 9
   |
12 | | hashsng 12556 |
. . . . . . . . 9
         |
13 | 11, 12 | syl 17 |
. . . . . . . 8
         |
14 | 10, 13 | oveq12d 6313 |
. . . . . . 7
      ..^             |
15 | 7, 14 | syl5eq 2499 |
. . . . . 6
         |
16 | 8 | nn0cnd 10934 |
. . . . . . 7
   |
17 | 16 | mulid1d 9665 |
. . . . . 6
     |
18 | 15, 17 | eqtrd 2487 |
. . . . 5
       |
19 | | ccatmulgnn0dir.b |
. . . . . . . . 9
  ..^     |
20 | 19 | fveq2i 5873 |
. . . . . . . 8
         ..^      |
21 | | fzofi 12194 |
. . . . . . . . 9
 ..^  |
22 | | hashxp 12613 |
. . . . . . . . 9
   ..^  
      ..^          ..^           |
23 | 21, 4, 22 | mp2an 679 |
. . . . . . . 8
     ..^          ..^          |
24 | 20, 23 | eqtri 2475 |
. . . . . . 7
         ..^          |
25 | | ccatmulgnn0dir.n |
. . . . . . . . 9
   |
26 | | hashfzo0 12609 |
. . . . . . . . 9

    ..^    |
27 | 25, 26 | syl 17 |
. . . . . . . 8
     ..^    |
28 | 27, 13 | oveq12d 6313 |
. . . . . . 7
      ..^             |
29 | 24, 28 | syl5eq 2499 |
. . . . . 6
         |
30 | 25 | nn0cnd 10934 |
. . . . . . 7
   |
31 | 30 | mulid1d 9665 |
. . . . . 6
     |
32 | 29, 31 | eqtrd 2487 |
. . . . 5
       |
33 | 18, 32 | oveq12d 6313 |
. . . 4
               |
34 | 33 | oveq2d 6311 |
. . 3
  ..^            ..^     |
35 | | simpll 761 |
. . . . 5
    ..^             ..^        |
36 | | simpr 463 |
. . . . . 6
    ..^             ..^       ..^       |
37 | 18 | oveq2d 6311 |
. . . . . . 7
  ..^      ..^   |
38 | 35, 37 | syl 17 |
. . . . . 6
    ..^             ..^       ..^      ..^   |
39 | 36, 38 | eleqtrd 2533 |
. . . . 5
    ..^             ..^       ..^   |
40 | | fconstg 5775 |
. . . . . . . 8
   ..^       ..^       |
41 | 11, 40 | syl 17 |
. . . . . . 7
   ..^       ..^       |
42 | 1 | a1i 11 |
. . . . . . . 8
   ..^      |
43 | 42 | feq1d 5719 |
. . . . . . 7
     ..^    
  ..^       ..^        |
44 | 41, 43 | mpbird 236 |
. . . . . 6
    ..^       |
45 | | fvconst 6087 |
. . . . . 6
     ..^      ..^        |
46 | 44, 45 | sylan 474 |
. . . . 5
 
 ..^        |
47 | 35, 39, 46 | syl2anc 667 |
. . . 4
    ..^             ..^            |
48 | | simpll 761 |
. . . . 5
    ..^             ..^        |
49 | | simplr 763 |
. . . . . . 7
    ..^             ..^       ..^             |
50 | | simpr 463 |
. . . . . . 7
    ..^             ..^     
 ..^       |
51 | 18, 8 | eqeltrd 2531 |
. . . . . . . . 9
       |
52 | 48, 51 | syl 17 |
. . . . . . . 8
    ..^             ..^            |
53 | 52 | nn0zd 11045 |
. . . . . . 7
    ..^             ..^            |
54 | 32, 25 | eqeltrd 2531 |
. . . . . . . . 9
       |
55 | 48, 54 | syl 17 |
. . . . . . . 8
    ..^             ..^            |
56 | 55 | nn0zd 11045 |
. . . . . . 7
    ..^             ..^            |
57 | | fzocatel 11985 |
. . . . . . 7
    ..^          
 ..^                        ..^       |
58 | 49, 50, 53, 56, 57 | syl22anc 1270 |
. . . . . 6
    ..^             ..^             ..^       |
59 | 32 | oveq2d 6311 |
. . . . . . 7
  ..^      ..^   |
60 | 48, 59 | syl 17 |
. . . . . 6
    ..^             ..^       ..^      ..^   |
61 | 58, 60 | eleqtrd 2533 |
. . . . 5
    ..^             ..^             ..^   |
62 | | fconstg 5775 |
. . . . . . . 8
   ..^       ..^       |
63 | 11, 62 | syl 17 |
. . . . . . 7
   ..^       ..^       |
64 | 19 | a1i 11 |
. . . . . . . 8
   ..^      |
65 | 64 | feq1d 5719 |
. . . . . . 7
     ..^    
  ..^       ..^        |
66 | 63, 65 | mpbird 236 |
. . . . . 6
    ..^       |
67 | | fvconst 6087 |
. . . . . 6
     ..^            ..^              |
68 | 66, 67 | sylan 474 |
. . . . 5
 
       ..^              |
69 | 48, 61, 68 | syl2anc 667 |
. . . 4
    ..^             ..^                  |
70 | 47, 69 | ifeqda 3916 |
. . 3
 
 ..^               ..^                        |
71 | 34, 70 | mpteq12dva 4483 |
. 2
   ..^              ..^                         ..^      |
72 | | ovex 6323 |
. . . . 5
 ..^  |
73 | | snex 4644 |
. . . . 5
 
 |
74 | 72, 73 | xpex 6600 |
. . . 4
  ..^     |
75 | 1, 74 | eqeltri 2527 |
. . 3
 |
76 | | ovex 6323 |
. . . . 5
 ..^  |
77 | 76, 73 | xpex 6600 |
. . . 4
  ..^     |
78 | 19, 77 | eqeltri 2527 |
. . 3
 |
79 | | ccatfval 12726 |
. . 3
 
  ++    ..^              ..^                         |
80 | 75, 78, 79 | mp2an 679 |
. 2
 ++    ..^              ..^                        |
81 | | ccatmulgnn0dir.c |
. . 3
  ..^       |
82 | | fconstmpt 4881 |
. . 3
  ..^        ..^     |
83 | 81, 82 | eqtri 2475 |
. 2
  ..^     |
84 | 71, 80, 83 | 3eqtr4g 2512 |
1
  ++    |