Step | Hyp | Ref
| Expression |
1 | | mpteq1 4499 |
. . . . 5

    ![]_ ]_](_urbrack.gif)               ![]_ ]_](_urbrack.gif)
            |
2 | 1 | oveq2d 6336 |
. . . 4

 g     ![]_ ]_](_urbrack.gif)             g     ![]_ ]_](_urbrack.gif)
             |
3 | | eleq2 2529 |
. . . . . . . 8


   |
4 | 3 | ifbid 3915 |
. . . . . . 7

     ![]_ ]_](_urbrack.gif)            ![]_ ]_](_urbrack.gif)         |
5 | 4 | ifeq1d 3911 |
. . . . . 6

        ![]_ ]_](_urbrack.gif)                     ![]_ ]_](_urbrack.gif)               |
6 | 5 | mpt2eq3dv 6389 |
. . . . 5

          ![]_ ]_](_urbrack.gif)                        ![]_ ]_](_urbrack.gif)                |
7 | 6 | fveq2d 5896 |
. . . 4

             ![]_ ]_](_urbrack.gif)                            ![]_ ]_](_urbrack.gif)                 |
8 | 2, 7 | eqeq12d 2477 |
. . 3

  g     ![]_ ]_](_urbrack.gif)                         ![]_ ]_](_urbrack.gif)                g     ![]_ ]_](_urbrack.gif)
                        ![]_ ]_](_urbrack.gif)                  |
9 | | mpteq1 4499 |
. . . . 5
     ![]_ ]_](_urbrack.gif)
              ![]_ ]_](_urbrack.gif)             |
10 | 9 | oveq2d 6336 |
. . . 4
  g     ![]_ ]_](_urbrack.gif)             g     ![]_ ]_](_urbrack.gif)              |
11 | | eleq2 2529 |
. . . . . . . 8
 
   |
12 | 11 | ifbid 3915 |
. . . . . . 7
      ![]_ ]_](_urbrack.gif)            ![]_ ]_](_urbrack.gif)         |
13 | 12 | ifeq1d 3911 |
. . . . . 6
         ![]_ ]_](_urbrack.gif)                     ![]_ ]_](_urbrack.gif)               |
14 | 13 | mpt2eq3dv 6389 |
. . . . 5
           ![]_ ]_](_urbrack.gif)               
        ![]_ ]_](_urbrack.gif)                |
15 | 14 | fveq2d 5896 |
. . . 4
              ![]_ ]_](_urbrack.gif)                            ![]_ ]_](_urbrack.gif)                 |
16 | 10, 15 | eqeq12d 2477 |
. . 3
   g     ![]_ ]_](_urbrack.gif)                         ![]_ ]_](_urbrack.gif)                g     ![]_ ]_](_urbrack.gif)                         ![]_ ]_](_urbrack.gif)                  |
17 | | mpteq1 4499 |
. . . . 5
         ![]_ ]_](_urbrack.gif)                   ![]_ ]_](_urbrack.gif)             |
18 | 17 | oveq2d 6336 |
. . . 4
      g     ![]_ ]_](_urbrack.gif)             g         ![]_ ]_](_urbrack.gif)              |
19 | | eleq2 2529 |
. . . . . . . 8
             |
20 | 19 | ifbid 3915 |
. . . . . . 7
          ![]_ ]_](_urbrack.gif)                ![]_ ]_](_urbrack.gif)         |
21 | 20 | ifeq1d 3911 |
. . . . . 6
             ![]_ ]_](_urbrack.gif)                         ![]_ ]_](_urbrack.gif)               |
22 | 21 | mpt2eq3dv 6389 |
. . . . 5
               ![]_ ]_](_urbrack.gif)                            ![]_ ]_](_urbrack.gif)                |
23 | 22 | fveq2d 5896 |
. . . 4
         
        ![]_ ]_](_urbrack.gif)                                ![]_ ]_](_urbrack.gif)                 |
24 | 18, 23 | eqeq12d 2477 |
. . 3
       g     ![]_ ]_](_urbrack.gif)                         ![]_ ]_](_urbrack.gif)                g         ![]_ ]_](_urbrack.gif)                
            ![]_ ]_](_urbrack.gif)                  |
