Step | Hyp | Ref
| Expression |
1 | | ringgrp 13189 |
. . . . . 6
โข (๐
โ Ring โ ๐
โ Grp) |
2 | | rngz.b |
. . . . . . 7
โข ๐ต = (Baseโ๐
) |
3 | | rngz.z |
. . . . . . 7
โข 0 =
(0gโ๐
) |
4 | 2, 3 | grpidcl 12909 |
. . . . . 6
โข (๐
โ Grp โ 0 โ ๐ต) |
5 | | eqid 2177 |
. . . . . . 7
โข
(+gโ๐
) = (+gโ๐
) |
6 | 2, 5, 3 | grplid 12911 |
. . . . . 6
โข ((๐
โ Grp โง 0 โ ๐ต) โ ( 0 (+gโ๐
) 0 ) = 0 ) |
7 | 1, 4, 6 | syl2anc2 412 |
. . . . 5
โข (๐
โ Ring โ ( 0
(+gโ๐
)
0 ) =
0
) |
8 | 7 | adantr 276 |
. . . 4
โข ((๐
โ Ring โง ๐ โ ๐ต) โ ( 0 (+gโ๐
) 0 ) = 0 ) |
9 | 8 | oveq1d 5892 |
. . 3
โข ((๐
โ Ring โง ๐ โ ๐ต) โ (( 0 (+gโ๐
) 0 ) ยท ๐) = ( 0 ยท ๐)) |
10 | 1, 4 | syl 14 |
. . . . . 6
โข (๐
โ Ring โ 0 โ ๐ต) |
11 | 10 | adantr 276 |
. . . . 5
โข ((๐
โ Ring โง ๐ โ ๐ต) โ 0 โ ๐ต) |
12 | | simpr 110 |
. . . . 5
โข ((๐
โ Ring โง ๐ โ ๐ต) โ ๐ โ ๐ต) |
13 | 11, 11, 12 | 3jca 1177 |
. . . 4
โข ((๐
โ Ring โง ๐ โ ๐ต) โ ( 0 โ ๐ต โง 0 โ ๐ต โง ๐ โ ๐ต)) |
14 | | rngz.t |
. . . . 5
โข ยท =
(.rโ๐
) |
15 | 2, 5, 14 | ringdir 13207 |
. . . 4
โข ((๐
โ Ring โง ( 0 โ ๐ต โง 0 โ ๐ต โง ๐ โ ๐ต)) โ (( 0 (+gโ๐
) 0 ) ยท ๐) = (( 0 ยท ๐)(+gโ๐
)( 0 ยท ๐))) |
16 | 13, 15 | syldan 282 |
. . 3
โข ((๐
โ Ring โง ๐ โ ๐ต) โ (( 0 (+gโ๐
) 0 ) ยท ๐) = (( 0 ยท ๐)(+gโ๐
)( 0 ยท ๐))) |
17 | 1 | adantr 276 |
. . . 4
โข ((๐
โ Ring โง ๐ โ ๐ต) โ ๐
โ Grp) |
18 | | simpl 109 |
. . . . 5
โข ((๐
โ Ring โง ๐ โ ๐ต) โ ๐
โ Ring) |
19 | 2, 14 | ringcl 13201 |
. . . . 5
โข ((๐
โ Ring โง 0 โ ๐ต โง ๐ โ ๐ต) โ ( 0 ยท ๐) โ ๐ต) |
20 | 18, 11, 12, 19 | syl3anc 1238 |
. . . 4
โข ((๐
โ Ring โง ๐ โ ๐ต) โ ( 0 ยท ๐) โ ๐ต) |
21 | 2, 5, 3 | grprid 12912 |
. . . . 5
โข ((๐
โ Grp โง ( 0 ยท ๐) โ ๐ต) โ (( 0 ยท ๐)(+gโ๐
) 0 ) = ( 0 ยท ๐)) |
22 | 21 | eqcomd 2183 |
. . . 4
โข ((๐
โ Grp โง ( 0 ยท ๐) โ ๐ต) โ ( 0 ยท ๐) = (( 0 ยท ๐)(+gโ๐
) 0 )) |
23 | 17, 20, 22 | syl2anc 411 |
. . 3
โข ((๐
โ Ring โง ๐ โ ๐ต) โ ( 0 ยท ๐) = (( 0 ยท ๐)(+gโ๐
) 0 )) |
24 | 9, 16, 23 | 3eqtr3d 2218 |
. 2
โข ((๐
โ Ring โง ๐ โ ๐ต) โ (( 0 ยท ๐)(+gโ๐
)( 0 ยท ๐)) = (( 0 ยท ๐)(+gโ๐
) 0 )) |
25 | 2, 5 | grplcan 12937 |
. . 3
โข ((๐
โ Grp โง (( 0 ยท ๐) โ ๐ต โง 0 โ ๐ต โง ( 0 ยท ๐) โ ๐ต)) โ ((( 0 ยท ๐)(+gโ๐
)( 0 ยท ๐)) = (( 0 ยท ๐)(+gโ๐
) 0 ) โ ( 0 ยท ๐) = 0 )) |
26 | 17, 20, 11, 20, 25 | syl13anc 1240 |
. 2
โข ((๐
โ Ring โง ๐ โ ๐ต) โ ((( 0 ยท ๐)(+gโ๐
)( 0 ยท ๐)) = (( 0 ยท ๐)(+gโ๐
) 0 ) โ ( 0 ยท ๐) = 0 )) |
27 | 24, 26 | mpbid 147 |
1
โข ((๐
โ Ring โง ๐ โ ๐ต) โ ( 0 ยท ๐) = 0 ) |