Step | Hyp | Ref
| Expression |
1 | | rngabl 46637 |
. . . . . . 7
โข (๐
โ Rng โ ๐
โ Abel) |
2 | | ablgrp 19647 |
. . . . . . 7
โข (๐
โ Abel โ ๐
โ Grp) |
3 | 1, 2 | syl 17 |
. . . . . 6
โข (๐
โ Rng โ ๐
โ Grp) |
4 | | rngcl.b |
. . . . . . 7
โข ๐ต = (Baseโ๐
) |
5 | | rnglz.z |
. . . . . . 7
โข 0 =
(0gโ๐
) |
6 | 4, 5 | grpidcl 18846 |
. . . . . 6
โข (๐
โ Grp โ 0 โ ๐ต) |
7 | | eqid 2732 |
. . . . . . 7
โข
(+gโ๐
) = (+gโ๐
) |
8 | 4, 7, 5 | grplid 18848 |
. . . . . 6
โข ((๐
โ Grp โง 0 โ ๐ต) โ ( 0 (+gโ๐
) 0 ) = 0 ) |
9 | 3, 6, 8 | syl2anc2 585 |
. . . . 5
โข (๐
โ Rng โ ( 0
(+gโ๐
)
0 ) =
0
) |
10 | 9 | adantr 481 |
. . . 4
โข ((๐
โ Rng โง ๐ โ ๐ต) โ ( 0 (+gโ๐
) 0 ) = 0 ) |
11 | 10 | oveq1d 7420 |
. . 3
โข ((๐
โ Rng โง ๐ โ ๐ต) โ (( 0 (+gโ๐
) 0 ) ยท ๐) = ( 0 ยท ๐)) |
12 | | simpl 483 |
. . . 4
โข ((๐
โ Rng โง ๐ โ ๐ต) โ ๐
โ Rng) |
13 | 3, 6 | syl 17 |
. . . . . . 7
โข (๐
โ Rng โ 0 โ ๐ต) |
14 | 13, 13 | jca 512 |
. . . . . 6
โข (๐
โ Rng โ ( 0 โ ๐ต โง 0 โ ๐ต)) |
15 | 14 | anim1i 615 |
. . . . 5
โข ((๐
โ Rng โง ๐ โ ๐ต) โ (( 0 โ ๐ต โง 0 โ ๐ต) โง ๐ โ ๐ต)) |
16 | | df-3an 1089 |
. . . . 5
โข (( 0 โ ๐ต โง 0 โ ๐ต โง ๐ โ ๐ต) โ (( 0 โ ๐ต โง 0 โ ๐ต) โง ๐ โ ๐ต)) |
17 | 15, 16 | sylibr 233 |
. . . 4
โข ((๐
โ Rng โง ๐ โ ๐ต) โ ( 0 โ ๐ต โง 0 โ ๐ต โง ๐ โ ๐ต)) |
18 | | rngcl.t |
. . . . 5
โข ยท =
(.rโ๐
) |
19 | 4, 7, 18 | rngdir 46646 |
. . . 4
โข ((๐
โ Rng โง ( 0 โ ๐ต โง 0 โ ๐ต โง ๐ โ ๐ต)) โ (( 0 (+gโ๐
) 0 ) ยท ๐) = (( 0 ยท ๐)(+gโ๐
)( 0 ยท ๐))) |
20 | 12, 17, 19 | syl2anc 584 |
. . 3
โข ((๐
โ Rng โง ๐ โ ๐ต) โ (( 0 (+gโ๐
) 0 ) ยท ๐) = (( 0 ยท ๐)(+gโ๐
)( 0 ยท ๐))) |
21 | 3 | adantr 481 |
. . . 4
โข ((๐
โ Rng โง ๐ โ ๐ต) โ ๐
โ Grp) |
22 | 13 | adantr 481 |
. . . . 5
โข ((๐
โ Rng โง ๐ โ ๐ต) โ 0 โ ๐ต) |
23 | | simpr 485 |
. . . . 5
โข ((๐
โ Rng โง ๐ โ ๐ต) โ ๐ โ ๐ต) |
24 | 4, 18 | rngcl 46649 |
. . . . 5
โข ((๐
โ Rng โง 0 โ ๐ต โง ๐ โ ๐ต) โ ( 0 ยท ๐) โ ๐ต) |
25 | 12, 22, 23, 24 | syl3anc 1371 |
. . . 4
โข ((๐
โ Rng โง ๐ โ ๐ต) โ ( 0 ยท ๐) โ ๐ต) |
26 | 4, 7, 5 | grprid 18849 |
. . . . 5
โข ((๐
โ Grp โง ( 0 ยท ๐) โ ๐ต) โ (( 0 ยท ๐)(+gโ๐
) 0 ) = ( 0 ยท ๐)) |
27 | 26 | eqcomd 2738 |
. . . 4
โข ((๐
โ Grp โง ( 0 ยท ๐) โ ๐ต) โ ( 0 ยท ๐) = (( 0 ยท ๐)(+gโ๐
) 0 )) |
28 | 21, 25, 27 | syl2anc 584 |
. . 3
โข ((๐
โ Rng โง ๐ โ ๐ต) โ ( 0 ยท ๐) = (( 0 ยท ๐)(+gโ๐
) 0 )) |
29 | 11, 20, 28 | 3eqtr3d 2780 |
. 2
โข ((๐
โ Rng โง ๐ โ ๐ต) โ (( 0 ยท ๐)(+gโ๐
)( 0 ยท ๐)) = (( 0 ยท ๐)(+gโ๐
) 0 )) |
30 | 4, 7 | grplcan 18881 |
. . 3
โข ((๐
โ Grp โง (( 0 ยท ๐) โ ๐ต โง 0 โ ๐ต โง ( 0 ยท ๐) โ ๐ต)) โ ((( 0 ยท ๐)(+gโ๐
)( 0 ยท ๐)) = (( 0 ยท ๐)(+gโ๐
) 0 ) โ ( 0 ยท ๐) = 0 )) |
31 | 21, 25, 22, 25, 30 | syl13anc 1372 |
. 2
โข ((๐
โ Rng โง ๐ โ ๐ต) โ ((( 0 ยท ๐)(+gโ๐
)( 0 ยท ๐)) = (( 0 ยท ๐)(+gโ๐
) 0 ) โ ( 0 ยท ๐) = 0 )) |
32 | 29, 31 | mpbid 231 |
1
โข ((๐
โ Rng โง ๐ โ ๐ต) โ ( 0 ยท ๐) = 0 ) |