25 | | mpteq1 4499 |
. . . . 5
     ![]_ ]_](_urbrack.gif)
              ![]_ ]_](_urbrack.gif)             |
26 | 25 | oveq2d 6336 |
. . . 4
  g     ![]_ ]_](_urbrack.gif)             g     ![]_ ]_](_urbrack.gif)              |
27 | | eleq2 2529 |
. . . . . . . 8
 
   |
28 | 27 | ifbid 3915 |
. . . . . . 7
      ![]_ ]_](_urbrack.gif)          
 ![]_ ]_](_urbrack.gif)         |
29 | 28 | ifeq1d 3911 |
. . . . . 6
         ![]_ ]_](_urbrack.gif)                     ![]_ ]_](_urbrack.gif)               |
30 | 29 | mpt2eq3dv 6389 |
. . . . 5
           ![]_ ]_](_urbrack.gif)               
      
 ![]_ ]_](_urbrack.gif)                |
31 | 30 | fveq2d 5896 |
. . . 4
              ![]_ ]_](_urbrack.gif)                            ![]_ ]_](_urbrack.gif)                 |
32 | 26, 31 | eqeq12d 2477 |
. . 3
   g     ![]_ ]_](_urbrack.gif)                         ![]_ ]_](_urbrack.gif)                g     ![]_ ]_](_urbrack.gif)                         ![]_ ]_](_urbrack.gif)                  |
33 | | noel 3747 |
. . . . . . . . 9
 |
34 | | iffalse 3902 |
. . . . . . . . 9
      ![]_ ]_](_urbrack.gif)             |
35 | 33, 34 | mp1i 13 |
. . . . . . . 8
 
      ![]_ ]_](_urbrack.gif)             |
36 | 35 | ifeq1d 3911 |
. . . . . . 7
 
         ![]_ ]_](_urbrack.gif)                            |
37 | 36 | mpt2eq3ia 6388 |
. . . . . 6
          ![]_ ]_](_urbrack.gif)                               |
38 | 37 | fveq2i 5895 |
. . . . 5
             ![]_ ]_](_urbrack.gif)                                    |
39 | | madugsum.d |
. . . . . 6
 maDet   |
40 | | madugsum.k |
. . . . . 6
     |
41 | | eqid 2462 |
. . . . . 6
         |
42 | | madugsum.r |
. . . . . 6
   |
43 | | madugsum.m |
. . . . . . . 8
   |
44 | | maduf.a |
. . . . . . . . 9
 Mat   |
45 | | maduf.b |
. . . . . . . . 9
     |
46 | 44, 45 | matrcl 19492 |
. . . . . . . 8
 
   |
47 | 43, 46 | syl 17 |
. . . . . . 7
     |
48 | 47 | simpld 465 |
. . . . . 6
   |
49 | 44, 40, 45 | matbas2i 19502 |
. . . . . . . . 9
       |
50 | | elmapi 7524 |
. . . . . . . . 9
  
          |
51 | 43, 49, 50 | 3syl 18 |
. . . . . . . 8
         |
52 | 51 | fovrnda 6472 |
. . . . . . 7
 

        |
53 | 52 | 3impb 1211 |
. . . . . 6
 

      |
54 | | madugsum.l |
. . . . . 6
   |
55 | 39, 40, 41, 42, 48, 53, 54 | mdetr0 19685 |
. . . . 5
                           |
56 | 38, 55 | syl5eq 2508 |
. . . 4
              ![]_ ]_](_urbrack.gif)                     |
57 | | mpt0 5731 |
. . . . . 6
    ![]_ ]_](_urbrack.gif)            |
58 | 57 | oveq2i 6331 |
. . . . 5
 g     ![]_ ]_](_urbrack.gif)
            g   |
59 | 41 | gsum0 16576 |
. . . . 5
 g       |
60 | 58, 59 | eqtri 2484 |
. . . 4
 g     ![]_ ]_](_urbrack.gif)
                |
