Step |
Hyp |
Ref |
Expression |
1 |
|
ringinvnzdiv.b |
โข ๐ต = ( Base โ ๐
) |
2 |
|
ringinvnzdiv.t |
โข ยท = ( .r โ ๐
) |
3 |
|
ringinvnzdiv.u |
โข 1 = ( 1r โ ๐
) |
4 |
|
ringinvnzdiv.z |
โข 0 = ( 0g โ ๐
) |
5 |
|
ringinvnzdiv.r |
โข ( ๐ โ ๐
โ Ring ) |
6 |
|
ringinvnzdiv.x |
โข ( ๐ โ ๐ โ ๐ต ) |
7 |
|
ringinvnzdiv.a |
โข ( ๐ โ โ ๐ โ ๐ต ( ๐ ยท ๐ ) = 1 ) |
8 |
|
ringinvnzdiv.y |
โข ( ๐ โ ๐ โ ๐ต ) |
9 |
1 2 3
|
ringlidm |
โข ( ( ๐
โ Ring โง ๐ โ ๐ต ) โ ( 1 ยท ๐ ) = ๐ ) |
10 |
5 8 9
|
syl2anc |
โข ( ๐ โ ( 1 ยท ๐ ) = ๐ ) |
11 |
10
|
eqcomd |
โข ( ๐ โ ๐ = ( 1 ยท ๐ ) ) |
12 |
11
|
ad3antrrr |
โข ( ( ( ( ๐ โง ๐ โ ๐ต ) โง ( ๐ ยท ๐ ) = 1 ) โง ( ๐ ยท ๐ ) = 0 ) โ ๐ = ( 1 ยท ๐ ) ) |
13 |
|
oveq1 |
โข ( 1 = ( ๐ ยท ๐ ) โ ( 1 ยท ๐ ) = ( ( ๐ ยท ๐ ) ยท ๐ ) ) |
14 |
13
|
eqcoms |
โข ( ( ๐ ยท ๐ ) = 1 โ ( 1 ยท ๐ ) = ( ( ๐ ยท ๐ ) ยท ๐ ) ) |
15 |
14
|
adantl |
โข ( ( ( ๐ โง ๐ โ ๐ต ) โง ( ๐ ยท ๐ ) = 1 ) โ ( 1 ยท ๐ ) = ( ( ๐ ยท ๐ ) ยท ๐ ) ) |
16 |
5
|
adantr |
โข ( ( ๐ โง ๐ โ ๐ต ) โ ๐
โ Ring ) |
17 |
|
simpr |
โข ( ( ๐ โง ๐ โ ๐ต ) โ ๐ โ ๐ต ) |
18 |
6
|
adantr |
โข ( ( ๐ โง ๐ โ ๐ต ) โ ๐ โ ๐ต ) |
19 |
8
|
adantr |
โข ( ( ๐ โง ๐ โ ๐ต ) โ ๐ โ ๐ต ) |
20 |
17 18 19
|
3jca |
โข ( ( ๐ โง ๐ โ ๐ต ) โ ( ๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต ) ) |
21 |
16 20
|
jca |
โข ( ( ๐ โง ๐ โ ๐ต ) โ ( ๐
โ Ring โง ( ๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต ) ) ) |
22 |
21
|
adantr |
โข ( ( ( ๐ โง ๐ โ ๐ต ) โง ( ๐ ยท ๐ ) = 1 ) โ ( ๐
โ Ring โง ( ๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต ) ) ) |
23 |
1 2
|
ringass |
โข ( ( ๐
โ Ring โง ( ๐ โ ๐ต โง ๐ โ ๐ต โง ๐ โ ๐ต ) ) โ ( ( ๐ ยท ๐ ) ยท ๐ ) = ( ๐ ยท ( ๐ ยท ๐ ) ) ) |
24 |
22 23
|
syl |
โข ( ( ( ๐ โง ๐ โ ๐ต ) โง ( ๐ ยท ๐ ) = 1 ) โ ( ( ๐ ยท ๐ ) ยท ๐ ) = ( ๐ ยท ( ๐ ยท ๐ ) ) ) |
25 |
15 24
|
eqtrd |
โข ( ( ( ๐ โง ๐ โ ๐ต ) โง ( ๐ ยท ๐ ) = 1 ) โ ( 1 ยท ๐ ) = ( ๐ ยท ( ๐ ยท ๐ ) ) ) |
26 |
25
|
adantr |
โข ( ( ( ( ๐ โง ๐ โ ๐ต ) โง ( ๐ ยท ๐ ) = 1 ) โง ( ๐ ยท ๐ ) = 0 ) โ ( 1 ยท ๐ ) = ( ๐ ยท ( ๐ ยท ๐ ) ) ) |
27 |
|
oveq2 |
โข ( ( ๐ ยท ๐ ) = 0 โ ( ๐ ยท ( ๐ ยท ๐ ) ) = ( ๐ ยท 0 ) ) |
28 |
1 2 4
|
ringrz |
โข ( ( ๐
โ Ring โง ๐ โ ๐ต ) โ ( ๐ ยท 0 ) = 0 ) |
29 |
5 28
|
sylan |
โข ( ( ๐ โง ๐ โ ๐ต ) โ ( ๐ ยท 0 ) = 0 ) |
30 |
29
|
adantr |
โข ( ( ( ๐ โง ๐ โ ๐ต ) โง ( ๐ ยท ๐ ) = 1 ) โ ( ๐ ยท 0 ) = 0 ) |
31 |
27 30
|
sylan9eqr |
โข ( ( ( ( ๐ โง ๐ โ ๐ต ) โง ( ๐ ยท ๐ ) = 1 ) โง ( ๐ ยท ๐ ) = 0 ) โ ( ๐ ยท ( ๐ ยท ๐ ) ) = 0 ) |
32 |
12 26 31
|
3eqtrd |
โข ( ( ( ( ๐ โง ๐ โ ๐ต ) โง ( ๐ ยท ๐ ) = 1 ) โง ( ๐ ยท ๐ ) = 0 ) โ ๐ = 0 ) |
33 |
32
|
exp31 |
โข ( ( ๐ โง ๐ โ ๐ต ) โ ( ( ๐ ยท ๐ ) = 1 โ ( ( ๐ ยท ๐ ) = 0 โ ๐ = 0 ) ) ) |
34 |
33
|
rexlimdva |
โข ( ๐ โ ( โ ๐ โ ๐ต ( ๐ ยท ๐ ) = 1 โ ( ( ๐ ยท ๐ ) = 0 โ ๐ = 0 ) ) ) |
35 |
7 34
|
mpd |
โข ( ๐ โ ( ( ๐ ยท ๐ ) = 0 โ ๐ = 0 ) ) |
36 |
|
oveq2 |
โข ( ๐ = 0 โ ( ๐ ยท ๐ ) = ( ๐ ยท 0 ) ) |
37 |
1 2 4
|
ringrz |
โข ( ( ๐
โ Ring โง ๐ โ ๐ต ) โ ( ๐ ยท 0 ) = 0 ) |
38 |
5 6 37
|
syl2anc |
โข ( ๐ โ ( ๐ ยท 0 ) = 0 ) |
39 |
36 38
|
sylan9eqr |
โข ( ( ๐ โง ๐ = 0 ) โ ( ๐ ยท ๐ ) = 0 ) |
40 |
39
|
ex |
โข ( ๐ โ ( ๐ = 0 โ ( ๐ ยท ๐ ) = 0 ) ) |
41 |
35 40
|
impbid |
โข ( ๐ โ ( ( ๐ ยท ๐ ) = 0 โ ๐ = 0 ) ) |