Step | Hyp | Ref
| Expression |
1 | | oveq1 7412 |
. . . . . . . 8
โข (๐ = 1 โ (๐ ยท ๐) = (1 ยท ๐)) |
2 | 1 | oveq1d 7420 |
. . . . . . 7
โข (๐ = 1 โ ((๐ ยท ๐) ยท ๐) = ((1 ยท ๐) ยท ๐)) |
3 | | oveq1 7412 |
. . . . . . 7
โข (๐ = 1 โ (๐ ยท (๐ ยท ๐)) = (1 ยท (๐ ยท ๐))) |
4 | 2, 3 | eqeq12d 2748 |
. . . . . 6
โข (๐ = 1 โ (((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐)) โ ((1 ยท ๐) ยท ๐) = (1 ยท (๐ ยท ๐)))) |
5 | 4 | imbi2d 340 |
. . . . 5
โข (๐ = 1 โ (((๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp) โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐))) โ ((๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp) โ ((1 ยท ๐) ยท ๐) = (1 ยท (๐ ยท ๐))))) |
6 | | oveq1 7412 |
. . . . . . . 8
โข (๐ = ๐ โ (๐ ยท ๐) = (๐ ยท ๐)) |
7 | 6 | oveq1d 7420 |
. . . . . . 7
โข (๐ = ๐ โ ((๐ ยท ๐) ยท ๐) = ((๐ ยท ๐) ยท ๐)) |
8 | | oveq1 7412 |
. . . . . . 7
โข (๐ = ๐ โ (๐ ยท (๐ ยท ๐)) = (๐ ยท (๐ ยท ๐))) |
9 | 7, 8 | eqeq12d 2748 |
. . . . . 6
โข (๐ = ๐ โ (((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐)) โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐)))) |
10 | 9 | imbi2d 340 |
. . . . 5
โข (๐ = ๐ โ (((๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp) โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐))) โ ((๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp) โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐))))) |
11 | | oveq1 7412 |
. . . . . . . 8
โข (๐ = (๐ + 1) โ (๐ ยท ๐) = ((๐ + 1) ยท ๐)) |
12 | 11 | oveq1d 7420 |
. . . . . . 7
โข (๐ = (๐ + 1) โ ((๐ ยท ๐) ยท ๐) = (((๐ + 1) ยท ๐) ยท ๐)) |
13 | | oveq1 7412 |
. . . . . . 7
โข (๐ = (๐ + 1) โ (๐ ยท (๐ ยท ๐)) = ((๐ + 1) ยท (๐ ยท ๐))) |
14 | 12, 13 | eqeq12d 2748 |
. . . . . 6
โข (๐ = (๐ + 1) โ (((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐)) โ (((๐ + 1) ยท ๐) ยท ๐) = ((๐ + 1) ยท (๐ ยท ๐)))) |
15 | 14 | imbi2d 340 |
. . . . 5
โข (๐ = (๐ + 1) โ (((๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp) โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐))) โ ((๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp) โ (((๐ + 1) ยท ๐) ยท ๐) = ((๐ + 1) ยท (๐ ยท ๐))))) |
16 | | oveq1 7412 |
. . . . . . . 8
โข (๐ = ๐ โ (๐ ยท ๐) = (๐ ยท ๐)) |
17 | 16 | oveq1d 7420 |
. . . . . . 7
โข (๐ = ๐ โ ((๐ ยท ๐) ยท ๐) = ((๐ ยท ๐) ยท ๐)) |
18 | | oveq1 7412 |
. . . . . . 7
โข (๐ = ๐ โ (๐ ยท (๐ ยท ๐)) = (๐ ยท (๐ ยท ๐))) |
19 | 17, 18 | eqeq12d 2748 |
. . . . . 6
โข (๐ = ๐ โ (((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐)) โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐)))) |
20 | 19 | imbi2d 340 |
. . . . 5
โข (๐ = ๐ โ (((๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp) โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐))) โ ((๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp) โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐))))) |
21 | | nncn 12216 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ
โ) |
22 | 21 | mullidd 11228 |
. . . . . . . 8
โข (๐ โ โ โ (1
ยท ๐) = ๐) |
23 | 22 | 3ad2ant1 1133 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp) โ (1 ยท ๐) = ๐) |
24 | 23 | oveq1d 7420 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp) โ ((1 ยท ๐) ยท ๐) = (๐ ยท ๐)) |
25 | | sgrpmgm 18611 |
. . . . . . . . 9
โข (๐บ โ Smgrp โ ๐บ โ Mgm) |
26 | | mulgass.b |
. . . . . . . . . 10
โข ๐ต = (Baseโ๐บ) |
27 | | mulgass.t |
. . . . . . . . . 10
โข ยท =
(.gโ๐บ) |
28 | 26, 27 | mulgnncl 18963 |
. . . . . . . . 9
โข ((๐บ โ Mgm โง ๐ โ โ โง ๐ โ ๐ต) โ (๐ ยท ๐) โ ๐ต) |
29 | 25, 28 | syl3an1 1163 |
. . . . . . . 8
โข ((๐บ โ Smgrp โง ๐ โ โ โง ๐ โ ๐ต) โ (๐ ยท ๐) โ ๐ต) |
30 | 29 | 3coml 1127 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp) โ (๐ ยท ๐) โ ๐ต) |
31 | 26, 27 | mulg1 18955 |
. . . . . . 7
โข ((๐ ยท ๐) โ ๐ต โ (1 ยท (๐ ยท ๐)) = (๐ ยท ๐)) |
32 | 30, 31 | syl 17 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp) โ (1 ยท (๐ ยท ๐)) = (๐ ยท ๐)) |
33 | 24, 32 | eqtr4d 2775 |
. . . . 5
โข ((๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp) โ ((1 ยท ๐) ยท ๐) = (1 ยท (๐ ยท ๐))) |
34 | | oveq1 7412 |
. . . . . . . 8
โข (((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐)) โ (((๐ ยท ๐) ยท ๐)(+gโ๐บ)(๐ ยท ๐)) = ((๐ ยท (๐ ยท ๐))(+gโ๐บ)(๐ ยท ๐))) |
35 | | nncn 12216 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ๐ โ
โ) |
36 | 35 | adantr 481 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง (๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp)) โ ๐ โ โ) |
37 | | simpr1 1194 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง (๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp)) โ ๐ โ โ) |
38 | 37 | nncnd 12224 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง (๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp)) โ ๐ โ โ) |
39 | 36, 38 | adddirp1d 11236 |
. . . . . . . . . . 11
โข ((๐ โ โ โง (๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp)) โ ((๐ + 1) ยท ๐) = ((๐ ยท ๐) + ๐)) |
40 | 39 | oveq1d 7420 |
. . . . . . . . . 10
โข ((๐ โ โ โง (๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp)) โ (((๐ + 1) ยท ๐) ยท ๐) = (((๐ ยท ๐) + ๐) ยท ๐)) |
41 | | simpr3 1196 |
. . . . . . . . . . 11
โข ((๐ โ โ โง (๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp)) โ ๐บ โ Smgrp) |
42 | | nnmulcl 12232 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ โ) โ (๐ ยท ๐) โ โ) |
43 | 42 | 3ad2antr1 1188 |
. . . . . . . . . . 11
โข ((๐ โ โ โง (๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp)) โ (๐ ยท ๐) โ โ) |
44 | | simpr2 1195 |
. . . . . . . . . . 11
โข ((๐ โ โ โง (๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp)) โ ๐ โ ๐ต) |
45 | | eqid 2732 |
. . . . . . . . . . . 12
โข
(+gโ๐บ) = (+gโ๐บ) |
46 | 26, 27, 45 | mulgnndir 18977 |
. . . . . . . . . . 11
โข ((๐บ โ Smgrp โง ((๐ ยท ๐) โ โ โง ๐ โ โ โง ๐ โ ๐ต)) โ (((๐ ยท ๐) + ๐) ยท ๐) = (((๐ ยท ๐) ยท ๐)(+gโ๐บ)(๐ ยท ๐))) |
47 | 41, 43, 37, 44, 46 | syl13anc 1372 |
. . . . . . . . . 10
โข ((๐ โ โ โง (๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp)) โ (((๐ ยท ๐) + ๐) ยท ๐) = (((๐ ยท ๐) ยท ๐)(+gโ๐บ)(๐ ยท ๐))) |
48 | 40, 47 | eqtrd 2772 |
. . . . . . . . 9
โข ((๐ โ โ โง (๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp)) โ (((๐ + 1) ยท ๐) ยท ๐) = (((๐ ยท ๐) ยท ๐)(+gโ๐บ)(๐ ยท ๐))) |
49 | 26, 27, 45 | mulgnnp1 18956 |
. . . . . . . . . 10
โข ((๐ โ โ โง (๐ ยท ๐) โ ๐ต) โ ((๐ + 1) ยท (๐ ยท ๐)) = ((๐ ยท (๐ ยท ๐))(+gโ๐บ)(๐ ยท ๐))) |
50 | 30, 49 | sylan2 593 |
. . . . . . . . 9
โข ((๐ โ โ โง (๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp)) โ ((๐ + 1) ยท (๐ ยท ๐)) = ((๐ ยท (๐ ยท ๐))(+gโ๐บ)(๐ ยท ๐))) |
51 | 48, 50 | eqeq12d 2748 |
. . . . . . . 8
โข ((๐ โ โ โง (๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp)) โ ((((๐ + 1) ยท ๐) ยท ๐) = ((๐ + 1) ยท (๐ ยท ๐)) โ (((๐ ยท ๐) ยท ๐)(+gโ๐บ)(๐ ยท ๐)) = ((๐ ยท (๐ ยท ๐))(+gโ๐บ)(๐ ยท ๐)))) |
52 | 34, 51 | imbitrrid 245 |
. . . . . . 7
โข ((๐ โ โ โง (๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp)) โ (((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐)) โ (((๐ + 1) ยท ๐) ยท ๐) = ((๐ + 1) ยท (๐ ยท ๐)))) |
53 | 52 | ex 413 |
. . . . . 6
โข (๐ โ โ โ ((๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp) โ (((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐)) โ (((๐ + 1) ยท ๐) ยท ๐) = ((๐ + 1) ยท (๐ ยท ๐))))) |
54 | 53 | a2d 29 |
. . . . 5
โข (๐ โ โ โ (((๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp) โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐))) โ ((๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp) โ (((๐ + 1) ยท ๐) ยท ๐) = ((๐ + 1) ยท (๐ ยท ๐))))) |
55 | 5, 10, 15, 20, 33, 54 | nnind 12226 |
. . . 4
โข (๐ โ โ โ ((๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp) โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐)))) |
56 | 55 | 3expd 1353 |
. . 3
โข (๐ โ โ โ (๐ โ โ โ (๐ โ ๐ต โ (๐บ โ Smgrp โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐)))))) |
57 | 56 | com4r 94 |
. 2
โข (๐บ โ Smgrp โ (๐ โ โ โ (๐ โ โ โ (๐ โ ๐ต โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐)))))) |
58 | 57 | 3imp2 1349 |
1
โข ((๐บ โ Smgrp โง (๐ โ โ โง ๐ โ โ โง ๐ โ ๐ต)) โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐))) |