Step | Hyp | Ref
| Expression |
1 | | 0re 11164 |
. . . . 5
โข 0 โ
โ |
2 | | remulcl 11143 |
. . . . 5
โข ((0
โ โ โง ๐ด
โ โ) โ (0 ยท ๐ด) โ โ) |
3 | 1, 2 | mpan 689 |
. . . 4
โข (๐ด โ โ โ (0
ยท ๐ด) โ
โ) |
4 | | ax-rrecex 11130 |
. . . 4
โข (((0
ยท ๐ด) โ โ
โง (0 ยท ๐ด) โ
0) โ โ๐ฆ โ
โ ((0 ยท ๐ด)
ยท ๐ฆ) =
1) |
5 | 3, 4 | sylan 581 |
. . 3
โข ((๐ด โ โ โง (0
ยท ๐ด) โ 0) โ
โ๐ฆ โ โ ((0
ยท ๐ด) ยท ๐ฆ) = 1) |
6 | 5 | adantr 482 |
. 2
โข (((๐ด โ โ โง (0
ยท ๐ด) โ 0) โง
๐ต โ โ) โ
โ๐ฆ โ โ ((0
ยท ๐ด) ยท ๐ฆ) = 1) |
7 | | 00id 11337 |
. . . . 5
โข (0 + 0) =
0 |
8 | 7 | oveq2i 7373 |
. . . 4
โข (((๐ฆ ยท ๐ด) ยท ๐ต) ยท (0 + 0)) = (((๐ฆ ยท ๐ด) ยท ๐ต) ยท 0) |
9 | 8 | eqcomi 2746 |
. . 3
โข (((๐ฆ ยท ๐ด) ยท ๐ต) ยท 0) = (((๐ฆ ยท ๐ด) ยท ๐ต) ยท (0 + 0)) |
10 | | simprl 770 |
. . . . . . 7
โข ((((๐ด โ โ โง (0
ยท ๐ด) โ 0) โง
๐ต โ โ) โง
(๐ฆ โ โ โง ((0
ยท ๐ด) ยท ๐ฆ) = 1)) โ ๐ฆ โ
โ) |
11 | 10 | recnd 11190 |
. . . . . 6
โข ((((๐ด โ โ โง (0
ยท ๐ด) โ 0) โง
๐ต โ โ) โง
(๐ฆ โ โ โง ((0
ยท ๐ด) ยท ๐ฆ) = 1)) โ ๐ฆ โ
โ) |
12 | | simplll 774 |
. . . . . . 7
โข ((((๐ด โ โ โง (0
ยท ๐ด) โ 0) โง
๐ต โ โ) โง
(๐ฆ โ โ โง ((0
ยท ๐ด) ยท ๐ฆ) = 1)) โ ๐ด โ โ) |
13 | 12 | recnd 11190 |
. . . . . 6
โข ((((๐ด โ โ โง (0
ยท ๐ด) โ 0) โง
๐ต โ โ) โง
(๐ฆ โ โ โง ((0
ยท ๐ด) ยท ๐ฆ) = 1)) โ ๐ด โ โ) |
14 | 11, 13 | mulcld 11182 |
. . . . 5
โข ((((๐ด โ โ โง (0
ยท ๐ด) โ 0) โง
๐ต โ โ) โง
(๐ฆ โ โ โง ((0
ยท ๐ด) ยท ๐ฆ) = 1)) โ (๐ฆ ยท ๐ด) โ โ) |
15 | | simplr 768 |
. . . . 5
โข ((((๐ด โ โ โง (0
ยท ๐ด) โ 0) โง
๐ต โ โ) โง
(๐ฆ โ โ โง ((0
ยท ๐ด) ยท ๐ฆ) = 1)) โ ๐ต โ โ) |
16 | | 0cn 11154 |
. . . . . 6
โข 0 โ
โ |
17 | | mul32 11328 |
. . . . . 6
โข (((๐ฆ ยท ๐ด) โ โ โง ๐ต โ โ โง 0 โ โ)
โ (((๐ฆ ยท ๐ด) ยท ๐ต) ยท 0) = (((๐ฆ ยท ๐ด) ยท 0) ยท ๐ต)) |
18 | 16, 17 | mp3an3 1451 |
. . . . 5
โข (((๐ฆ ยท ๐ด) โ โ โง ๐ต โ โ) โ (((๐ฆ ยท ๐ด) ยท ๐ต) ยท 0) = (((๐ฆ ยท ๐ด) ยท 0) ยท ๐ต)) |
19 | 14, 15, 18 | syl2anc 585 |
. . . 4
โข ((((๐ด โ โ โง (0
ยท ๐ด) โ 0) โง
๐ต โ โ) โง
(๐ฆ โ โ โง ((0
ยท ๐ด) ยท ๐ฆ) = 1)) โ (((๐ฆ ยท ๐ด) ยท ๐ต) ยท 0) = (((๐ฆ ยท ๐ด) ยท 0) ยท ๐ต)) |
20 | | mul31 11329 |
. . . . . . . . 9
โข ((๐ฆ โ โ โง ๐ด โ โ โง 0 โ
โ) โ ((๐ฆ
ยท ๐ด) ยท 0) =
((0 ยท ๐ด) ยท
๐ฆ)) |
21 | 16, 20 | mp3an3 1451 |
. . . . . . . 8
โข ((๐ฆ โ โ โง ๐ด โ โ) โ ((๐ฆ ยท ๐ด) ยท 0) = ((0 ยท ๐ด) ยท ๐ฆ)) |
22 | 11, 13, 21 | syl2anc 585 |
. . . . . . 7
โข ((((๐ด โ โ โง (0
ยท ๐ด) โ 0) โง
๐ต โ โ) โง
(๐ฆ โ โ โง ((0
ยท ๐ด) ยท ๐ฆ) = 1)) โ ((๐ฆ ยท ๐ด) ยท 0) = ((0 ยท ๐ด) ยท ๐ฆ)) |
23 | | simprr 772 |
. . . . . . 7
โข ((((๐ด โ โ โง (0
ยท ๐ด) โ 0) โง
๐ต โ โ) โง
(๐ฆ โ โ โง ((0
ยท ๐ด) ยท ๐ฆ) = 1)) โ ((0 ยท
๐ด) ยท ๐ฆ) = 1) |
24 | 22, 23 | eqtrd 2777 |
. . . . . 6
โข ((((๐ด โ โ โง (0
ยท ๐ด) โ 0) โง
๐ต โ โ) โง
(๐ฆ โ โ โง ((0
ยท ๐ด) ยท ๐ฆ) = 1)) โ ((๐ฆ ยท ๐ด) ยท 0) = 1) |
25 | 24 | oveq1d 7377 |
. . . . 5
โข ((((๐ด โ โ โง (0
ยท ๐ด) โ 0) โง
๐ต โ โ) โง
(๐ฆ โ โ โง ((0
ยท ๐ด) ยท ๐ฆ) = 1)) โ (((๐ฆ ยท ๐ด) ยท 0) ยท ๐ต) = (1 ยท ๐ต)) |
26 | | mulid2 11161 |
. . . . . 6
โข (๐ต โ โ โ (1
ยท ๐ต) = ๐ต) |
27 | 26 | ad2antlr 726 |
. . . . 5
โข ((((๐ด โ โ โง (0
ยท ๐ด) โ 0) โง
๐ต โ โ) โง
(๐ฆ โ โ โง ((0
ยท ๐ด) ยท ๐ฆ) = 1)) โ (1 ยท ๐ต) = ๐ต) |
28 | 25, 27 | eqtrd 2777 |
. . . 4
โข ((((๐ด โ โ โง (0
ยท ๐ด) โ 0) โง
๐ต โ โ) โง
(๐ฆ โ โ โง ((0
ยท ๐ด) ยท ๐ฆ) = 1)) โ (((๐ฆ ยท ๐ด) ยท 0) ยท ๐ต) = ๐ต) |
29 | 19, 28 | eqtrd 2777 |
. . 3
โข ((((๐ด โ โ โง (0
ยท ๐ด) โ 0) โง
๐ต โ โ) โง
(๐ฆ โ โ โง ((0
ยท ๐ด) ยท ๐ฆ) = 1)) โ (((๐ฆ ยท ๐ด) ยท ๐ต) ยท 0) = ๐ต) |
30 | 14, 15 | mulcld 11182 |
. . . . 5
โข ((((๐ด โ โ โง (0
ยท ๐ด) โ 0) โง
๐ต โ โ) โง
(๐ฆ โ โ โง ((0
ยท ๐ด) ยท ๐ฆ) = 1)) โ ((๐ฆ ยท ๐ด) ยท ๐ต) โ โ) |
31 | | adddi 11147 |
. . . . . 6
โข ((((๐ฆ ยท ๐ด) ยท ๐ต) โ โ โง 0 โ โ
โง 0 โ โ) โ (((๐ฆ ยท ๐ด) ยท ๐ต) ยท (0 + 0)) = ((((๐ฆ ยท ๐ด) ยท ๐ต) ยท 0) + (((๐ฆ ยท ๐ด) ยท ๐ต) ยท 0))) |
32 | 16, 16, 31 | mp3an23 1454 |
. . . . 5
โข (((๐ฆ ยท ๐ด) ยท ๐ต) โ โ โ (((๐ฆ ยท ๐ด) ยท ๐ต) ยท (0 + 0)) = ((((๐ฆ ยท ๐ด) ยท ๐ต) ยท 0) + (((๐ฆ ยท ๐ด) ยท ๐ต) ยท 0))) |
33 | 30, 32 | syl 17 |
. . . 4
โข ((((๐ด โ โ โง (0
ยท ๐ด) โ 0) โง
๐ต โ โ) โง
(๐ฆ โ โ โง ((0
ยท ๐ด) ยท ๐ฆ) = 1)) โ (((๐ฆ ยท ๐ด) ยท ๐ต) ยท (0 + 0)) = ((((๐ฆ ยท ๐ด) ยท ๐ต) ยท 0) + (((๐ฆ ยท ๐ด) ยท ๐ต) ยท 0))) |
34 | 29, 29 | oveq12d 7380 |
. . . 4
โข ((((๐ด โ โ โง (0
ยท ๐ด) โ 0) โง
๐ต โ โ) โง
(๐ฆ โ โ โง ((0
ยท ๐ด) ยท ๐ฆ) = 1)) โ ((((๐ฆ ยท ๐ด) ยท ๐ต) ยท 0) + (((๐ฆ ยท ๐ด) ยท ๐ต) ยท 0)) = (๐ต + ๐ต)) |
35 | 33, 34 | eqtrd 2777 |
. . 3
โข ((((๐ด โ โ โง (0
ยท ๐ด) โ 0) โง
๐ต โ โ) โง
(๐ฆ โ โ โง ((0
ยท ๐ด) ยท ๐ฆ) = 1)) โ (((๐ฆ ยท ๐ด) ยท ๐ต) ยท (0 + 0)) = (๐ต + ๐ต)) |
36 | 9, 29, 35 | 3eqtr3a 2801 |
. 2
โข ((((๐ด โ โ โง (0
ยท ๐ด) โ 0) โง
๐ต โ โ) โง
(๐ฆ โ โ โง ((0
ยท ๐ด) ยท ๐ฆ) = 1)) โ ๐ต = (๐ต + ๐ต)) |
37 | 6, 36 | rexlimddv 3159 |
1
โข (((๐ด โ โ โง (0
ยท ๐ด) โ 0) โง
๐ต โ โ) โ
๐ต = (๐ต + ๐ต)) |