61 | 56, 60 | syl6reqr 2515 |
. . 3
  g     ![]_ ]_](_urbrack.gif)
                        ![]_ ]_](_urbrack.gif)                 |
62 | | eqid 2462 |
. . . . . . 7
       |
63 | 42 | adantr 471 |
. . . . . . . . 9
 
    
  |
64 | | crngring 17846 |
. . . . . . . . 9

  |
65 | 63, 64 | syl 17 |
. . . . . . . 8
 
    
  |
66 | | ringcmn 17866 |
. . . . . . . 8

CMnd |
67 | 65, 66 | syl 17 |
. . . . . . 7
 
    
CMnd |
68 | 48 | adantr 471 |
. . . . . . . 8
 
    
  |
69 | | simprl 769 |
. . . . . . . 8
 
    
  |
70 | | ssfi 7823 |
. . . . . . . 8
     |
71 | 68, 69, 70 | syl2anc 671 |
. . . . . . 7
 
       |
72 | 65 | adantr 471 |
. . . . . . . 8
   
    
  |
73 | 69 | sselda 3444 |
. . . . . . . . 9
   
    
  |
74 | | madugsum.x |
. . . . . . . . . . 11
 
   |
75 | 74 | ralrimiva 2814 |
. . . . . . . . . 10
 
  |
76 | 75 | ad2antrr 737 |
. . . . . . . . 9
   
    

  |
77 | | rspcsbela 3807 |
. . . . . . . . 9
      ![]_ ]_](_urbrack.gif)   |
78 | 73, 76, 77 | syl2anc 671 |
. . . . . . . 8
   
    
  ![]_ ]_](_urbrack.gif)   |
79 | | maduf.j |
. . . . . . . . . . . . . 14
 maAdju   |
80 | 44, 79, 45 | maduf 19721 |
. . . . . . . . . . . . 13

      |
81 | 42, 80 | syl 17 |
. . . . . . . . . . . 12
       |
82 | 81, 43 | ffvelrnd 6051 |
. . . . . . . . . . 11
       |
83 | 44, 40, 45 | matbas2i 19502 |
. . . . . . . . . . 11
               |
84 | | elmapi 7524 |
. . . . . . . . . . 11
      
              |
85 | 82, 83, 84 | 3syl 18 |
. . . . . . . . . 10
             |
86 | 85 | ad2antrr 737 |
. . . . . . . . 9
   
    
            |
87 | 54 | ad2antrr 737 |
. . . . . . . . 9
   
    
  |
88 | 86, 73, 87 | fovrnd 6473 |
. . . . . . . 8
   
    
          |
89 | | madugsum.t |
. . . . . . . . 9
     |
90 | 40, 89 | ringcl 17849 |
. . . . . . . 8
    ![]_ ]_](_urbrack.gif)
            ![]_ ]_](_urbrack.gif)
           |
91 | 72, 78, 88, 90 | syl3anc 1276 |
. . . . . . 7
   
    
   ![]_ ]_](_urbrack.gif)            |
92 | | vex 3060 |
. . . . . . . 8
 |
93 | 92 | a1i 11 |
. . . . . . 7
 
       |
94 | | eldifn 3568 |
. . . . . . . 8
  
  |
95 | 94 | ad2antll 740 |
. . . . . . 7
 
    
  |
96 | | eldifi 3567 |
. . . . . . . . . 10
     |
97 | 96 | ad2antll 740 |
. . . . . . . . 9
 
       |
98 | 75 | adantr 471 |
. . . . . . . . 9
 
     
  |
99 | | rspcsbela 3807 |
. . . . . . . . 9
      ![]_ ]_](_urbrack.gif)   |
100 | 97, 98, 99 | syl2anc 671 |
. . . . . . . 8
 
     
 ![]_ ]_](_urbrack.gif)
  |
101 | 85 | adantr 471 |
. . . . . . . . 9
 
                 |
102 | 54 | adantr 471 |
. . . . . . . . 9
 
    
  |
103 | 101, 97, 102 | fovrnd 6473 |
. . . . . . . 8
 
               |
