Detailed syntax breakdown of Definition df-ring
Step | Hyp | Ref
| Expression |
1 | | crg 13132 |
. 2
 |
2 | | vf |
. . . . . . 7
 |
3 | 2 | cv 1352 |
. . . . . 6
 |
4 | | cmgp 13083 |
. . . . . 6
mulGrp |
5 | 3, 4 | cfv 5216 |
. . . . 5
mulGrp   |
6 | | cmnd 12771 |
. . . . 5
 |
7 | 5, 6 | wcel 2148 |
. . . 4
mulGrp   |
8 | | vx |
. . . . . . . . . . . . . 14
 |
9 | 8 | cv 1352 |
. . . . . . . . . . . . 13
 |
10 | | vy |
. . . . . . . . . . . . . . 15
 |
11 | 10 | cv 1352 |
. . . . . . . . . . . . . 14
 |
12 | | vz |
. . . . . . . . . . . . . . 15
 |
13 | 12 | cv 1352 |
. . . . . . . . . . . . . 14
 |
14 | | vp |
. . . . . . . . . . . . . . 15
 |
15 | 14 | cv 1352 |
. . . . . . . . . . . . . 14
 |
16 | 11, 13, 15 | co 5874 |
. . . . . . . . . . . . 13
     |
17 | | vt |
. . . . . . . . . . . . . 14
 |
18 | 17 | cv 1352 |
. . . . . . . . . . . . 13
 |
19 | 9, 16, 18 | co 5874 |
. . . . . . . . . . . 12
         |
20 | 9, 11, 18 | co 5874 |
. . . . . . . . . . . . 13
     |
21 | 9, 13, 18 | co 5874 |
. . . . . . . . . . . . 13
     |
22 | 20, 21, 15 | co 5874 |
. . . . . . . . . . . 12
             |
23 | 19, 22 | wceq 1353 |
. . . . . . . . . . 11
                     |
24 | 9, 11, 15 | co 5874 |
. . . . . . . . . . . . 13
     |
25 | 24, 13, 18 | co 5874 |
. . . . . . . . . . . 12
         |
26 | 11, 13, 18 | co 5874 |
. . . . . . . . . . . . 13
     |
27 | 21, 26, 15 | co 5874 |
. . . . . . . . . . . 12
             |
28 | 25, 27 | wceq 1353 |
. . . . . . . . . . 11
                     |
29 | 23, 28 | wa 104 |
. . . . . . . . . 10
                                           |
30 | | vr |
. . . . . . . . . . 11
 |
31 | 30 | cv 1352 |
. . . . . . . . . 10
 |
32 | 29, 12, 31 | wral 2455 |
. . . . . . . . 9

                                           |
33 | 32, 10, 31 | wral 2455 |
. . . . . . . 8


                                           |
34 | 33, 8, 31 | wral 2455 |
. . . . . . 7



                                           |
35 | | cmulr 12531 |
. . . . . . . 8
 |
36 | 3, 35 | cfv 5216 |
. . . . . . 7
     |
37 | 34, 17, 36 | wsbc 2962 |
. . . . . 6
      ![]. ].](_drbrack.gif)                                               |
38 | | cplusg 12530 |
. . . . . . 7
 |
39 | 3, 38 | cfv 5216 |
. . . . . 6
    |
40 | 37, 14, 39 | wsbc 2962 |
. . . . 5
     ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)                                               |
41 | | cbs 12456 |
. . . . . 6
 |
42 | 3, 41 | cfv 5216 |
. . . . 5
     |
43 | 40, 30, 42 | wsbc 2962 |
. . . 4
      ![]. ].](_drbrack.gif)      ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)                                               |
44 | 7, 43 | wa 104 |
. . 3
 mulGrp        ![]. ].](_drbrack.gif)      ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif) 


                                            |
45 | | cgrp 12831 |
. . 3
 |
46 | 44, 2, 45 | crab 2459 |
. 2
  mulGrp        ![]. ].](_drbrack.gif)      ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)                                                 |
47 | 1, 46 | wceq 1353 |
1
  mulGrp        ![]. ].](_drbrack.gif)      ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif) 


                                             |