Step | Hyp | Ref
| Expression |
1 | | simp1 988 |
. . 3
      |
2 | | linc1.s |
. . . . . . . . . 10
Scalar   |
3 | 2 | lmodrng 17082 |
. . . . . . . . 9

  |
4 | 2 | eqcomi 2467 |
. . . . . . . . . . . 12
Scalar   |
5 | 4 | fveq2i 5805 |
. . . . . . . . . . 11
   Scalar        |
6 | | linc1.1 |
. . . . . . . . . . 11
     |
7 | 5, 6 | rngidcl 16791 |
. . . . . . . . . 10

   Scalar     |
8 | | linc1.0 |
. . . . . . . . . . 11
     |
9 | 5, 8 | rng0cl 16792 |
. . . . . . . . . 10

   Scalar     |
10 | 7, 9 | jca 532 |
. . . . . . . . 9

   Scalar      Scalar      |
11 | 3, 10 | syl 16 |
. . . . . . . 8

   Scalar      Scalar      |
12 | 11 | 3ad2ant1 1009 |
. . . . . . 7
       Scalar      Scalar      |
13 | 12 | adantr 465 |
. . . . . 6
   

    Scalar      Scalar      |
14 | | ifcl 3942 |
. . . . . 6
    Scalar  
   Scalar      
   Scalar     |
15 | 13, 14 | syl 16 |
. . . . 5
   

  
    Scalar     |
16 | | linc1.f |
. . . . 5
      |
17 | 15, 16 | fmptd 5979 |
. . . 4
           Scalar     |
18 | | fvex 5812 |
. . . . 5
   Scalar    |
19 | | simp2 989 |
. . . . 5
       |
20 | | elmapg 7340 |
. . . . 5
     Scalar  
  
    Scalar           Scalar      |
21 | 18, 19, 20 | sylancr 663 |
. . . 4
    
    Scalar           Scalar      |
22 | 17, 21 | mpbird 232 |
. . 3
        Scalar      |
23 | | linc1.b |
. . . . . . 7
     |
24 | 23 | pweqi 3975 |
. . . . . 6
       |
25 | 24 | eleq2i 2532 |
. . . . 5
 
       |
26 | 25 | biimpi 194 |
. . . 4
 
       |
27 | 26 | 3ad2ant2 1010 |
. . 3
           |
28 | | lincval 31095 |
. . 3
      Scalar            linC
     g                  |
29 | 1, 22, 27, 28 | syl3anc 1219 |
. 2
      linC
     g                  |
30 | | eqid 2454 |
. . 3
         |
31 | | lmodgrp 17081 |
. . . . 5

  |
32 | | grpmnd 15672 |
. . . . 5
   |
33 | 31, 32 | syl 16 |
. . . 4

  |
34 | 33 | 3ad2ant1 1009 |
. . 3
      |
35 | | simp3 990 |
. . 3
      |
36 | 1 | adantr 465 |
. . . . 5
   

   |
37 | | simpr 461 |
. . . . . . 7
   

   |
38 | | eqid 2454 |
. . . . . . . . . . 11
         |
39 | 2, 38, 6 | lmod1cl 17101 |
. . . . . . . . . 10

      |
40 | 39 | 3ad2ant1 1009 |
. . . . . . . . 9
          |
41 | 40 | adantr 465 |
. . . . . . . 8
   

       |
42 | 2, 38, 8 | lmod0cl 17100 |
. . . . . . . . . 10

      |
43 | 42 | 3ad2ant1 1009 |
. . . . . . . . 9
          |
44 | 43 | adantr 465 |
. . . . . . . 8
   

       |
45 | 41, 44 | ifcld 3943 |
. . . . . . 7
   

   
      |
46 | | eqeq1 2458 |
. . . . . . . . 9
 
   |
47 | 46 | ifbid 3922 |
. . . . . . . 8
  
      |
48 | 47, 16 | fvmptg 5884 |
. . . . . . 7
    
              |
49 | 37, 45, 48 | syl2anc 661 |
. . . . . 6
   

          |
50 | 49, 45 | eqeltrd 2542 |
. . . . 5
   

           |
51 | | elelpwi 3982 |
. . . . . . . 8
 
 
  |
52 | 51 | expcom 435 |
. . . . . . 7
      |
53 | 52 | 3ad2ant2 1010 |
. . . . . 6
        |
54 | 53 | imp 429 |
. . . . 5
   

   |
55 | | eqid 2454 |
. . . . . 6
         |
56 | 23, 2, 55, 38 | lmodvscl 17091 |
. . . . 5
         
               |
57 | 36, 50, 54, 56 | syl3anc 1219 |
. . . 4
   

               |
58 | | eqid 2454 |
. . . 4
                             |
59 | 57, 58 | fmptd 5979 |
. . 3
                        |
60 | | fveq2 5802 |
. . . . . . 7
           |
61 | | id 22 |
. . . . . . 7
   |
62 | 60, 61 | oveq12d 6221 |
. . . . . 6
                           |
