Description: Obsolete version of mgpds as of 18-Oct-2024. Distance function of the multiplication group. (Contributed by Mario Carneiro, 5-Oct-2015) (Proof modification is discouraged.) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | mgpbas.1 | |- M = ( mulGrp ` R ) |
|
| mgpds.2 | |- B = ( dist ` R ) |
||
| Assertion | mgpdsOLD | |- B = ( dist ` M ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | mgpbas.1 | |- M = ( mulGrp ` R ) |
|
| 2 | mgpds.2 | |- B = ( dist ` R ) |
|
| 3 | df-ds | |- dist = Slot ; 1 2 |
|
| 4 | 1nn0 | |- 1 e. NN0 |
|
| 5 | 2nn | |- 2 e. NN |
|
| 6 | 4 5 | decnncl | |- ; 1 2 e. NN |
| 7 | 2re | |- 2 e. RR |
|
| 8 | 1nn | |- 1 e. NN |
|
| 9 | 2nn0 | |- 2 e. NN0 |
|
| 10 | 2lt10 | |- 2 < ; 1 0 |
|
| 11 | 8 9 9 10 | declti | |- 2 < ; 1 2 |
| 12 | 7 11 | gtneii | |- ; 1 2 =/= 2 |
| 13 | 1 3 6 12 | mgplemOLD | |- ( dist ` R ) = ( dist ` M ) |
| 14 | 2 13 | eqtri | |- B = ( dist ` M ) |