Detailed syntax breakdown of Definition df-srg
| Step | Hyp | Ref
| Expression |
| 1 | | csrg 13519 |
. 2
SRing |
| 2 | | vf |
. . . . . . 7
 |
| 3 | 2 | cv 1363 |
. . . . . 6
 |
| 4 | | cmgp 13476 |
. . . . . 6
mulGrp |
| 5 | 3, 4 | cfv 5258 |
. . . . 5
mulGrp   |
| 6 | | cmnd 13057 |
. . . . 5
 |
| 7 | 5, 6 | wcel 2167 |
. . . 4
mulGrp   |
| 8 | | vx |
. . . . . . . . . . . . . . . 16
 |
| 9 | 8 | cv 1363 |
. . . . . . . . . . . . . . 15
 |
| 10 | | vy |
. . . . . . . . . . . . . . . . 17
 |
| 11 | 10 | cv 1363 |
. . . . . . . . . . . . . . . 16
 |
| 12 | | vz |
. . . . . . . . . . . . . . . . 17
 |
| 13 | 12 | cv 1363 |
. . . . . . . . . . . . . . . 16
 |
| 14 | | vp |
. . . . . . . . . . . . . . . . 17
 |
| 15 | 14 | cv 1363 |
. . . . . . . . . . . . . . . 16
 |
| 16 | 11, 13, 15 | co 5922 |
. . . . . . . . . . . . . . 15
     |
| 17 | | vt |
. . . . . . . . . . . . . . . 16
 |
| 18 | 17 | cv 1363 |
. . . . . . . . . . . . . . 15
 |
| 19 | 9, 16, 18 | co 5922 |
. . . . . . . . . . . . . 14
         |
| 20 | 9, 11, 18 | co 5922 |
. . . . . . . . . . . . . . 15
     |
| 21 | 9, 13, 18 | co 5922 |
. . . . . . . . . . . . . . 15
     |
| 22 | 20, 21, 15 | co 5922 |
. . . . . . . . . . . . . 14
             |
| 23 | 19, 22 | wceq 1364 |
. . . . . . . . . . . . 13
                     |
| 24 | 9, 11, 15 | co 5922 |
. . . . . . . . . . . . . . 15
     |
| 25 | 24, 13, 18 | co 5922 |
. . . . . . . . . . . . . 14
         |
| 26 | 11, 13, 18 | co 5922 |
. . . . . . . . . . . . . . 15
     |
| 27 | 21, 26, 15 | co 5922 |
. . . . . . . . . . . . . 14
             |
| 28 | 25, 27 | wceq 1364 |
. . . . . . . . . . . . 13
                     |
| 29 | 23, 28 | wa 104 |
. . . . . . . . . . . 12
                                           |
| 30 | | vr |
. . . . . . . . . . . . 13
 |
| 31 | 30 | cv 1363 |
. . . . . . . . . . . 12
 |
| 32 | 29, 12, 31 | wral 2475 |
. . . . . . . . . . 11

                                           |
| 33 | 32, 10, 31 | wral 2475 |
. . . . . . . . . 10


                                           |
| 34 | | vn |
. . . . . . . . . . . . . 14
 |
| 35 | 34 | cv 1363 |
. . . . . . . . . . . . 13
 |
| 36 | 35, 9, 18 | co 5922 |
. . . . . . . . . . . 12
     |
| 37 | 36, 35 | wceq 1364 |
. . . . . . . . . . 11
     |
| 38 | 9, 35, 18 | co 5922 |
. . . . . . . . . . . 12
     |
| 39 | 38, 35 | wceq 1364 |
. . . . . . . . . . 11
     |
| 40 | 37, 39 | wa 104 |
. . . . . . . . . 10
           |
| 41 | 33, 40 | wa 104 |
. . . . . . . . 9
 

                                                      |
| 42 | 41, 8, 31 | wral 2475 |
. . . . . . . 8

 

                                                      |
| 43 | | c0g 12927 |
. . . . . . . . 9
 |
| 44 | 3, 43 | cfv 5258 |
. . . . . . . 8
     |
| 45 | 42, 34, 44 | wsbc 2989 |
. . . . . . 7
      ![]. ].](_drbrack.gif)   

                                                      |
| 46 | | cmulr 12756 |
. . . . . . . 8
 |
| 47 | 3, 46 | cfv 5258 |
. . . . . . 7
     |
| 48 | 45, 17, 47 | wsbc 2989 |
. . . . . 6
      ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)   

                                                      |
| 49 | | cplusg 12755 |
. . . . . . 7
 |
| 50 | 3, 49 | cfv 5258 |
. . . . . 6
    |
| 51 | 48, 14, 50 | wsbc 2989 |
. . . . 5
     ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)   

                                                      |
| 52 | | cbs 12678 |
. . . . . 6
 |
| 53 | 3, 52 | cfv 5258 |
. . . . 5
     |
| 54 | 51, 30, 53 | wsbc 2989 |
. . . 4
      ![]. ].](_drbrack.gif)      ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)                                                           |
| 55 | 7, 54 | wa 104 |
. . 3
 mulGrp        ![]. ].](_drbrack.gif)      ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif) 
                                                          |
| 56 | | ccmn 13414 |
. . 3
CMnd |
| 57 | 55, 2, 56 | crab 2479 |
. 2
 CMnd  mulGrp        ![]. ].](_drbrack.gif)      ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif) 
                                                           |
| 58 | 1, 57 | wceq 1364 |
1
SRing  CMnd
 mulGrp        ![]. ].](_drbrack.gif)      ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)                                                             |