63 | 62 | cbvmptv 4494 |
. . . . 5
                             |
64 | | fvex 5812 |
. . . . . 6
     |
65 | 64 | a1i 11 |
. . . . 5
          |
66 | | ovex 6228 |
. . . . . 6
             |
67 | 66 | a1i 11 |
. . . . 5
   

               |
68 | 63, 19, 65, 67 | mptsuppd 6825 |
. . . 4
                   supp                          |
69 | | ax-1 6 |
. . . . . . . 8
                     |
70 | 69 | a1d 25 |
. . . . . . 7
     
                      |
71 | | simprr 756 |
. . . . . . . . . . . . . 14
   
      |
72 | | fvex 5812 |
. . . . . . . . . . . . . . . 16
     |
73 | 6, 72 | eqeltri 2538 |
. . . . . . . . . . . . . . 15
 |
74 | | fvex 5812 |
. . . . . . . . . . . . . . . 16
     |
75 | 8, 74 | eqeltri 2538 |
. . . . . . . . . . . . . . 15
 |
76 | 73, 75 | ifex 3969 |
. . . . . . . . . . . . . 14
    |
77 | | eqeq1 2458 |
. . . . . . . . . . . . . . . 16
 
   |
78 | 77 | ifbid 3922 |
. . . . . . . . . . . . . . 15
  
      |
79 | 78, 16 | fvmptg 5884 |
. . . . . . . . . . . . . 14
    
          |
80 | 71, 76, 79 | sylancl 662 |
. . . . . . . . . . . . 13
   
             |
81 | | iffalse 3910 |
. . . . . . . . . . . . . 14
   
 |
82 | 81 | adantr 465 |
. . . . . . . . . . . . 13
   
      
 |
83 | 80, 82 | eqtrd 2495 |
. . . . . . . . . . . 12
   
         |
84 | 83 | oveq1d 6218 |
. . . . . . . . . . 11
   
                        |
85 | 1 | adantr 465 |
. . . . . . . . . . . . 13
   

   |
86 | 85 | adantl 466 |
. . . . . . . . . . . 12
   
   
  |
87 | | elelpwi 3982 |
. . . . . . . . . . . . . . . 16
 
 
  |
88 | 87 | expcom 435 |
. . . . . . . . . . . . . . 15
      |
89 | 88 | 3ad2ant2 1010 |
. . . . . . . . . . . . . 14
        |
90 | 89 | imp 429 |
. . . . . . . . . . . . 13
   

   |
91 | 90 | adantl 466 |
. . . . . . . . . . . 12
   
      |
92 | 23, 2, 55, 8, 30 | lmod0vs 17107 |
. . . . . . . . . . . 12
               |
93 | 86, 91, 92 | syl2anc 661 |
. . . . . . . . . . 11
   
                |
94 | 84, 93 | eqtrd 2495 |
. . . . . . . . . 10
   
                      |
95 | 94 | neeq1d 2729 |
. . . . . . . . 9
   
                    
           |
96 | | eqneqall 2661 |
. . . . . . . . . 10
                     |
97 | 30, 96 | ax-mp 5 |
. . . . . . . . 9
           |
98 | 95, 97 | syl6bi 228 |
. . . . . . . 8
   
                        |
99 | 98 | ex 434 |
. . . . . . 7
   
                        |
100 | 70, 99 | pm2.61i 164 |
. . . . . 6
   

                     |
101 | 100 | ralrimiva 2830 |
. . . . 5
    
                    |
102 | | rabsssn 30886 |
. . . . 5
                                          |
103 | 101, 102 | sylibr 212 |
. . . 4
                          |
104 | 68, 103 | eqsstrd 3501 |
. . 3
                   supp          |
105 | 23, 30, 34, 19, 35, 59, 104 | gsumpt 16579 |
. 2
     g                                    |
106 | | ovex 6228 |
. . . 4
             |
107 | | fveq2 5802 |
. . . . . 6
           |
108 | | id 22 |
. . . . . 6
   |
109 | 107, 108 | oveq12d 6221 |
. . . . 5
                           |
110 | 109, 58 | fvmptg 5884 |
. . . 4
                                               |
111 | 35, 106, 110 | sylancl 662 |
. . 3
                                    |
112 | | iftrue 3908 |
. . . . . 6
  
  |
113 | 112, 16 | fvmptg 5884 |
. . . . 5
        |
114 | 35, 73, 113 | sylancl 662 |
. . . 4
         |
115 | 114 | oveq1d 6218 |
. . 3
                        |
116 | | elelpwi 3982 |
. . . . . 6
 
 
  |
117 | 116 | ancoms 453 |
. . . . 5
  

  |
118 | 117 | 3adant1 1006 |
. . . 4
      |
119 | 23, 2, 55, 6 | lmodvs1 17102 |
. . . 4
           |
120 | 1, 118, 119 | syl2anc 661 |
. . 3
            |
121 | 111, 115,
120 | 3eqtrd 2499 |
. 2
                        |
122 | 29, 105, 121 | 3eqtrd 2499 |
1
      linC
      |