Step | Hyp | Ref
| Expression |
1 | | recexap 8609 |
. . . 4
โข ((๐ต โ โ โง ๐ต # 0) โ โ๐ฆ โ โ (๐ต ยท ๐ฆ) = 1) |
2 | 1 | 3adant1 1015 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต # 0) โ โ๐ฆ โ โ (๐ต ยท ๐ฆ) = 1) |
3 | | simprl 529 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง (๐ต ยท ๐ฆ) = 1)) โ ๐ฆ โ โ) |
4 | | simpll 527 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง (๐ต ยท ๐ฆ) = 1)) โ ๐ด โ โ) |
5 | 3, 4 | mulcld 7977 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง (๐ต ยท ๐ฆ) = 1)) โ (๐ฆ ยท ๐ด) โ โ) |
6 | | oveq1 5881 |
. . . . . . . 8
โข ((๐ต ยท ๐ฆ) = 1 โ ((๐ต ยท ๐ฆ) ยท ๐ด) = (1 ยท ๐ด)) |
7 | 6 | ad2antll 491 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง (๐ต ยท ๐ฆ) = 1)) โ ((๐ต ยท ๐ฆ) ยท ๐ด) = (1 ยท ๐ด)) |
8 | | simplr 528 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง (๐ต ยท ๐ฆ) = 1)) โ ๐ต โ โ) |
9 | 8, 3, 4 | mulassd 7980 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง (๐ต ยท ๐ฆ) = 1)) โ ((๐ต ยท ๐ฆ) ยท ๐ด) = (๐ต ยท (๐ฆ ยท ๐ด))) |
10 | 4 | mulid2d 7975 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง (๐ต ยท ๐ฆ) = 1)) โ (1 ยท ๐ด) = ๐ด) |
11 | 7, 9, 10 | 3eqtr3d 2218 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง (๐ต ยท ๐ฆ) = 1)) โ (๐ต ยท (๐ฆ ยท ๐ด)) = ๐ด) |
12 | | oveq2 5882 |
. . . . . . . 8
โข (๐ฅ = (๐ฆ ยท ๐ด) โ (๐ต ยท ๐ฅ) = (๐ต ยท (๐ฆ ยท ๐ด))) |
13 | 12 | eqeq1d 2186 |
. . . . . . 7
โข (๐ฅ = (๐ฆ ยท ๐ด) โ ((๐ต ยท ๐ฅ) = ๐ด โ (๐ต ยท (๐ฆ ยท ๐ด)) = ๐ด)) |
14 | 13 | rspcev 2841 |
. . . . . 6
โข (((๐ฆ ยท ๐ด) โ โ โง (๐ต ยท (๐ฆ ยท ๐ด)) = ๐ด) โ โ๐ฅ โ โ (๐ต ยท ๐ฅ) = ๐ด) |
15 | 5, 11, 14 | syl2anc 411 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง (๐ต ยท ๐ฆ) = 1)) โ โ๐ฅ โ โ (๐ต ยท ๐ฅ) = ๐ด) |
16 | 15 | rexlimdvaa 2595 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โ๐ฆ โ โ
(๐ต ยท ๐ฆ) = 1 โ โ๐ฅ โ โ (๐ต ยท ๐ฅ) = ๐ด)) |
17 | 16 | 3adant3 1017 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต # 0) โ (โ๐ฆ โ โ (๐ต ยท ๐ฆ) = 1 โ โ๐ฅ โ โ (๐ต ยท ๐ฅ) = ๐ด)) |
18 | 2, 17 | mpd 13 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต # 0) โ โ๐ฅ โ โ (๐ต ยท ๐ฅ) = ๐ด) |
19 | | eqtr3 2197 |
. . . . . . 7
โข (((๐ต ยท ๐ฅ) = ๐ด โง (๐ต ยท ๐ฆ) = ๐ด) โ (๐ต ยท ๐ฅ) = (๐ต ยท ๐ฆ)) |
20 | | mulcanap 8621 |
. . . . . . 7
โข ((๐ฅ โ โ โง ๐ฆ โ โ โง (๐ต โ โ โง ๐ต # 0)) โ ((๐ต ยท ๐ฅ) = (๐ต ยท ๐ฆ) โ ๐ฅ = ๐ฆ)) |
21 | 19, 20 | imbitrid 154 |
. . . . . 6
โข ((๐ฅ โ โ โง ๐ฆ โ โ โง (๐ต โ โ โง ๐ต # 0)) โ (((๐ต ยท ๐ฅ) = ๐ด โง (๐ต ยท ๐ฆ) = ๐ด) โ ๐ฅ = ๐ฆ)) |
22 | 21 | 3expa 1203 |
. . . . 5
โข (((๐ฅ โ โ โง ๐ฆ โ โ) โง (๐ต โ โ โง ๐ต # 0)) โ (((๐ต ยท ๐ฅ) = ๐ด โง (๐ต ยท ๐ฆ) = ๐ด) โ ๐ฅ = ๐ฆ)) |
23 | 22 | expcom 116 |
. . . 4
โข ((๐ต โ โ โง ๐ต # 0) โ ((๐ฅ โ โ โง ๐ฆ โ โ) โ (((๐ต ยท ๐ฅ) = ๐ด โง (๐ต ยท ๐ฆ) = ๐ด) โ ๐ฅ = ๐ฆ))) |
24 | 23 | 3adant1 1015 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต # 0) โ ((๐ฅ โ โ โง ๐ฆ โ โ) โ (((๐ต ยท ๐ฅ) = ๐ด โง (๐ต ยท ๐ฆ) = ๐ด) โ ๐ฅ = ๐ฆ))) |
25 | 24 | ralrimivv 2558 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต # 0) โ โ๐ฅ โ โ โ๐ฆ โ โ (((๐ต ยท ๐ฅ) = ๐ด โง (๐ต ยท ๐ฆ) = ๐ด) โ ๐ฅ = ๐ฆ)) |
26 | | oveq2 5882 |
. . . 4
โข (๐ฅ = ๐ฆ โ (๐ต ยท ๐ฅ) = (๐ต ยท ๐ฆ)) |
27 | 26 | eqeq1d 2186 |
. . 3
โข (๐ฅ = ๐ฆ โ ((๐ต ยท ๐ฅ) = ๐ด โ (๐ต ยท ๐ฆ) = ๐ด)) |
28 | 27 | reu4 2931 |
. 2
โข
(โ!๐ฅ โ
โ (๐ต ยท ๐ฅ) = ๐ด โ (โ๐ฅ โ โ (๐ต ยท ๐ฅ) = ๐ด โง โ๐ฅ โ โ โ๐ฆ โ โ (((๐ต ยท ๐ฅ) = ๐ด โง (๐ต ยท ๐ฆ) = ๐ด) โ ๐ฅ = ๐ฆ))) |
29 | 18, 25, 28 | sylanbrc 417 |
1
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต # 0) โ โ!๐ฅ โ โ (๐ต ยท ๐ฅ) = ๐ด) |