104 | 40, 89 | ringcl 17849 |
. . . . . . . 8
    ![]_ ]_](_urbrack.gif)
            ![]_ ]_](_urbrack.gif)
           |
105 | 65, 100, 103, 104 | syl3anc 1276 |
. . . . . . 7
 
        ![]_ ]_](_urbrack.gif)
           |
106 | | csbeq1 3378 |
. . . . . . . 8
   ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
107 | | oveq1 6327 |
. . . . . . . 8
                   |
108 | 106, 107 | oveq12d 6338 |
. . . . . . 7
  
 ![]_ ]_](_urbrack.gif)
            ![]_ ]_](_urbrack.gif)            |
109 | 40, 62, 67, 71, 91, 93, 95, 105, 108 | gsumunsn 17647 |
. . . . . 6
 
      g         ![]_ ]_](_urbrack.gif)              g     ![]_ ]_](_urbrack.gif)                    ![]_ ]_](_urbrack.gif)             |
110 | 109 | adantr 471 |
. . . . 5
   
     g     ![]_ ]_](_urbrack.gif)                
        ![]_ ]_](_urbrack.gif)                 g         ![]_ ]_](_urbrack.gif)              g     ![]_ ]_](_urbrack.gif)                    ![]_ ]_](_urbrack.gif)             |
111 | | oveq1 6327 |
. . . . . 6
  g     ![]_ ]_](_urbrack.gif)                         ![]_ ]_](_urbrack.gif)                 g     ![]_ ]_](_urbrack.gif)                    ![]_ ]_](_urbrack.gif)                         ![]_ ]_](_urbrack.gif)                       ![]_ ]_](_urbrack.gif)             |
112 | 111 | adantl 472 |
. . . . 5
   
     g     ![]_ ]_](_urbrack.gif)                
        ![]_ ]_](_urbrack.gif)                  g     ![]_ ]_](_urbrack.gif)                    ![]_ ]_](_urbrack.gif)                         ![]_ ]_](_urbrack.gif)                       ![]_ ]_](_urbrack.gif)             |
113 | | elun 3586 |
. . . . . . . . . . . . . 14
           |
114 | | elsn 3994 |
. . . . . . . . . . . . . . 15
     |
115 | 114 | orbi2i 526 |
. . . . . . . . . . . . . 14
    

   |
116 | 113, 115 | bitri 257 |
. . . . . . . . . . . . 13
         |
117 | | ifbi 3914 |
. . . . . . . . . . . . 13
                  ![]_ ]_](_urbrack.gif)              ![]_ ]_](_urbrack.gif)         |
118 | 116, 117 | ax-mp 5 |
. . . . . . . . . . . 12
         ![]_ ]_](_urbrack.gif)              ![]_ ]_](_urbrack.gif)        |
119 | | ringmnd 17844 |
. . . . . . . . . . . . . . 15

  |
120 | 65, 119 | syl 17 |
. . . . . . . . . . . . . 14
 
    
  |
121 | 120 | 3ad2ant1 1035 |
. . . . . . . . . . . . 13
   
   

  |
122 | | simp3 1016 |
. . . . . . . . . . . . . 14
   
   

  |
123 | 98 | 3ad2ant1 1035 |
. . . . . . . . . . . . . 14
   
   


  |
124 | 122, 123,
77 | syl2anc 671 |
. . . . . . . . . . . . 13
   
   

  ![]_ ]_](_urbrack.gif)   |
125 | | elequ1 1905 |
. . . . . . . . . . . . . . . 16
 
   |
126 | 125 | biimpac 493 |
. . . . . . . . . . . . . . 15
 
   |
127 | 95, 126 | nsyl 126 |
. . . . . . . . . . . . . 14
 
         |
128 | 127 | 3ad2ant1 1035 |
. . . . . . . . . . . . 13
   
   


   |
129 | 40, 41, 62 | mndifsplit 19716 |
. . . . . . . . . . . . 13
    ![]_ ]_](_urbrack.gif)
          ![]_ ]_](_urbrack.gif)             ![]_ ]_](_urbrack.gif)                 ![]_ ]_](_urbrack.gif)          |
