Step | Hyp | Ref
| Expression |
1 | | df-ne 2941 |
. . 3
โข (๐ด โ 0 โ ยฌ ๐ด = 0) |
2 | | ax-rrecex 11131 |
. . . . 5
โข ((๐ด โ โ โง ๐ด โ 0) โ โ๐ฅ โ โ (๐ด ยท ๐ฅ) = 1) |
3 | | simpll 766 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ฅ โ โ โง (๐ด ยท ๐ฅ) = 1)) โ ๐ด โ โ) |
4 | 3 | recnd 11191 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ฅ โ โ โง (๐ด ยท ๐ฅ) = 1)) โ ๐ด โ โ) |
5 | | simprl 770 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ฅ โ โ โง (๐ด ยท ๐ฅ) = 1)) โ ๐ฅ โ โ) |
6 | 5 | recnd 11191 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ฅ โ โ โง (๐ด ยท ๐ฅ) = 1)) โ ๐ฅ โ โ) |
7 | 4, 6, 4 | mulassd 11186 |
. . . . . 6
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ฅ โ โ โง (๐ด ยท ๐ฅ) = 1)) โ ((๐ด ยท ๐ฅ) ยท ๐ด) = (๐ด ยท (๐ฅ ยท ๐ด))) |
8 | | simprr 772 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ฅ โ โ โง (๐ด ยท ๐ฅ) = 1)) โ (๐ด ยท ๐ฅ) = 1) |
9 | 8 | oveq1d 7376 |
. . . . . 6
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ฅ โ โ โง (๐ด ยท ๐ฅ) = 1)) โ ((๐ด ยท ๐ฅ) ยท ๐ด) = (1 ยท ๐ด)) |
10 | 3, 5, 8 | remulinvcom 40948 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ฅ โ โ โง (๐ด ยท ๐ฅ) = 1)) โ (๐ฅ ยท ๐ด) = 1) |
11 | 10 | oveq2d 7377 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ฅ โ โ โง (๐ด ยท ๐ฅ) = 1)) โ (๐ด ยท (๐ฅ ยท ๐ด)) = (๐ด ยท 1)) |
12 | | ax-1rid 11129 |
. . . . . . . 8
โข (๐ด โ โ โ (๐ด ยท 1) = ๐ด) |
13 | 3, 12 | syl 17 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ฅ โ โ โง (๐ด ยท ๐ฅ) = 1)) โ (๐ด ยท 1) = ๐ด) |
14 | 11, 13 | eqtrd 2773 |
. . . . . 6
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ฅ โ โ โง (๐ด ยท ๐ฅ) = 1)) โ (๐ด ยท (๐ฅ ยท ๐ด)) = ๐ด) |
15 | 7, 9, 14 | 3eqtr3d 2781 |
. . . . 5
โข (((๐ด โ โ โง ๐ด โ 0) โง (๐ฅ โ โ โง (๐ด ยท ๐ฅ) = 1)) โ (1 ยท ๐ด) = ๐ด) |
16 | 2, 15 | rexlimddv 3155 |
. . . 4
โข ((๐ด โ โ โง ๐ด โ 0) โ (1 ยท
๐ด) = ๐ด) |
17 | 16 | ex 414 |
. . 3
โข (๐ด โ โ โ (๐ด โ 0 โ (1 ยท ๐ด) = ๐ด)) |
18 | 1, 17 | biimtrrid 242 |
. 2
โข (๐ด โ โ โ (ยฌ
๐ด = 0 โ (1 ยท
๐ด) = ๐ด)) |
19 | | 1re 11163 |
. . . 4
โข 1 โ
โ |
20 | | remul01 40923 |
. . . 4
โข (1 โ
โ โ (1 ยท 0) = 0) |
21 | 19, 20 | mp1i 13 |
. . 3
โข (๐ด = 0 โ (1 ยท 0) =
0) |
22 | | oveq2 7369 |
. . 3
โข (๐ด = 0 โ (1 ยท ๐ด) = (1 ยท
0)) |
23 | | id 22 |
. . 3
โข (๐ด = 0 โ ๐ด = 0) |
24 | 21, 22, 23 | 3eqtr4d 2783 |
. 2
โข (๐ด = 0 โ (1 ยท ๐ด) = ๐ด) |
25 | 18, 24 | pm2.61d2 181 |
1
โข (๐ด โ โ โ (1
ยท ๐ด) = ๐ด) |