Proof of Theorem lgsqrlem1
Step | Hyp | Ref
| Expression |
1 | | lgsqr.t |
. . . . 5
        |
2 | 1 | fveq2i 5690 |
. . . 4
             
  |
3 | 2 | fveq1i 5688 |
. . 3
                                |
4 | | lgsqr.o |
. . . . 5
eval1   |
5 | | lgsqr.s |
. . . . 5
Poly1   |
6 | | eqid 2404 |
. . . . 5
         |
7 | | lgsqr.b |
. . . . 5
     |
8 | | lgsqr.1 |
. . . . . . . . 9
       |
9 | 8 | eldifad 3292 |
. . . . . . . 8
   |
10 | | lgsqr.y |
. . . . . . . . 9
ℤ/nℤ   |
11 | 10 | znfld 16796 |
. . . . . . . 8

Field |
12 | 9, 11 | syl 16 |
. . . . . . 7
 Field |
13 | | fldidom 16320 |
. . . . . . 7
 Field IDomn |
14 | 12, 13 | syl 16 |
. . . . . 6
 IDomn |
15 | | isidom 16319 |
. . . . . . 7
 IDomn  Domn  |
16 | 15 | simplbi 447 |
. . . . . 6
 IDomn   |
17 | 14, 16 | syl 16 |
. . . . 5
   |
18 | | crngrng 15629 |
. . . . . . . . 9

  |
19 | 17, 18 | syl 16 |
. . . . . . . 8
   |
20 | | eqid 2404 |
. . . . . . . . 9
ℂfld
↾s  ℂfld ↾s   |
21 | | lgsqr.l |
. . . . . . . . 9
 RHom   |
22 | 20, 21 | zrhrhm 16748 |
. . . . . . . 8

 ℂfld ↾s  RingHom    |
23 | 19, 22 | syl 16 |
. . . . . . 7
  ℂfld ↾s  RingHom    |
24 | | zsubrg 16707 |
. . . . . . . . 9
SubRing ℂfld |
25 | 20 | subrgbas 15832 |
. . . . . . . . 9
 SubRing ℂfld
   ℂfld
↾s     |
26 | 24, 25 | ax-mp 8 |
. . . . . . . 8
   ℂfld
↾s    |
27 | 26, 6 | rhmf 15782 |
. . . . . . 7
  ℂfld
↾s  RingHom            |
28 | 23, 27 | syl 16 |
. . . . . 6
           |
29 | | lgsqrlem1.3 |
. . . . . 6
   |
30 | 28, 29 | ffvelrnd 5830 |
. . . . 5
           |
31 | | lgsqr.x |
. . . . . . . 8
var1   |
32 | 4, 31, 6, 5, 7, 17,
30 | evl1vard 19906 |
. . . . . . 7
                     |
33 | | lgsqr.e |
. . . . . . 7
.g mulGrp    |
34 | | eqid 2404 |
. . . . . . 7
.g mulGrp   .g mulGrp    |
35 | | oddprm 13144 |
. . . . . . . . 9
           |
36 | 8, 35 | syl 16 |
. . . . . . . 8
       |
37 | 36 | nnnn0d 10230 |
. . . . . . 7
       |
38 | 4, 5, 6, 7, 17, 30, 32, 33, 34, 37 | evl1expd 19911 |
. . . . . 6
                                .g mulGrp            |
39 | | cnrng 16678 |
. . . . . . . . . . . . 13
ℂfld  |
40 | | eqid 2404 |
. . . . . . . . . . . . . 14
mulGrp ℂfld mulGrp ℂfld |
41 | 20, 40 | mgpress 15614 |
. . . . . . . . . . . . 13
 ℂfld SubRing ℂfld  mulGrp ℂfld
↾s  mulGrp ℂfld ↾s     |
42 | 39, 24, 41 | mp2an 654 |
. . . . . . . . . . . 12
 mulGrp ℂfld ↾s 
mulGrp ℂfld ↾s    |
43 | | eqid 2404 |
. . . . . . . . . . . 12
mulGrp  mulGrp   |
44 | 42, 43 | rhmmhm 15780 |
. . . . . . . . . . 11
  ℂfld
↾s  RingHom    mulGrp ℂfld
↾s  MndHom mulGrp     |
45 | 23, 44 | syl 16 |
. . . . . . . . . 10
   mulGrp ℂfld
↾s  MndHom mulGrp     |
46 | 42, 26 | mgpbas 15609 |
. . . . . . . . . . 11
    mulGrp ℂfld ↾s    |
47 | | eqid 2404 |
. . . . . . . . . . 11
.g  mulGrp ℂfld
↾s   .g  mulGrp ℂfld ↾s    |
48 | 46, 47, 34 | mhmmulg 14877 |
. . . . . . . . . 10
    mulGrp ℂfld
↾s  MndHom mulGrp      
          .g  mulGrp ℂfld ↾s            .g mulGrp           |
49 | 45, 37, 29, 48 | syl3anc 1184 |
. . . . . . . . 9
          .g  mulGrp ℂfld ↾s            .g mulGrp           |
50 | 40 | subrgsubm 15836 |
. . . . . . . . . . . . . 14
 SubRing ℂfld
SubMnd mulGrp ℂfld   |
51 | 24, 50 | mp1i 12 |
. . . . . . . . . . . . 13
 SubMnd mulGrp ℂfld   |
52 | | eqid 2404 |
. . . . . . . . . . . . . 14
.g mulGrp ℂfld .g mulGrp ℂfld  |
53 | | eqid 2404 |
. . . . . . . . . . . . . 14
 mulGrp ℂfld ↾s 
 mulGrp ℂfld