130 | 121, 124,
128, 129 | syl3anc 1276 |
. . . . . . . . . . . 12
   
   

       ![]_ ]_](_urbrack.gif)             ![]_ ]_](_urbrack.gif)                 ![]_ ]_](_urbrack.gif)          |
131 | 118, 130 | syl5eq 2508 |
. . . . . . . . . . 11
   
   

         ![]_ ]_](_urbrack.gif)             ![]_ ]_](_urbrack.gif)                 ![]_ ]_](_urbrack.gif)          |
132 | 106 | adantl 472 |
. . . . . . . . . . . . . . 15
   
    
  ![]_ ]_](_urbrack.gif)   ![]_ ]_](_urbrack.gif)   |
133 | 132 | ifeq1da 3923 |
. . . . . . . . . . . . . 14
 
          ![]_ ]_](_urbrack.gif)            ![]_ ]_](_urbrack.gif)         |
134 | | ovif2 6406 |
. . . . . . . . . . . . . . 15
   ![]_ ]_](_urbrack.gif)                     ![]_ ]_](_urbrack.gif)          ![]_ ]_](_urbrack.gif)
       |
135 | | eqid 2462 |
. . . . . . . . . . . . . . . . . 18
         |
136 | 40, 89, 135 | ringridm 17860 |
. . . . . . . . . . . . . . . . 17
    ![]_ ]_](_urbrack.gif)   
 ![]_ ]_](_urbrack.gif)
       ![]_ ]_](_urbrack.gif)   |
137 | 65, 100, 136 | syl2anc 671 |
. . . . . . . . . . . . . . . 16
 
        ![]_ ]_](_urbrack.gif)
       ![]_ ]_](_urbrack.gif)   |
138 | 40, 89, 41 | ringrz 17873 |
. . . . . . . . . . . . . . . . 17
    ![]_ ]_](_urbrack.gif)   
 ![]_ ]_](_urbrack.gif)
           |
139 | 65, 100, 138 | syl2anc 671 |
. . . . . . . . . . . . . . . 16
 
        ![]_ ]_](_urbrack.gif)
           |
140 | 137, 139 | ifeq12d 3913 |
. . . . . . . . . . . . . . 15
 
           ![]_ ]_](_urbrack.gif)          ![]_ ]_](_urbrack.gif)
           ![]_ ]_](_urbrack.gif)         |
141 | 134, 140 | syl5eq 2508 |
. . . . . . . . . . . . . 14
 
        ![]_ ]_](_urbrack.gif)
                   ![]_ ]_](_urbrack.gif)         |
142 | 133, 141 | eqtr4d 2499 |
. . . . . . . . . . . . 13
 
          ![]_ ]_](_urbrack.gif)          ![]_ ]_](_urbrack.gif)                 |
143 | 142 | oveq2d 6336 |
. . . . . . . . . . . 12
 
           ![]_ ]_](_urbrack.gif)                 ![]_ ]_](_urbrack.gif)              ![]_ ]_](_urbrack.gif)               ![]_ ]_](_urbrack.gif)                  |
144 | 143 | 3ad2ant1 1035 |
. . . . . . . . . . 11
   
   

      ![]_ ]_](_urbrack.gif)                 ![]_ ]_](_urbrack.gif)              ![]_ ]_](_urbrack.gif)               ![]_ ]_](_urbrack.gif)                  |
145 | 131, 144 | eqtrd 2496 |
. . . . . . . . . 10
   
   

         ![]_ ]_](_urbrack.gif)             ![]_ ]_](_urbrack.gif)               ![]_ ]_](_urbrack.gif)                  |
146 | 145 | ifeq1d 3911 |
. . . . . . . . 9
   
   

            ![]_ ]_](_urbrack.gif)                      ![]_ ]_](_urbrack.gif)               ![]_ ]_](_urbrack.gif)                        |
147 | 146 | mpt2eq3dva 6387 |
. . . . . . . 8
 
      
            ![]_ ]_](_urbrack.gif)               
         ![]_ ]_](_urbrack.gif)               ![]_ ]_](_urbrack.gif)                         |
