Step | Hyp | Ref
| Expression |
1 | | oveq1 5881 |
. . . . . . . 8
โข (๐ = 1 โ (๐ ยท ๐) = (1 ยท ๐)) |
2 | 1 | oveq1d 5889 |
. . . . . . 7
โข (๐ = 1 โ ((๐ ยท ๐) ยท ๐) = ((1 ยท ๐) ยท ๐)) |
3 | | oveq1 5881 |
. . . . . . 7
โข (๐ = 1 โ (๐ ยท (๐ ยท ๐)) = (1 ยท (๐ ยท ๐))) |
4 | 2, 3 | eqeq12d 2192 |
. . . . . 6
โข (๐ = 1 โ (((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐)) โ ((1 ยท ๐) ยท ๐) = (1 ยท (๐ ยท ๐)))) |
5 | 4 | imbi2d 230 |
. . . . 5
โข (๐ = 1 โ (((๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp) โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐))) โ ((๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp) โ ((1 ยท ๐) ยท ๐) = (1 ยท (๐ ยท ๐))))) |
6 | | oveq1 5881 |
. . . . . . . 8
โข (๐ = ๐ โ (๐ ยท ๐) = (๐ ยท ๐)) |
7 | 6 | oveq1d 5889 |
. . . . . . 7
โข (๐ = ๐ โ ((๐ ยท ๐) ยท ๐) = ((๐ ยท ๐) ยท ๐)) |
8 | | oveq1 5881 |
. . . . . . 7
โข (๐ = ๐ โ (๐ ยท (๐ ยท ๐)) = (๐ ยท (๐ ยท ๐))) |
9 | 7, 8 | eqeq12d 2192 |
. . . . . 6
โข (๐ = ๐ โ (((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐)) โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐)))) |
10 | 9 | imbi2d 230 |
. . . . 5
โข (๐ = ๐ โ (((๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp) โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐))) โ ((๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp) โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐))))) |
11 | | oveq1 5881 |
. . . . . . . 8
โข (๐ = (๐ + 1) โ (๐ ยท ๐) = ((๐ + 1) ยท ๐)) |
12 | 11 | oveq1d 5889 |
. . . . . . 7
โข (๐ = (๐ + 1) โ ((๐ ยท ๐) ยท ๐) = (((๐ + 1) ยท ๐) ยท ๐)) |
13 | | oveq1 5881 |
. . . . . . 7
โข (๐ = (๐ + 1) โ (๐ ยท (๐ ยท ๐)) = ((๐ + 1) ยท (๐ ยท ๐))) |
14 | 12, 13 | eqeq12d 2192 |
. . . . . 6
โข (๐ = (๐ + 1) โ (((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐)) โ (((๐ + 1) ยท ๐) ยท ๐) = ((๐ + 1) ยท (๐ ยท ๐)))) |
15 | 14 | imbi2d 230 |
. . . . 5
โข (๐ = (๐ + 1) โ (((๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp) โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐))) โ ((๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp) โ (((๐ + 1) ยท ๐) ยท ๐) = ((๐ + 1) ยท (๐ ยท ๐))))) |
16 | | oveq1 5881 |
. . . . . . . 8
โข (๐ = ๐ โ (๐ ยท ๐) = (๐ ยท ๐)) |
17 | 16 | oveq1d 5889 |
. . . . . . 7
โข (๐ = ๐ โ ((๐ ยท ๐) ยท ๐) = ((๐ ยท ๐) ยท ๐)) |
18 | | oveq1 5881 |
. . . . . . 7
โข (๐ = ๐ โ (๐ ยท (๐ ยท ๐)) = (๐ ยท (๐ ยท ๐))) |
19 | 17, 18 | eqeq12d 2192 |
. . . . . 6
โข (๐ = ๐ โ (((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐)) โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐)))) |
20 | 19 | imbi2d 230 |
. . . . 5
โข (๐ = ๐ โ (((๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp) โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐))) โ ((๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp) โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐))))) |
21 | | nncn 8926 |
. . . . . . . . 9
โข (๐ โ โ โ ๐ โ
โ) |
22 | 21 | mulid2d 7975 |
. . . . . . . 8
โข (๐ โ โ โ (1
ยท ๐) = ๐) |
23 | 22 | 3ad2ant1 1018 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp) โ (1 ยท ๐) = ๐) |
24 | 23 | oveq1d 5889 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp) โ ((1 ยท ๐) ยท ๐) = (๐ ยท ๐)) |
25 | | sgrpmgm 12812 |
. . . . . . . . 9
โข (๐บ โ Smgrp โ ๐บ โ Mgm) |
26 | | mulgass.b |
. . . . . . . . . 10
โข ๐ต = (Baseโ๐บ) |
27 | | mulgass.t |
. . . . . . . . . 10
โข ยท =
(.gโ๐บ) |
28 | 26, 27 | mulgnncl 12997 |
. . . . . . . . 9
โข ((๐บ โ Mgm โง ๐ โ โ โง ๐ โ ๐ต) โ (๐ ยท ๐) โ ๐ต) |
29 | 25, 28 | syl3an1 1271 |
. . . . . . . 8
โข ((๐บ โ Smgrp โง ๐ โ โ โง ๐ โ ๐ต) โ (๐ ยท ๐) โ ๐ต) |
30 | 29 | 3coml 1210 |
. . . . . . 7
โข ((๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp) โ (๐ ยท ๐) โ ๐ต) |
31 | 26, 27 | mulg1 12989 |
. . . . . . 7
โข ((๐ ยท ๐) โ ๐ต โ (1 ยท (๐ ยท ๐)) = (๐ ยท ๐)) |
32 | 30, 31 | syl 14 |
. . . . . 6
โข ((๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp) โ (1 ยท (๐ ยท ๐)) = (๐ ยท ๐)) |
33 | 24, 32 | eqtr4d 2213 |
. . . . 5
โข ((๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp) โ ((1 ยท ๐) ยท ๐) = (1 ยท (๐ ยท ๐))) |
34 | | oveq1 5881 |
. . . . . . . 8
โข (((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐)) โ (((๐ ยท ๐) ยท ๐)(+gโ๐บ)(๐ ยท ๐)) = ((๐ ยท (๐ ยท ๐))(+gโ๐บ)(๐ ยท ๐))) |
35 | | nncn 8926 |
. . . . . . . . . . . . 13
โข (๐ โ โ โ ๐ โ
โ) |
36 | 35 | adantr 276 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง (๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp)) โ ๐ โ โ) |
37 | | simpr1 1003 |
. . . . . . . . . . . . 13
โข ((๐ โ โ โง (๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp)) โ ๐ โ โ) |
38 | 37 | nncnd 8932 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง (๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp)) โ ๐ โ โ) |
39 | 36, 38 | adddirp1d 7983 |
. . . . . . . . . . 11
โข ((๐ โ โ โง (๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp)) โ ((๐ + 1) ยท ๐) = ((๐ ยท ๐) + ๐)) |
40 | 39 | oveq1d 5889 |
. . . . . . . . . 10
โข ((๐ โ โ โง (๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp)) โ (((๐ + 1) ยท ๐) ยท ๐) = (((๐ ยท ๐) + ๐) ยท ๐)) |
41 | | simpr3 1005 |
. . . . . . . . . . 11
โข ((๐ โ โ โง (๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp)) โ ๐บ โ Smgrp) |
42 | | nnmulcl 8939 |
. . . . . . . . . . . 12
โข ((๐ โ โ โง ๐ โ โ) โ (๐ ยท ๐) โ โ) |
43 | 42 | 3ad2antr1 1162 |
. . . . . . . . . . 11
โข ((๐ โ โ โง (๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp)) โ (๐ ยท ๐) โ โ) |
44 | | simpr2 1004 |
. . . . . . . . . . 11
โข ((๐ โ โ โง (๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp)) โ ๐ โ ๐ต) |
45 | | eqid 2177 |
. . . . . . . . . . . 12
โข
(+gโ๐บ) = (+gโ๐บ) |
46 | 26, 27, 45 | mulgnndir 13010 |
. . . . . . . . . . 11
โข ((๐บ โ Smgrp โง ((๐ ยท ๐) โ โ โง ๐ โ โ โง ๐ โ ๐ต)) โ (((๐ ยท ๐) + ๐) ยท ๐) = (((๐ ยท ๐) ยท ๐)(+gโ๐บ)(๐ ยท ๐))) |
47 | 41, 43, 37, 44, 46 | syl13anc 1240 |
. . . . . . . . . 10
โข ((๐ โ โ โง (๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp)) โ (((๐ ยท ๐) + ๐) ยท ๐) = (((๐ ยท ๐) ยท ๐)(+gโ๐บ)(๐ ยท ๐))) |
48 | 40, 47 | eqtrd 2210 |
. . . . . . . . 9
โข ((๐ โ โ โง (๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp)) โ (((๐ + 1) ยท ๐) ยท ๐) = (((๐ ยท ๐) ยท ๐)(+gโ๐บ)(๐ ยท ๐))) |
49 | 26, 27, 45 | mulgnnp1 12990 |
. . . . . . . . . 10
โข ((๐ โ โ โง (๐ ยท ๐) โ ๐ต) โ ((๐ + 1) ยท (๐ ยท ๐)) = ((๐ ยท (๐ ยท ๐))(+gโ๐บ)(๐ ยท ๐))) |
50 | 30, 49 | sylan2 286 |
. . . . . . . . 9
โข ((๐ โ โ โง (๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp)) โ ((๐ + 1) ยท (๐ ยท ๐)) = ((๐ ยท (๐ ยท ๐))(+gโ๐บ)(๐ ยท ๐))) |
51 | 48, 50 | eqeq12d 2192 |
. . . . . . . 8
โข ((๐ โ โ โง (๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp)) โ ((((๐ + 1) ยท ๐) ยท ๐) = ((๐ + 1) ยท (๐ ยท ๐)) โ (((๐ ยท ๐) ยท ๐)(+gโ๐บ)(๐ ยท ๐)) = ((๐ ยท (๐ ยท ๐))(+gโ๐บ)(๐ ยท ๐)))) |
52 | 34, 51 | imbitrrid 156 |
. . . . . . 7
โข ((๐ โ โ โง (๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp)) โ (((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐)) โ (((๐ + 1) ยท ๐) ยท ๐) = ((๐ + 1) ยท (๐ ยท ๐)))) |
53 | 52 | ex 115 |
. . . . . 6
โข (๐ โ โ โ ((๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp) โ (((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐)) โ (((๐ + 1) ยท ๐) ยท ๐) = ((๐ + 1) ยท (๐ ยท ๐))))) |
54 | 53 | a2d 26 |
. . . . 5
โข (๐ โ โ โ (((๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp) โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐))) โ ((๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp) โ (((๐ + 1) ยท ๐) ยท ๐) = ((๐ + 1) ยท (๐ ยท ๐))))) |
55 | 5, 10, 15, 20, 33, 54 | nnind 8934 |
. . . 4
โข (๐ โ โ โ ((๐ โ โ โง ๐ โ ๐ต โง ๐บ โ Smgrp) โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐)))) |
56 | 55 | 3expd 1224 |
. . 3
โข (๐ โ โ โ (๐ โ โ โ (๐ โ ๐ต โ (๐บ โ Smgrp โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐)))))) |
57 | 56 | com4r 86 |
. 2
โข (๐บ โ Smgrp โ (๐ โ โ โ (๐ โ โ โ (๐ โ ๐ต โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐)))))) |
58 | 57 | 3imp2 1222 |
1
โข ((๐บ โ Smgrp โง (๐ โ โ โง ๐ โ โ โง ๐ โ ๐ต)) โ ((๐ ยท ๐) ยท ๐) = (๐ ยท (๐ ยท ๐))) |