↾s   |
54 | 52, 53, 47 | submmulg 14880 |
. . . . . . . . . . . . 13
  SubMnd mulGrp ℂfld    
       .g mulGrp ℂfld         .g  mulGrp ℂfld
↾s       |
55 | 51, 37, 29, 54 | syl3anc 1184 |
. . . . . . . . . . . 12
       .g mulGrp ℂfld         .g  mulGrp ℂfld
↾s       |
56 | 29 | zcnd 10332 |
. . . . . . . . . . . . 13
   |
57 | | cnfldexp 16689 |
. . . . . . . . . . . . 13
             .g mulGrp ℂfld             |
58 | 56, 37, 57 | syl2anc 643 |
. . . . . . . . . . . 12
       .g mulGrp ℂfld             |
59 | 55, 58 | eqtr3d 2438 |
. . . . . . . . . . 11
       .g  mulGrp ℂfld
↾s               |
60 | 59 | fveq2d 5691 |
. . . . . . . . . 10
          .g  mulGrp ℂfld ↾s                    |
61 | | lgsqrlem1.4 |
. . . . . . . . . . . 12
               |
62 | | prmnn 13037 |
. . . . . . . . . . . . . 14

  |
63 | 9, 62 | syl 16 |
. . . . . . . . . . . . 13
   |
64 | | zexpcl 11351 |
. . . . . . . . . . . . . 14
                 |
65 | 29, 37, 64 | syl2anc 643 |
. . . . . . . . . . . . 13
           |
66 | | 1z 10267 |
. . . . . . . . . . . . . 14
 |
67 | 66 | a1i 11 |
. . . . . . . . . . . . 13
   |
68 | | moddvds 12814 |
. . . . . . . . . . . . 13
                       
             |
69 | 63, 65, 67, 68 | syl3anc 1184 |
. . . . . . . . . . . 12
             
             |
70 | 61, 69 | mpbid 202 |
. . . . . . . . . . 11
             |
71 | 63 | nnnn0d 10230 |
. . . . . . . . . . . 12
   |
72 | 10, 21 | zndvds 16785 |
. . . . . . . . . . . 12
                           
             |
73 | 71, 65, 67, 72 | syl3anc 1184 |
. . . . . . . . . . 11
                 
             |
74 | 70, 73 | mpbird 224 |
. . . . . . . . . 10
                   |
75 | | cnfld1 16681 |
. . . . . . . . . . . . . 14
  ℂfld |
76 | 20, 75 | subrg1 15833 |
. . . . . . . . . . . . 13
 SubRing ℂfld
   ℂfld ↾s
    |
77 | 24, 76 | ax-mp 8 |
. . . . . . . . . . . 12
   ℂfld ↾s    |
78 | | eqid 2404 |
. . . . . . . . . . . 12
         |
79 | 77, 78 | rhm1 15786 |
. . . . . . . . . . 11
  ℂfld
↾s  RingHom            |
80 | 23, 79 | syl 16 |
. . . . . . . . . 10
           |
81 | 60, 74, 80 | 3eqtrd 2440 |
. . . . . . . . 9
          .g  mulGrp ℂfld ↾s            |
82 | 49, 81 | eqtr3d 2438 |
. . . . . . . 8
       .g mulGrp               |
83 | 82 | eqeq2d 2415 |
. . . . . . 7
                          .g mulGrp                                  |
84 | 83 | anbi2d 685 |
. . . . . 6
                                 .g mulGrp         
     

        
                 |
85 | 38, 84 | mpbid 202 |
. . . . 5
                                 |
86 | | eqid 2404 |
. . . . . . 7
algSc  algSc   |
87 | 6, 78 | rngidcl 15639 |
. . . . . . . 8

          |
88 | 19, 87 | syl 16 |
. . . . . . 7
           |
89 | 4, 5, 6, 86, 7, 17, 88, 30 | evl1scad 19904 |
. . . . . 6
   algSc              algSc                        |
90 | | lgsqr.u |
. . . . . . . . . 10
     |
91 | 5, 86, 78, 90 | ply1scl1 16638 |
. . . . . . . . 9

 algSc          |
92 | 19, 91 | syl 16 |
. . . . . . . 8
  algSc          |
93 | 92 | eleq1d 2470 |
. . . . . . 7
   algSc        
   |
94 | 92 | fveq2d 5691 |
. . . . . . . . 9
     algSc              |
95 | 94 | fveq1d 5689 |
. . . . . . . 8
      algSc                             |
96 | 95 | eqeq1d 2412 |
. . . . . . 7
       algSc                    
                 |
97 | 93, 96 | anbi12d 692 |
. . . . . 6
    algSc              algSc                                        |
98 | 89, 97 | mpbid 202 |
. . . . 5
                  |
99 | | lgsqr.m |
. . . . 5
     |
100 | | eqid 2404 |
. . . . 5
         |
101 | 4, 5, 6, 7, 17, 30, 85, 98, 99, 100 | evl1subd 19908 |
. . . 4
        
                                      |
102 | 101 | simprd 450 |
. . 3
                                      |
103 | 3, 102 | syl5eq 2448 |
. 2
                               |
104 | | rnggrp 15624 |
. . . 4

  |
105 | 19, 104 | syl 16 |
. . 3
   |
106 | | eqid 2404 |
. . . 4
         |
107 | 6, 106, 100 | grpsubid 14828 |
. . 3
                                 |
108 | 105, 88, 107 | syl2anc 643 |
. 2
                       |
109 | 103, 108 | eqtrd 2436 |
1
                   |