148 | 147 | fveq2d 5896 |
. . . . . . 7
 
                      ![]_ ]_](_urbrack.gif)                             ![]_ ]_](_urbrack.gif)               ![]_ ]_](_urbrack.gif)                          |
149 | 40, 41 | ring0cl 17857 |
. . . . . . . . . . 11

      |
150 | 65, 149 | syl 17 |
. . . . . . . . . 10
 
           |
151 | 150 | 3ad2ant1 1035 |
. . . . . . . . 9
   
   

      |
152 | 124, 151 | ifcld 3936 |
. . . . . . . 8
   
   

     ![]_ ]_](_urbrack.gif)         |
153 | 40, 135 | ringidcl 17856 |
. . . . . . . . . . . 12

      |
154 | 65, 153 | syl 17 |
. . . . . . . . . . 11
 
           |
155 | 154, 150 | ifcld 3936 |
. . . . . . . . . 10
 
                    |
156 | 40, 89 | ringcl 17849 |
. . . . . . . . . 10
    ![]_ ]_](_urbrack.gif)
                 ![]_ ]_](_urbrack.gif)
                |
157 | 65, 100, 155, 156 | syl3anc 1276 |
. . . . . . . . 9
 
        ![]_ ]_](_urbrack.gif)
                |
158 | 157 | 3ad2ant1 1035 |
. . . . . . . 8
   
   

   ![]_ ]_](_urbrack.gif)                 |
159 | 51 | adantr 471 |
. . . . . . . . . 10
 
             |
160 | 159 | fovrnda 6472 |
. . . . . . . . 9
   
             |
161 | 160 | 3impb 1211 |
. . . . . . . 8
   
   

      |
162 | 39, 40, 62, 63, 68, 152, 158, 161, 102 | mdetrlin2 19687 |
. . . . . . 7
 
                   ![]_ ]_](_urbrack.gif)               ![]_ ]_](_urbrack.gif)                                      ![]_ ]_](_urbrack.gif)                               ![]_ ]_](_urbrack.gif)
                         |
163 | 155 | 3ad2ant1 1035 |
. . . . . . . . . 10
   
   

               |
164 | 39, 40, 89, 63, 68, 163, 161, 100, 102 | mdetrsca2 19684 |
. . . . . . . . 9
 
                ![]_ ]_](_urbrack.gif)                          ![]_ ]_](_urbrack.gif)                                 |
165 | 43 | adantr 471 |
. . . . . . . . . . 11
 
    
  |
166 | 44, 39, 79, 45, 135, 41 | maducoeval 19719 |
. . . . . . . . . . 11
 
                                        |
167 | 165, 97, 102, 166 | syl3anc 1276 |
. . . . . . . . . 10
 
                                            |
168 | 167 | oveq2d 6336 |
. . . . . . . . 9
 
        ![]_ ]_](_urbrack.gif)
            ![]_ ]_](_urbrack.gif)                                 |
169 | 164, 168 | eqtr4d 2499 |
. . . . . . . 8
 
                ![]_ ]_](_urbrack.gif)                          ![]_ ]_](_urbrack.gif)            |
170 | 169 | oveq2d 6336 |
. . . . . . 7
 
          
        ![]_ ]_](_urbrack.gif)                        
      ![]_ ]_](_urbrack.gif)                                      ![]_ ]_](_urbrack.gif)                       ![]_ ]_](_urbrack.gif)             |
171 | 148, 162,
170 | 3eqtrrd 2501 |
. . . . . 6
 
          
        ![]_ ]_](_urbrack.gif)                       ![]_ ]_](_urbrack.gif)                            ![]_ ]_](_urbrack.gif)                 |
172 | 171 | adantr 471 |
. . . . 5
   
     g     ![]_ ]_](_urbrack.gif)                
        ![]_ ]_](_urbrack.gif)                              ![]_ ]_](_urbrack.gif)                       ![]_ ]_](_urbrack.gif)                            ![]_ ]_](_urbrack.gif)                 |
