Step |
Hyp |
Ref |
Expression |
1 |
|
mulgass.b |
โข ๐ต = ( Base โ ๐บ ) |
2 |
|
mulgass.t |
โข ยท = ( .g โ ๐บ ) |
3 |
|
mndsgrp |
โข ( ๐บ โ Mnd โ ๐บ โ Smgrp ) |
4 |
3
|
adantr |
โข ( ( ๐บ โ Mnd โง ( ๐ โ โ0 โง ๐ โ โ0 โง ๐ โ ๐ต ) ) โ ๐บ โ Smgrp ) |
5 |
4
|
adantr |
โข ( ( ( ๐บ โ Mnd โง ( ๐ โ โ0 โง ๐ โ โ0 โง ๐ โ ๐ต ) ) โง ( ๐ โ โ โง ๐ โ โ ) ) โ ๐บ โ Smgrp ) |
6 |
|
simprl |
โข ( ( ( ๐บ โ Mnd โง ( ๐ โ โ0 โง ๐ โ โ0 โง ๐ โ ๐ต ) ) โง ( ๐ โ โ โง ๐ โ โ ) ) โ ๐ โ โ ) |
7 |
|
simprr |
โข ( ( ( ๐บ โ Mnd โง ( ๐ โ โ0 โง ๐ โ โ0 โง ๐ โ ๐ต ) ) โง ( ๐ โ โ โง ๐ โ โ ) ) โ ๐ โ โ ) |
8 |
|
simpr3 |
โข ( ( ๐บ โ Mnd โง ( ๐ โ โ0 โง ๐ โ โ0 โง ๐ โ ๐ต ) ) โ ๐ โ ๐ต ) |
9 |
8
|
adantr |
โข ( ( ( ๐บ โ Mnd โง ( ๐ โ โ0 โง ๐ โ โ0 โง ๐ โ ๐ต ) ) โง ( ๐ โ โ โง ๐ โ โ ) ) โ ๐ โ ๐ต ) |
10 |
1 2
|
mulgnnass |
โข ( ( ๐บ โ Smgrp โง ( ๐ โ โ โง ๐ โ โ โง ๐ โ ๐ต ) ) โ ( ( ๐ ยท ๐ ) ยท ๐ ) = ( ๐ ยท ( ๐ ยท ๐ ) ) ) |
11 |
5 6 7 9 10
|
syl13anc |
โข ( ( ( ๐บ โ Mnd โง ( ๐ โ โ0 โง ๐ โ โ0 โง ๐ โ ๐ต ) ) โง ( ๐ โ โ โง ๐ โ โ ) ) โ ( ( ๐ ยท ๐ ) ยท ๐ ) = ( ๐ ยท ( ๐ ยท ๐ ) ) ) |
12 |
11
|
expr |
โข ( ( ( ๐บ โ Mnd โง ( ๐ โ โ0 โง ๐ โ โ0 โง ๐ โ ๐ต ) ) โง ๐ โ โ ) โ ( ๐ โ โ โ ( ( ๐ ยท ๐ ) ยท ๐ ) = ( ๐ ยท ( ๐ ยท ๐ ) ) ) ) |
13 |
|
eqid |
โข ( 0g โ ๐บ ) = ( 0g โ ๐บ ) |
14 |
1 13 2
|
mulg0 |
โข ( ๐ โ ๐ต โ ( 0 ยท ๐ ) = ( 0g โ ๐บ ) ) |
15 |
8 14
|
syl |
โข ( ( ๐บ โ Mnd โง ( ๐ โ โ0 โง ๐ โ โ0 โง ๐ โ ๐ต ) ) โ ( 0 ยท ๐ ) = ( 0g โ ๐บ ) ) |
16 |
|
simpr1 |
โข ( ( ๐บ โ Mnd โง ( ๐ โ โ0 โง ๐ โ โ0 โง ๐ โ ๐ต ) ) โ ๐ โ โ0 ) |
17 |
16
|
nn0cnd |
โข ( ( ๐บ โ Mnd โง ( ๐ โ โ0 โง ๐ โ โ0 โง ๐ โ ๐ต ) ) โ ๐ โ โ ) |
18 |
17
|
mul01d |
โข ( ( ๐บ โ Mnd โง ( ๐ โ โ0 โง ๐ โ โ0 โง ๐ โ ๐ต ) ) โ ( ๐ ยท 0 ) = 0 ) |
19 |
18
|
oveq1d |
โข ( ( ๐บ โ Mnd โง ( ๐ โ โ0 โง ๐ โ โ0 โง ๐ โ ๐ต ) ) โ ( ( ๐ ยท 0 ) ยท ๐ ) = ( 0 ยท ๐ ) ) |
20 |
15
|
oveq2d |
โข ( ( ๐บ โ Mnd โง ( ๐ โ โ0 โง ๐ โ โ0 โง ๐ โ ๐ต ) ) โ ( ๐ ยท ( 0 ยท ๐ ) ) = ( ๐ ยท ( 0g โ ๐บ ) ) ) |
21 |
1 2 13
|
mulgnn0z |
โข ( ( ๐บ โ Mnd โง ๐ โ โ0 ) โ ( ๐ ยท ( 0g โ ๐บ ) ) = ( 0g โ ๐บ ) ) |
22 |
21
|
3ad2antr1 |
โข ( ( ๐บ โ Mnd โง ( ๐ โ โ0 โง ๐ โ โ0 โง ๐ โ ๐ต ) ) โ ( ๐ ยท ( 0g โ ๐บ ) ) = ( 0g โ ๐บ ) ) |
23 |
20 22
|
eqtrd |
โข ( ( ๐บ โ Mnd โง ( ๐ โ โ0 โง ๐ โ โ0 โง ๐ โ ๐ต ) ) โ ( ๐ ยท ( 0 ยท ๐ ) ) = ( 0g โ ๐บ ) ) |
24 |
15 19 23
|
3eqtr4d |
โข ( ( ๐บ โ Mnd โง ( ๐ โ โ0 โง ๐ โ โ0 โง ๐ โ ๐ต ) ) โ ( ( ๐ ยท 0 ) ยท ๐ ) = ( ๐ ยท ( 0 ยท ๐ ) ) ) |
25 |
24
|
adantr |
โข ( ( ( ๐บ โ Mnd โง ( ๐ โ โ0 โง ๐ โ โ0 โง ๐ โ ๐ต ) ) โง ๐ โ โ ) โ ( ( ๐ ยท 0 ) ยท ๐ ) = ( ๐ ยท ( 0 ยท ๐ ) ) ) |
26 |
|
oveq2 |
โข ( ๐ = 0 โ ( ๐ ยท ๐ ) = ( ๐ ยท 0 ) ) |
27 |
26
|
oveq1d |
โข ( ๐ = 0 โ ( ( ๐ ยท ๐ ) ยท ๐ ) = ( ( ๐ ยท 0 ) ยท ๐ ) ) |
28 |
|
oveq1 |
โข ( ๐ = 0 โ ( ๐ ยท ๐ ) = ( 0 ยท ๐ ) ) |
29 |
28
|
oveq2d |
โข ( ๐ = 0 โ ( ๐ ยท ( ๐ ยท ๐ ) ) = ( ๐ ยท ( 0 ยท ๐ ) ) ) |
30 |
27 29
|
eqeq12d |
โข ( ๐ = 0 โ ( ( ( ๐ ยท ๐ ) ยท ๐ ) = ( ๐ ยท ( ๐ ยท ๐ ) ) โ ( ( ๐ ยท 0 ) ยท ๐ ) = ( ๐ ยท ( 0 ยท ๐ ) ) ) ) |
31 |
25 30
|
syl5ibrcom |
โข ( ( ( ๐บ โ Mnd โง ( ๐ โ โ0 โง ๐ โ โ0 โง ๐ โ ๐ต ) ) โง ๐ โ โ ) โ ( ๐ = 0 โ ( ( ๐ ยท ๐ ) ยท ๐ ) = ( ๐ ยท ( ๐ ยท ๐ ) ) ) ) |
32 |
|
simpr2 |
โข ( ( ๐บ โ Mnd โง ( ๐ โ โ0 โง ๐ โ โ0 โง ๐ โ ๐ต ) ) โ ๐ โ โ0 ) |
33 |
|
elnn0 |
โข ( ๐ โ โ0 โ ( ๐ โ โ โจ ๐ = 0 ) ) |
34 |
32 33
|
sylib |
โข ( ( ๐บ โ Mnd โง ( ๐ โ โ0 โง ๐ โ โ0 โง ๐ โ ๐ต ) ) โ ( ๐ โ โ โจ ๐ = 0 ) ) |
35 |
34
|
adantr |
โข ( ( ( ๐บ โ Mnd โง ( ๐ โ โ0 โง ๐ โ โ0 โง ๐ โ ๐ต ) ) โง ๐ โ โ ) โ ( ๐ โ โ โจ ๐ = 0 ) ) |
36 |
12 31 35
|
mpjaod |
โข ( ( ( ๐บ โ Mnd โง ( ๐ โ โ0 โง ๐ โ โ0 โง ๐ โ ๐ต ) ) โง ๐ โ โ ) โ ( ( ๐ ยท ๐ ) ยท ๐ ) = ( ๐ ยท ( ๐ ยท ๐ ) ) ) |
37 |
36
|
ex |
โข ( ( ๐บ โ Mnd โง ( ๐ โ โ0 โง ๐ โ โ0 โง ๐ โ ๐ต ) ) โ ( ๐ โ โ โ ( ( ๐ ยท ๐ ) ยท ๐ ) = ( ๐ ยท ( ๐ ยท ๐ ) ) ) ) |
38 |
32
|
nn0cnd |
โข ( ( ๐บ โ Mnd โง ( ๐ โ โ0 โง ๐ โ โ0 โง ๐ โ ๐ต ) ) โ ๐ โ โ ) |
39 |
38
|
mul02d |
โข ( ( ๐บ โ Mnd โง ( ๐ โ โ0 โง ๐ โ โ0 โง ๐ โ ๐ต ) ) โ ( 0 ยท ๐ ) = 0 ) |
40 |
39
|
oveq1d |
โข ( ( ๐บ โ Mnd โง ( ๐ โ โ0 โง ๐ โ โ0 โง ๐ โ ๐ต ) ) โ ( ( 0 ยท ๐ ) ยท ๐ ) = ( 0 ยท ๐ ) ) |
41 |
1 2
|
mulgnn0cl |
โข ( ( ๐บ โ Mnd โง ๐ โ โ0 โง ๐ โ ๐ต ) โ ( ๐ ยท ๐ ) โ ๐ต ) |
42 |
41
|
3adant3r1 |
โข ( ( ๐บ โ Mnd โง ( ๐ โ โ0 โง ๐ โ โ0 โง ๐ โ ๐ต ) ) โ ( ๐ ยท ๐ ) โ ๐ต ) |
43 |
1 13 2
|
mulg0 |
โข ( ( ๐ ยท ๐ ) โ ๐ต โ ( 0 ยท ( ๐ ยท ๐ ) ) = ( 0g โ ๐บ ) ) |
44 |
42 43
|
syl |
โข ( ( ๐บ โ Mnd โง ( ๐ โ โ0 โง ๐ โ โ0 โง ๐ โ ๐ต ) ) โ ( 0 ยท ( ๐ ยท ๐ ) ) = ( 0g โ ๐บ ) ) |
45 |
15 40 44
|
3eqtr4d |
โข ( ( ๐บ โ Mnd โง ( ๐ โ โ0 โง ๐ โ โ0 โง ๐ โ ๐ต ) ) โ ( ( 0 ยท ๐ ) ยท ๐ ) = ( 0 ยท ( ๐ ยท ๐ ) ) ) |
46 |
|
oveq1 |
โข ( ๐ = 0 โ ( ๐ ยท ๐ ) = ( 0 ยท ๐ ) ) |
47 |
46
|
oveq1d |
โข ( ๐ = 0 โ ( ( ๐ ยท ๐ ) ยท ๐ ) = ( ( 0 ยท ๐ ) ยท ๐ ) ) |
48 |
|
oveq1 |
โข ( ๐ = 0 โ ( ๐ ยท ( ๐ ยท ๐ ) ) = ( 0 ยท ( ๐ ยท ๐ ) ) ) |
49 |
47 48
|
eqeq12d |
โข ( ๐ = 0 โ ( ( ( ๐ ยท ๐ ) ยท ๐ ) = ( ๐ ยท ( ๐ ยท ๐ ) ) โ ( ( 0 ยท ๐ ) ยท ๐ ) = ( 0 ยท ( ๐ ยท ๐ ) ) ) ) |
50 |
45 49
|
syl5ibrcom |
โข ( ( ๐บ โ Mnd โง ( ๐ โ โ0 โง ๐ โ โ0 โง ๐ โ ๐ต ) ) โ ( ๐ = 0 โ ( ( ๐ ยท ๐ ) ยท ๐ ) = ( ๐ ยท ( ๐ ยท ๐ ) ) ) ) |
51 |
|
elnn0 |
โข ( ๐ โ โ0 โ ( ๐ โ โ โจ ๐ = 0 ) ) |
52 |
16 51
|
sylib |
โข ( ( ๐บ โ Mnd โง ( ๐ โ โ0 โง ๐ โ โ0 โง ๐ โ ๐ต ) ) โ ( ๐ โ โ โจ ๐ = 0 ) ) |
53 |
37 50 52
|
mpjaod |
โข ( ( ๐บ โ Mnd โง ( ๐ โ โ0 โง ๐ โ โ0 โง ๐ โ ๐ต ) ) โ ( ( ๐ ยท ๐ ) ยท ๐ ) = ( ๐ ยท ( ๐ ยท ๐ ) ) ) |