Step | Hyp | Ref
| Expression |
1 | | recex 11845 |
. . . 4
โข ((๐ต โ โ โง ๐ต โ 0) โ โ๐ฆ โ โ (๐ต ยท ๐ฆ) = 1) |
2 | 1 | 3adant1 1127 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ โ๐ฆ โ โ (๐ต ยท ๐ฆ) = 1) |
3 | | simprl 768 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง (๐ต ยท ๐ฆ) = 1)) โ ๐ฆ โ โ) |
4 | | simpll 764 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง (๐ต ยท ๐ฆ) = 1)) โ ๐ด โ โ) |
5 | 3, 4 | mulcld 11233 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง (๐ต ยท ๐ฆ) = 1)) โ (๐ฆ ยท ๐ด) โ โ) |
6 | | oveq1 7409 |
. . . . . . . 8
โข ((๐ต ยท ๐ฆ) = 1 โ ((๐ต ยท ๐ฆ) ยท ๐ด) = (1 ยท ๐ด)) |
7 | 6 | ad2antll 726 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง (๐ต ยท ๐ฆ) = 1)) โ ((๐ต ยท ๐ฆ) ยท ๐ด) = (1 ยท ๐ด)) |
8 | | simplr 766 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง (๐ต ยท ๐ฆ) = 1)) โ ๐ต โ โ) |
9 | 8, 3, 4 | mulassd 11236 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง (๐ต ยท ๐ฆ) = 1)) โ ((๐ต ยท ๐ฆ) ยท ๐ด) = (๐ต ยท (๐ฆ ยท ๐ด))) |
10 | 4 | mullidd 11231 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง (๐ต ยท ๐ฆ) = 1)) โ (1 ยท ๐ด) = ๐ด) |
11 | 7, 9, 10 | 3eqtr3d 2772 |
. . . . . 6
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง (๐ต ยท ๐ฆ) = 1)) โ (๐ต ยท (๐ฆ ยท ๐ด)) = ๐ด) |
12 | | oveq2 7410 |
. . . . . . . 8
โข (๐ฅ = (๐ฆ ยท ๐ด) โ (๐ต ยท ๐ฅ) = (๐ต ยท (๐ฆ ยท ๐ด))) |
13 | 12 | eqeq1d 2726 |
. . . . . . 7
โข (๐ฅ = (๐ฆ ยท ๐ด) โ ((๐ต ยท ๐ฅ) = ๐ด โ (๐ต ยท (๐ฆ ยท ๐ด)) = ๐ด)) |
14 | 13 | rspcev 3604 |
. . . . . 6
โข (((๐ฆ ยท ๐ด) โ โ โง (๐ต ยท (๐ฆ ยท ๐ด)) = ๐ด) โ โ๐ฅ โ โ (๐ต ยท ๐ฅ) = ๐ด) |
15 | 5, 11, 14 | syl2anc 583 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ฆ โ โ โง (๐ต ยท ๐ฆ) = 1)) โ โ๐ฅ โ โ (๐ต ยท ๐ฅ) = ๐ด) |
16 | 15 | rexlimdvaa 3148 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ) โ
(โ๐ฆ โ โ
(๐ต ยท ๐ฆ) = 1 โ โ๐ฅ โ โ (๐ต ยท ๐ฅ) = ๐ด)) |
17 | 16 | 3adant3 1129 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ (โ๐ฆ โ โ (๐ต ยท ๐ฆ) = 1 โ โ๐ฅ โ โ (๐ต ยท ๐ฅ) = ๐ด)) |
18 | 2, 17 | mpd 15 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ โ๐ฅ โ โ (๐ต ยท ๐ฅ) = ๐ด) |
19 | | eqtr3 2750 |
. . . . . . 7
โข (((๐ต ยท ๐ฅ) = ๐ด โง (๐ต ยท ๐ฆ) = ๐ด) โ (๐ต ยท ๐ฅ) = (๐ต ยท ๐ฆ)) |
20 | | mulcan 11850 |
. . . . . . 7
โข ((๐ฅ โ โ โง ๐ฆ โ โ โง (๐ต โ โ โง ๐ต โ 0)) โ ((๐ต ยท ๐ฅ) = (๐ต ยท ๐ฆ) โ ๐ฅ = ๐ฆ)) |
21 | 19, 20 | imbitrid 243 |
. . . . . 6
โข ((๐ฅ โ โ โง ๐ฆ โ โ โง (๐ต โ โ โง ๐ต โ 0)) โ (((๐ต ยท ๐ฅ) = ๐ด โง (๐ต ยท ๐ฆ) = ๐ด) โ ๐ฅ = ๐ฆ)) |
22 | 21 | 3expa 1115 |
. . . . 5
โข (((๐ฅ โ โ โง ๐ฆ โ โ) โง (๐ต โ โ โง ๐ต โ 0)) โ (((๐ต ยท ๐ฅ) = ๐ด โง (๐ต ยท ๐ฆ) = ๐ด) โ ๐ฅ = ๐ฆ)) |
23 | 22 | expcom 413 |
. . . 4
โข ((๐ต โ โ โง ๐ต โ 0) โ ((๐ฅ โ โ โง ๐ฆ โ โ) โ (((๐ต ยท ๐ฅ) = ๐ด โง (๐ต ยท ๐ฆ) = ๐ด) โ ๐ฅ = ๐ฆ))) |
24 | 23 | 3adant1 1127 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ ((๐ฅ โ โ โง ๐ฆ โ โ) โ (((๐ต ยท ๐ฅ) = ๐ด โง (๐ต ยท ๐ฆ) = ๐ด) โ ๐ฅ = ๐ฆ))) |
25 | 24 | ralrimivv 3190 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ โ๐ฅ โ โ โ๐ฆ โ โ (((๐ต ยท ๐ฅ) = ๐ด โง (๐ต ยท ๐ฆ) = ๐ด) โ ๐ฅ = ๐ฆ)) |
26 | | oveq2 7410 |
. . . 4
โข (๐ฅ = ๐ฆ โ (๐ต ยท ๐ฅ) = (๐ต ยท ๐ฆ)) |
27 | 26 | eqeq1d 2726 |
. . 3
โข (๐ฅ = ๐ฆ โ ((๐ต ยท ๐ฅ) = ๐ด โ (๐ต ยท ๐ฆ) = ๐ด)) |
28 | 27 | reu4 3720 |
. 2
โข
(โ!๐ฅ โ
โ (๐ต ยท ๐ฅ) = ๐ด โ (โ๐ฅ โ โ (๐ต ยท ๐ฅ) = ๐ด โง โ๐ฅ โ โ โ๐ฆ โ โ (((๐ต ยท ๐ฅ) = ๐ด โง (๐ต ยท ๐ฆ) = ๐ด) โ ๐ฅ = ๐ฆ))) |
29 | 18, 25, 28 | sylanbrc 582 |
1
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ต โ 0) โ โ!๐ฅ โ โ (๐ต ยท ๐ฅ) = ๐ด) |