Step | Hyp | Ref
| Expression |
1 | | recex 11794 |
. . . 4
โข ((๐ต โ โ โง ๐ต โ 0) โ โ๐ฆ โ โ (๐ต ยท ๐ฆ) = 1) |
2 | 1 | 3adant1 1131 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ โ๐ฆ โ โ (๐ต ยท ๐ฆ) = 1) |
3 | | simprl 770 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง (๐ต ยท ๐ฆ) = 1)) โ ๐ฆ โ โ) |
4 | | simpll 766 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง (๐ต ยท ๐ฆ) = 1)) โ ๐ด โ โ) |
5 | 3, 4 | mulcld 11182 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง (๐ต ยท ๐ฆ) = 1)) โ (๐ฆ ยท ๐ด) โ โ) |
6 | | oveq1 7369 |
. . . . . . . 8
โข ((๐ต ยท ๐ฆ) = 1 โ ((๐ต ยท ๐ฆ) ยท ๐ด) = (1 ยท ๐ด)) |
7 | 6 | ad2antll 728 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง (๐ต ยท ๐ฆ) = 1)) โ ((๐ต ยท ๐ฆ) ยท ๐ด) = (1 ยท ๐ด)) |
8 | | simplr 768 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง (๐ต ยท ๐ฆ) = 1)) โ ๐ต โ โ) |
9 | 8, 3, 4 | mulassd 11185 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง (๐ต ยท ๐ฆ) = 1)) โ ((๐ต ยท ๐ฆ) ยท ๐ด) = (๐ต ยท (๐ฆ ยท ๐ด))) |
10 | 4 | mulid2d 11180 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง (๐ต ยท ๐ฆ) = 1)) โ (1 ยท ๐ด) = ๐ด) |
11 | 7, 9, 10 | 3eqtr3d 2785 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง (๐ต ยท ๐ฆ) = 1)) โ (๐ต ยท (๐ฆ ยท ๐ด)) = ๐ด) |
12 | | oveq2 7370 |
. . . . . . . 8
โข (๐ฅ = (๐ฆ ยท ๐ด) โ (๐ต ยท ๐ฅ) = (๐ต ยท (๐ฆ ยท ๐ด))) |
13 | 12 | eqeq1d 2739 |
. . . . . . 7
โข (๐ฅ = (๐ฆ ยท ๐ด) โ ((๐ต ยท ๐ฅ) = ๐ด โ (๐ต ยท (๐ฆ ยท ๐ด)) = ๐ด)) |
14 | 13 | rspcev 3584 |
. . . . . 6
โข (((๐ฆ ยท ๐ด) โ โ โง (๐ต ยท (๐ฆ ยท ๐ด)) = ๐ด) โ โ๐ฅ โ โ (๐ต ยท ๐ฅ) = ๐ด) |
15 | 5, 11, 14 | syl2anc 585 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง (๐ต ยท ๐ฆ) = 1)) โ โ๐ฅ โ โ (๐ต ยท ๐ฅ) = ๐ด) |
16 | 15 | rexlimdvaa 3154 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โ๐ฆ โ โ
(๐ต ยท ๐ฆ) = 1 โ โ๐ฅ โ โ (๐ต ยท ๐ฅ) = ๐ด)) |
17 | 16 | 3adant3 1133 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ (โ๐ฆ โ โ (๐ต ยท ๐ฆ) = 1 โ โ๐ฅ โ โ (๐ต ยท ๐ฅ) = ๐ด)) |
18 | 2, 17 | mpd 15 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ โ๐ฅ โ โ (๐ต ยท ๐ฅ) = ๐ด) |
19 | | eqtr3 2763 |
. . . . . . 7
โข (((๐ต ยท ๐ฅ) = ๐ด โง (๐ต ยท ๐ฆ) = ๐ด) โ (๐ต ยท ๐ฅ) = (๐ต ยท ๐ฆ)) |
20 | | mulcan 11799 |
. . . . . . 7
โข ((๐ฅ โ โ โง ๐ฆ โ โ โง (๐ต โ โ โง ๐ต โ 0)) โ ((๐ต ยท ๐ฅ) = (๐ต ยท ๐ฆ) โ ๐ฅ = ๐ฆ)) |
21 | 19, 20 | imbitrid 243 |
. . . . . 6
โข ((๐ฅ โ โ โง ๐ฆ โ โ โง (๐ต โ โ โง ๐ต โ 0)) โ (((๐ต ยท ๐ฅ) = ๐ด โง (๐ต ยท ๐ฆ) = ๐ด) โ ๐ฅ = ๐ฆ)) |
22 | 21 | 3expa 1119 |
. . . . 5
โข (((๐ฅ โ โ โง ๐ฆ โ โ) โง (๐ต โ โ โง ๐ต โ 0)) โ (((๐ต ยท ๐ฅ) = ๐ด โง (๐ต ยท ๐ฆ) = ๐ด) โ ๐ฅ = ๐ฆ)) |
23 | 22 | expcom 415 |
. . . 4
โข ((๐ต โ โ โง ๐ต โ 0) โ ((๐ฅ โ โ โง ๐ฆ โ โ) โ (((๐ต ยท ๐ฅ) = ๐ด โง (๐ต ยท ๐ฆ) = ๐ด) โ ๐ฅ = ๐ฆ))) |
24 | 23 | 3adant1 1131 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ ((๐ฅ โ โ โง ๐ฆ โ โ) โ (((๐ต ยท ๐ฅ) = ๐ด โง (๐ต ยท ๐ฆ) = ๐ด) โ ๐ฅ = ๐ฆ))) |
25 | 24 | ralrimivv 3196 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ โ๐ฅ โ โ โ๐ฆ โ โ (((๐ต ยท ๐ฅ) = ๐ด โง (๐ต ยท ๐ฆ) = ๐ด) โ ๐ฅ = ๐ฆ)) |
26 | | oveq2 7370 |
. . . 4
โข (๐ฅ = ๐ฆ โ (๐ต ยท ๐ฅ) = (๐ต ยท ๐ฆ)) |
27 | 26 | eqeq1d 2739 |
. . 3
โข (๐ฅ = ๐ฆ โ ((๐ต ยท ๐ฅ) = ๐ด โ (๐ต ยท ๐ฆ) = ๐ด)) |
28 | 27 | reu4 3694 |
. 2
โข
(โ!๐ฅ โ
โ (๐ต ยท ๐ฅ) = ๐ด โ (โ๐ฅ โ โ (๐ต ยท ๐ฅ) = ๐ด โง โ๐ฅ โ โ โ๐ฆ โ โ (((๐ต ยท ๐ฅ) = ๐ด โง (๐ต ยท ๐ฆ) = ๐ด) โ ๐ฅ = ๐ฆ))) |
29 | 18, 25, 28 | sylanbrc 584 |
1
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ โ!๐ฅ โ โ (๐ต ยท ๐ฅ) = ๐ด) |