Step | Hyp | Ref
| Expression |
1 | | rngdi.b |
. . . 4
โข ๐ต = (Baseโ๐
) |
2 | | eqid 2733 |
. . . 4
โข
(mulGrpโ๐
) =
(mulGrpโ๐
) |
3 | | rngdi.p |
. . . 4
โข + =
(+gโ๐
) |
4 | | rngdi.t |
. . . 4
โข ยท =
(.rโ๐
) |
5 | 1, 2, 3, 4 | isrng 46260 |
. . 3
โข (๐
โ Rng โ (๐
โ Abel โง
(mulGrpโ๐
) โ
Smgrp โง โ๐
โ ๐ต โ๐ โ ๐ต โ๐ โ ๐ต ((๐ ยท (๐ + ๐)) = ((๐ ยท ๐) + (๐ ยท ๐)) โง ((๐ + ๐) ยท ๐) = ((๐ ยท ๐) + (๐ ยท ๐))))) |
6 | | oveq1 7365 |
. . . . . . . 8
โข (๐ = ๐ โ (๐ ยท (๐ + ๐)) = (๐ ยท (๐ + ๐))) |
7 | | oveq1 7365 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐ ยท ๐) = (๐ ยท ๐)) |
8 | | oveq1 7365 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐ ยท ๐) = (๐ ยท ๐)) |
9 | 7, 8 | oveq12d 7376 |
. . . . . . . 8
โข (๐ = ๐ โ ((๐ ยท ๐) + (๐ ยท ๐)) = ((๐ ยท ๐) + (๐ ยท ๐))) |
10 | 6, 9 | eqeq12d 2749 |
. . . . . . 7
โข (๐ = ๐ โ ((๐ ยท (๐ + ๐)) = ((๐ ยท ๐) + (๐ ยท ๐)) โ (๐ ยท (๐ + ๐)) = ((๐ ยท ๐) + (๐ ยท ๐)))) |
11 | | oveq1 7365 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐ + ๐) = (๐ + ๐)) |
12 | 11 | oveq1d 7373 |
. . . . . . . 8
โข (๐ = ๐ โ ((๐ + ๐) ยท ๐) = ((๐ + ๐) ยท ๐)) |
13 | 8 | oveq1d 7373 |
. . . . . . . 8
โข (๐ = ๐ โ ((๐ ยท ๐) + (๐ ยท ๐)) = ((๐ ยท ๐) + (๐ ยท ๐))) |
14 | 12, 13 | eqeq12d 2749 |
. . . . . . 7
โข (๐ = ๐ โ (((๐ + ๐) ยท ๐) = ((๐ ยท ๐) + (๐ ยท ๐)) โ ((๐ + ๐) ยท ๐) = ((๐ ยท ๐) + (๐ ยท ๐)))) |
15 | 10, 14 | anbi12d 632 |
. . . . . 6
โข (๐ = ๐ โ (((๐ ยท (๐ + ๐)) = ((๐ ยท ๐) + (๐ ยท ๐)) โง ((๐ + ๐) ยท ๐) = ((๐ ยท ๐) + (๐ ยท ๐))) โ ((๐ ยท (๐ + ๐)) = ((๐ ยท ๐) + (๐ ยท ๐)) โง ((๐ + ๐) ยท ๐) = ((๐ ยท ๐) + (๐ ยท ๐))))) |
16 | | oveq1 7365 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐ + ๐) = (๐ + ๐)) |
17 | 16 | oveq2d 7374 |
. . . . . . . 8
โข (๐ = ๐ โ (๐ ยท (๐ + ๐)) = (๐ ยท (๐ + ๐))) |
18 | | oveq2 7366 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐ ยท ๐) = (๐ ยท ๐)) |
19 | 18 | oveq1d 7373 |
. . . . . . . 8
โข (๐ = ๐ โ ((๐ ยท ๐) + (๐ ยท ๐)) = ((๐ ยท ๐) + (๐ ยท ๐))) |
20 | 17, 19 | eqeq12d 2749 |
. . . . . . 7
โข (๐ = ๐ โ ((๐ ยท (๐ + ๐)) = ((๐ ยท ๐) + (๐ ยท ๐)) โ (๐ ยท (๐ + ๐)) = ((๐ ยท ๐) + (๐ ยท ๐)))) |
21 | | oveq2 7366 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐ + ๐) = (๐ + ๐)) |
22 | 21 | oveq1d 7373 |
. . . . . . . 8
โข (๐ = ๐ โ ((๐ + ๐) ยท ๐) = ((๐ + ๐) ยท ๐)) |
23 | | oveq1 7365 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐ ยท ๐) = (๐ ยท ๐)) |
24 | 23 | oveq2d 7374 |
. . . . . . . 8
โข (๐ = ๐ โ ((๐ ยท ๐) + (๐ ยท ๐)) = ((๐ ยท ๐) + (๐ ยท ๐))) |
25 | 22, 24 | eqeq12d 2749 |
. . . . . . 7
โข (๐ = ๐ โ (((๐ + ๐) ยท ๐) = ((๐ ยท ๐) + (๐ ยท ๐)) โ ((๐ + ๐) ยท ๐) = ((๐ ยท ๐) + (๐ ยท ๐)))) |
26 | 20, 25 | anbi12d 632 |
. . . . . 6
โข (๐ = ๐ โ (((๐ ยท (๐ + ๐)) = ((๐ ยท ๐) + (๐ ยท ๐)) โง ((๐ + ๐) ยท ๐) = ((๐ ยท ๐) + (๐ ยท ๐))) โ ((๐ ยท (๐ + ๐)) = ((๐ ยท ๐) + (๐ ยท ๐)) โง ((๐ + ๐) ยท ๐) = ((๐ ยท ๐) + (๐ ยท ๐))))) |
27 | | oveq2 7366 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐ + ๐) = (๐ + ๐)) |
28 | 27 | oveq2d 7374 |
. . . . . . . 8
โข (๐ = ๐ โ (๐ ยท (๐ + ๐)) = (๐ ยท (๐ + ๐))) |
29 | | oveq2 7366 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐ ยท ๐) = (๐ ยท ๐)) |
30 | 29 | oveq2d 7374 |
. . . . . . . 8
โข (๐ = ๐ โ ((๐ ยท ๐) + (๐ ยท ๐)) = ((๐ ยท ๐) + (๐ ยท ๐))) |
31 | 28, 30 | eqeq12d 2749 |
. . . . . . 7
โข (๐ = ๐ โ ((๐ ยท (๐ + ๐)) = ((๐ ยท ๐) + (๐ ยท ๐)) โ (๐ ยท (๐ + ๐)) = ((๐ ยท ๐) + (๐ ยท ๐)))) |
32 | | oveq2 7366 |
. . . . . . . 8
โข (๐ = ๐ โ ((๐ + ๐) ยท ๐) = ((๐ + ๐) ยท ๐)) |
33 | | oveq2 7366 |
. . . . . . . . 9
โข (๐ = ๐ โ (๐ ยท ๐) = (๐ ยท ๐)) |
34 | 29, 33 | oveq12d 7376 |
. . . . . . . 8
โข (๐ = ๐ โ ((๐ ยท ๐) + (๐ ยท ๐)) = ((๐ ยท ๐) + (๐ ยท ๐))) |
35 | 32, 34 | eqeq12d 2749 |
. . . . . . 7
โข (๐ = ๐ โ (((๐ + ๐) ยท ๐) = ((๐ ยท ๐) + (๐ ยท ๐)) โ ((๐ + ๐) ยท ๐) = ((๐ ยท ๐) + (๐ ยท ๐)))) |
36 | 31, 35 | anbi12d 632 |
. . . . . 6
โข (๐ = ๐ โ (((๐ ยท (๐ + ๐)) = ((๐ ยท ๐) + (๐ ยท ๐)) โง ((๐ + ๐) ยท ๐) = ((๐ ยท ๐) + (๐ ยท ๐))) โ ((๐ ยท (๐ + ๐)) = ((๐ ยท ๐) + (๐ ยท ๐)) โง ((๐ + ๐) ยท ๐) = ((๐ ยท ๐) + (๐ ยท ๐))))) |
37 | 15, 26, 36 | rspc3v 3592 |
. . . . 5
โข ((๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต) โ (โ๐ โ ๐ต โ๐ โ ๐ต โ๐ โ ๐ต ((๐ ยท (๐ + ๐)) = ((๐ ยท ๐) + (๐ ยท ๐)) โง ((๐ + ๐) ยท ๐) = ((๐ ยท ๐) + (๐ ยท ๐))) โ ((๐ ยท (๐ + ๐)) = ((๐ ยท ๐) + (๐ ยท ๐)) โง ((๐ + ๐) ยท ๐) = ((๐ ยท ๐) + (๐ ยท ๐))))) |
38 | | simpr 486 |
. . . . 5
โข (((๐ ยท (๐ + ๐)) = ((๐ ยท ๐) + (๐ ยท ๐)) โง ((๐ + ๐) ยท ๐) = ((๐ ยท ๐) + (๐ ยท ๐))) โ ((๐ + ๐) ยท ๐) = ((๐ ยท ๐) + (๐ ยท ๐))) |
39 | 37, 38 | syl6com 37 |
. . . 4
โข
(โ๐ โ
๐ต โ๐ โ ๐ต โ๐ โ ๐ต ((๐ ยท (๐ + ๐)) = ((๐ ยท ๐) + (๐ ยท ๐)) โง ((๐ + ๐) ยท ๐) = ((๐ ยท ๐) + (๐ ยท ๐))) โ ((๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต) โ ((๐ + ๐) ยท ๐) = ((๐ ยท ๐) + (๐ ยท ๐)))) |
40 | 39 | 3ad2ant3 1136 |
. . 3
โข ((๐
โ Abel โง
(mulGrpโ๐
) โ
Smgrp โง โ๐
โ ๐ต โ๐ โ ๐ต โ๐ โ ๐ต ((๐ ยท (๐ + ๐)) = ((๐ ยท ๐) + (๐ ยท ๐)) โง ((๐ + ๐) ยท ๐) = ((๐ ยท ๐) + (๐ ยท ๐)))) โ ((๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต) โ ((๐ + ๐) ยท ๐) = ((๐ ยท ๐) + (๐ ยท ๐)))) |
41 | 5, 40 | sylbi 216 |
. 2
โข (๐
โ Rng โ ((๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต) โ ((๐ + ๐) ยท ๐) = ((๐ ยท ๐) + (๐ ยท ๐)))) |
42 | 41 | imp 408 |
1
โข ((๐
โ Rng โง (๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต)) โ ((๐ + ๐) ยท ๐) = ((๐ ยท ๐) + (๐ ยท ๐))) |