Step |
Hyp |
Ref |
Expression |
1 |
|
ringz.b |
โข ๐ต = ( Base โ ๐
) |
2 |
|
ringz.t |
โข ยท = ( .r โ ๐
) |
3 |
|
ringz.z |
โข 0 = ( 0g โ ๐
) |
4 |
|
ringgrp |
โข ( ๐
โ Ring โ ๐
โ Grp ) |
5 |
1 3
|
grpidcl |
โข ( ๐
โ Grp โ 0 โ ๐ต ) |
6 |
|
eqid |
โข ( +g โ ๐
) = ( +g โ ๐
) |
7 |
1 6 3
|
grplid |
โข ( ( ๐
โ Grp โง 0 โ ๐ต ) โ ( 0 ( +g โ ๐
) 0 ) = 0 ) |
8 |
4 5 7
|
syl2anc2 |
โข ( ๐
โ Ring โ ( 0 ( +g โ ๐
) 0 ) = 0 ) |
9 |
8
|
adantr |
โข ( ( ๐
โ Ring โง ๐ โ ๐ต ) โ ( 0 ( +g โ ๐
) 0 ) = 0 ) |
10 |
9
|
oveq2d |
โข ( ( ๐
โ Ring โง ๐ โ ๐ต ) โ ( ๐ ยท ( 0 ( +g โ ๐
) 0 ) ) = ( ๐ ยท 0 ) ) |
11 |
|
simpr |
โข ( ( ๐
โ Ring โง ๐ โ ๐ต ) โ ๐ โ ๐ต ) |
12 |
4 5
|
syl |
โข ( ๐
โ Ring โ 0 โ ๐ต ) |
13 |
12
|
adantr |
โข ( ( ๐
โ Ring โง ๐ โ ๐ต ) โ 0 โ ๐ต ) |
14 |
11 13 13
|
3jca |
โข ( ( ๐
โ Ring โง ๐ โ ๐ต ) โ ( ๐ โ ๐ต โง 0 โ ๐ต โง 0 โ ๐ต ) ) |
15 |
1 6 2
|
ringdi |
โข ( ( ๐
โ Ring โง ( ๐ โ ๐ต โง 0 โ ๐ต โง 0 โ ๐ต ) ) โ ( ๐ ยท ( 0 ( +g โ ๐
) 0 ) ) = ( ( ๐ ยท 0 ) ( +g โ ๐
) ( ๐ ยท 0 ) ) ) |
16 |
14 15
|
syldan |
โข ( ( ๐
โ Ring โง ๐ โ ๐ต ) โ ( ๐ ยท ( 0 ( +g โ ๐
) 0 ) ) = ( ( ๐ ยท 0 ) ( +g โ ๐
) ( ๐ ยท 0 ) ) ) |
17 |
4
|
adantr |
โข ( ( ๐
โ Ring โง ๐ โ ๐ต ) โ ๐
โ Grp ) |
18 |
1 2
|
ringcl |
โข ( ( ๐
โ Ring โง ๐ โ ๐ต โง 0 โ ๐ต ) โ ( ๐ ยท 0 ) โ ๐ต ) |
19 |
13 18
|
mpd3an3 |
โข ( ( ๐
โ Ring โง ๐ โ ๐ต ) โ ( ๐ ยท 0 ) โ ๐ต ) |
20 |
1 6 3
|
grplid |
โข ( ( ๐
โ Grp โง ( ๐ ยท 0 ) โ ๐ต ) โ ( 0 ( +g โ ๐
) ( ๐ ยท 0 ) ) = ( ๐ ยท 0 ) ) |
21 |
20
|
eqcomd |
โข ( ( ๐
โ Grp โง ( ๐ ยท 0 ) โ ๐ต ) โ ( ๐ ยท 0 ) = ( 0 ( +g โ ๐
) ( ๐ ยท 0 ) ) ) |
22 |
17 19 21
|
syl2anc |
โข ( ( ๐
โ Ring โง ๐ โ ๐ต ) โ ( ๐ ยท 0 ) = ( 0 ( +g โ ๐
) ( ๐ ยท 0 ) ) ) |
23 |
10 16 22
|
3eqtr3d |
โข ( ( ๐
โ Ring โง ๐ โ ๐ต ) โ ( ( ๐ ยท 0 ) ( +g โ ๐
) ( ๐ ยท 0 ) ) = ( 0 ( +g โ ๐
) ( ๐ ยท 0 ) ) ) |
24 |
1 6
|
grprcan |
โข ( ( ๐
โ Grp โง ( ( ๐ ยท 0 ) โ ๐ต โง 0 โ ๐ต โง ( ๐ ยท 0 ) โ ๐ต ) ) โ ( ( ( ๐ ยท 0 ) ( +g โ ๐
) ( ๐ ยท 0 ) ) = ( 0 ( +g โ ๐
) ( ๐ ยท 0 ) ) โ ( ๐ ยท 0 ) = 0 ) ) |
25 |
17 19 13 19 24
|
syl13anc |
โข ( ( ๐
โ Ring โง ๐ โ ๐ต ) โ ( ( ( ๐ ยท 0 ) ( +g โ ๐
) ( ๐ ยท 0 ) ) = ( 0 ( +g โ ๐
) ( ๐ ยท 0 ) ) โ ( ๐ ยท 0 ) = 0 ) ) |
26 |
23 25
|
mpbid |
โข ( ( ๐
โ Ring โง ๐ โ ๐ต ) โ ( ๐ ยท 0 ) = 0 ) |