173 | 110, 112,
172 | 3eqtrd 2500 |
. . . 4
   
     g     ![]_ ]_](_urbrack.gif)                
        ![]_ ]_](_urbrack.gif)                 g         ![]_ ]_](_urbrack.gif)                
            ![]_ ]_](_urbrack.gif)                 |
174 | 173 | ex 440 |
. . 3
 
       g     ![]_ ]_](_urbrack.gif)                
        ![]_ ]_](_urbrack.gif)              
 g         ![]_ ]_](_urbrack.gif)                
            ![]_ ]_](_urbrack.gif)                  |
175 | 8, 16, 24, 32, 61, 174, 48 | findcard2d 7844 |
. 2
  g     ![]_ ]_](_urbrack.gif)                         ![]_ ]_](_urbrack.gif)                 |
176 | | nfcv 2603 |
. . . 4
             |
177 | | nfcsb1v 3391 |
. . . . 5
  
 ![]_ ]_](_urbrack.gif)  |
178 | | nfcv 2603 |
. . . . 5
  |
179 | | nfcv 2603 |
. . . . 5
           |
180 | 177, 178,
179 | nfov 6346 |
. . . 4
     ![]_ ]_](_urbrack.gif)
          |
181 | | csbeq1a 3384 |
. . . . 5
   ![]_ ]_](_urbrack.gif)   |
182 | | oveq1 6327 |
. . . . 5
                   |
183 | 181, 182 | oveq12d 6338 |
. . . 4
              ![]_ ]_](_urbrack.gif)            |
184 | 176, 180,
183 | cbvmpt 4510 |
. . 3
                ![]_ ]_](_urbrack.gif)            |
185 | 184 | oveq2i 6331 |
. 2
 g               g     ![]_ ]_](_urbrack.gif)             |
186 | | nfcv 2603 |
. . . . 5
            |
187 | | nfcv 2603 |
. . . . 5
            |
188 | | nfcv 2603 |
. . . . 5
       ![]_ ]_](_urbrack.gif)        |
189 | | nfv 1772 |
. . . . . 6
  |
190 | | nfcv 2603 |
. . . . . 6
       |
191 | 189, 177,
190 | nfif 3922 |
. . . . 5
       ![]_ ]_](_urbrack.gif)        |
192 | | eqeq1 2466 |
. . . . . . 7
 
   |
193 | 192 | adantr 471 |
. . . . . 6
 
     |
194 | 181 | adantl 472 |
. . . . . 6
 
   ![]_ ]_](_urbrack.gif)   |
195 | | oveq12 6329 |
. . . . . 6
 
           |
196 | 193, 194,
195 | ifbieq12d 3920 |
. . . . 5
 
               ![]_ ]_](_urbrack.gif)         |
197 | 186, 187,
188, 191, 196 | cbvmpt2 6402 |
. . . 4
     
           
 ![]_ ]_](_urbrack.gif)         |
198 | | iftrue 3899 |
. . . . . . . 8
      ![]_ ]_](_urbrack.gif)         ![]_ ]_](_urbrack.gif)   |
199 | 198 | eqcomd 2468 |
. . . . . . 7
   ![]_ ]_](_urbrack.gif)      ![]_ ]_](_urbrack.gif)         |
200 | 199 | adantl 472 |
. . . . . 6
 
   ![]_ ]_](_urbrack.gif)
     ![]_ ]_](_urbrack.gif)         |
201 | 200 | ifeq1d 3911 |
. . . . 5
 
      ![]_ ]_](_urbrack.gif)             
 ![]_ ]_](_urbrack.gif)               |
202 | 201 | mpt2eq3ia 6388 |
. . . 4
     
 ![]_ ]_](_urbrack.gif)                  ![]_ ]_](_urbrack.gif)               |
203 | 197, 202 | eqtri 2484 |
. . 3
     
                ![]_ ]_](_urbrack.gif)               |
204 | 203 | fveq2i 5895 |
. 2
                             ![]_ ]_](_urbrack.gif)                |
205 | 175, 185,
204 | 3eqtr4g 2521 |
1
  g                                |