Step | Hyp | Ref
| Expression |
1 | | ressxr 11206 |
. . . 4
โข โ
โ โ* |
2 | | xrecex 31818 |
. . . . 5
โข ((๐ต โ โ โง ๐ต โ 0) โ โ๐ฆ โ โ (๐ต ยทe ๐ฆ) = 1) |
3 | 2 | 3adant1 1131 |
. . . 4
โข ((๐ด โ โ*
โง ๐ต โ โ
โง ๐ต โ 0) โ
โ๐ฆ โ โ
(๐ต ยทe
๐ฆ) = 1) |
4 | | ssrexv 4016 |
. . . 4
โข (โ
โ โ* โ (โ๐ฆ โ โ (๐ต ยทe ๐ฆ) = 1 โ โ๐ฆ โ โ* (๐ต ยทe ๐ฆ) = 1)) |
5 | 1, 3, 4 | mpsyl 68 |
. . 3
โข ((๐ด โ โ*
โง ๐ต โ โ
โง ๐ต โ 0) โ
โ๐ฆ โ
โ* (๐ต
ยทe ๐ฆ) =
1) |
6 | | simprl 770 |
. . . . . . 7
โข (((๐ด โ โ*
โง ๐ต โ โ)
โง (๐ฆ โ
โ* โง (๐ต ยทe ๐ฆ) = 1)) โ ๐ฆ โ โ*) |
7 | | simpll 766 |
. . . . . . 7
โข (((๐ด โ โ*
โง ๐ต โ โ)
โง (๐ฆ โ
โ* โง (๐ต ยทe ๐ฆ) = 1)) โ ๐ด โ
โ*) |
8 | 6, 7 | xmulcld 13228 |
. . . . . 6
โข (((๐ด โ โ*
โง ๐ต โ โ)
โง (๐ฆ โ
โ* โง (๐ต ยทe ๐ฆ) = 1)) โ (๐ฆ ยทe ๐ด) โ
โ*) |
9 | | oveq1 7369 |
. . . . . . . 8
โข ((๐ต ยทe ๐ฆ) = 1 โ ((๐ต ยทe ๐ฆ) ยทe ๐ด) = (1 ยทe ๐ด)) |
10 | 9 | ad2antll 728 |
. . . . . . 7
โข (((๐ด โ โ*
โง ๐ต โ โ)
โง (๐ฆ โ
โ* โง (๐ต ยทe ๐ฆ) = 1)) โ ((๐ต ยทe ๐ฆ) ยทe ๐ด) = (1 ยทe ๐ด)) |
11 | | simplr 768 |
. . . . . . . . 9
โข (((๐ด โ โ*
โง ๐ต โ โ)
โง (๐ฆ โ
โ* โง (๐ต ยทe ๐ฆ) = 1)) โ ๐ต โ โ) |
12 | 11 | rexrd 11212 |
. . . . . . . 8
โข (((๐ด โ โ*
โง ๐ต โ โ)
โง (๐ฆ โ
โ* โง (๐ต ยทe ๐ฆ) = 1)) โ ๐ต โ
โ*) |
13 | | xmulass 13213 |
. . . . . . . 8
โข ((๐ต โ โ*
โง ๐ฆ โ
โ* โง ๐ด
โ โ*) โ ((๐ต ยทe ๐ฆ) ยทe ๐ด) = (๐ต ยทe (๐ฆ ยทe ๐ด))) |
14 | 12, 6, 7, 13 | syl3anc 1372 |
. . . . . . 7
โข (((๐ด โ โ*
โง ๐ต โ โ)
โง (๐ฆ โ
โ* โง (๐ต ยทe ๐ฆ) = 1)) โ ((๐ต ยทe ๐ฆ) ยทe ๐ด) = (๐ต ยทe (๐ฆ ยทe ๐ด))) |
15 | | xmulid2 13206 |
. . . . . . . 8
โข (๐ด โ โ*
โ (1 ยทe ๐ด) = ๐ด) |
16 | 7, 15 | syl 17 |
. . . . . . 7
โข (((๐ด โ โ*
โง ๐ต โ โ)
โง (๐ฆ โ
โ* โง (๐ต ยทe ๐ฆ) = 1)) โ (1 ยทe ๐ด) = ๐ด) |
17 | 10, 14, 16 | 3eqtr3d 2785 |
. . . . . 6
โข (((๐ด โ โ*
โง ๐ต โ โ)
โง (๐ฆ โ
โ* โง (๐ต ยทe ๐ฆ) = 1)) โ (๐ต ยทe (๐ฆ ยทe ๐ด)) = ๐ด) |
18 | | oveq2 7370 |
. . . . . . . 8
โข (๐ฅ = (๐ฆ ยทe ๐ด) โ (๐ต ยทe ๐ฅ) = (๐ต ยทe (๐ฆ ยทe ๐ด))) |
19 | 18 | eqeq1d 2739 |
. . . . . . 7
โข (๐ฅ = (๐ฆ ยทe ๐ด) โ ((๐ต ยทe ๐ฅ) = ๐ด โ (๐ต ยทe (๐ฆ ยทe ๐ด)) = ๐ด)) |
20 | 19 | rspcev 3584 |
. . . . . 6
โข (((๐ฆ ยทe ๐ด) โ โ*
โง (๐ต
ยทe (๐ฆ
ยทe ๐ด)) =
๐ด) โ โ๐ฅ โ โ*
(๐ต ยทe
๐ฅ) = ๐ด) |
21 | 8, 17, 20 | syl2anc 585 |
. . . . 5
โข (((๐ด โ โ*
โง ๐ต โ โ)
โง (๐ฆ โ
โ* โง (๐ต ยทe ๐ฆ) = 1)) โ โ๐ฅ โ โ* (๐ต ยทe ๐ฅ) = ๐ด) |
22 | 21 | rexlimdvaa 3154 |
. . . 4
โข ((๐ด โ โ*
โง ๐ต โ โ)
โ (โ๐ฆ โ
โ* (๐ต
ยทe ๐ฆ) = 1
โ โ๐ฅ โ
โ* (๐ต
ยทe ๐ฅ) =
๐ด)) |
23 | 22 | 3adant3 1133 |
. . 3
โข ((๐ด โ โ*
โง ๐ต โ โ
โง ๐ต โ 0) โ
(โ๐ฆ โ
โ* (๐ต
ยทe ๐ฆ) = 1
โ โ๐ฅ โ
โ* (๐ต
ยทe ๐ฅ) =
๐ด)) |
24 | 5, 23 | mpd 15 |
. 2
โข ((๐ด โ โ*
โง ๐ต โ โ
โง ๐ต โ 0) โ
โ๐ฅ โ
โ* (๐ต
ยทe ๐ฅ) =
๐ด) |
25 | | eqtr3 2763 |
. . . . . . 7
โข (((๐ต ยทe ๐ฅ) = ๐ด โง (๐ต ยทe ๐ฆ) = ๐ด) โ (๐ต ยทe ๐ฅ) = (๐ต ยทe ๐ฆ)) |
26 | | simp1 1137 |
. . . . . . . 8
โข ((๐ฅ โ โ*
โง ๐ฆ โ
โ* โง (๐ต โ โ โง ๐ต โ 0)) โ ๐ฅ โ โ*) |
27 | | simp2 1138 |
. . . . . . . 8
โข ((๐ฅ โ โ*
โง ๐ฆ โ
โ* โง (๐ต โ โ โง ๐ต โ 0)) โ ๐ฆ โ โ*) |
28 | | simp3l 1202 |
. . . . . . . 8
โข ((๐ฅ โ โ*
โง ๐ฆ โ
โ* โง (๐ต โ โ โง ๐ต โ 0)) โ ๐ต โ โ) |
29 | | simp3r 1203 |
. . . . . . . 8
โข ((๐ฅ โ โ*
โง ๐ฆ โ
โ* โง (๐ต โ โ โง ๐ต โ 0)) โ ๐ต โ 0) |
30 | 26, 27, 28, 29 | xmulcand 31819 |
. . . . . . 7
โข ((๐ฅ โ โ*
โง ๐ฆ โ
โ* โง (๐ต โ โ โง ๐ต โ 0)) โ ((๐ต ยทe ๐ฅ) = (๐ต ยทe ๐ฆ) โ ๐ฅ = ๐ฆ)) |
31 | 25, 30 | imbitrid 243 |
. . . . . 6
โข ((๐ฅ โ โ*
โง ๐ฆ โ
โ* โง (๐ต โ โ โง ๐ต โ 0)) โ (((๐ต ยทe ๐ฅ) = ๐ด โง (๐ต ยทe ๐ฆ) = ๐ด) โ ๐ฅ = ๐ฆ)) |
32 | 31 | 3expa 1119 |
. . . . 5
โข (((๐ฅ โ โ*
โง ๐ฆ โ
โ*) โง (๐ต โ โ โง ๐ต โ 0)) โ (((๐ต ยทe ๐ฅ) = ๐ด โง (๐ต ยทe ๐ฆ) = ๐ด) โ ๐ฅ = ๐ฆ)) |
33 | 32 | expcom 415 |
. . . 4
โข ((๐ต โ โ โง ๐ต โ 0) โ ((๐ฅ โ โ*
โง ๐ฆ โ
โ*) โ (((๐ต ยทe ๐ฅ) = ๐ด โง (๐ต ยทe ๐ฆ) = ๐ด) โ ๐ฅ = ๐ฆ))) |
34 | 33 | 3adant1 1131 |
. . 3
โข ((๐ด โ โ*
โง ๐ต โ โ
โง ๐ต โ 0) โ
((๐ฅ โ
โ* โง ๐ฆ
โ โ*) โ (((๐ต ยทe ๐ฅ) = ๐ด โง (๐ต ยทe ๐ฆ) = ๐ด) โ ๐ฅ = ๐ฆ))) |
35 | 34 | ralrimivv 3196 |
. 2
โข ((๐ด โ โ*
โง ๐ต โ โ
โง ๐ต โ 0) โ
โ๐ฅ โ
โ* โ๐ฆ โ โ* (((๐ต ยทe ๐ฅ) = ๐ด โง (๐ต ยทe ๐ฆ) = ๐ด) โ ๐ฅ = ๐ฆ)) |
36 | | oveq2 7370 |
. . . 4
โข (๐ฅ = ๐ฆ โ (๐ต ยทe ๐ฅ) = (๐ต ยทe ๐ฆ)) |
37 | 36 | eqeq1d 2739 |
. . 3
โข (๐ฅ = ๐ฆ โ ((๐ต ยทe ๐ฅ) = ๐ด โ (๐ต ยทe ๐ฆ) = ๐ด)) |
38 | 37 | reu4 3694 |
. 2
โข
(โ!๐ฅ โ
โ* (๐ต
ยทe ๐ฅ) =
๐ด โ (โ๐ฅ โ โ*
(๐ต ยทe
๐ฅ) = ๐ด โง โ๐ฅ โ โ* โ๐ฆ โ โ*
(((๐ต ยทe
๐ฅ) = ๐ด โง (๐ต ยทe ๐ฆ) = ๐ด) โ ๐ฅ = ๐ฆ))) |
39 | 24, 35, 38 | sylanbrc 584 |
1
โข ((๐ด โ โ*
โง ๐ต โ โ
โง ๐ต โ 0) โ
โ!๐ฅ โ
โ* (๐ต
ยทe ๐ฅ) =
๐ด) |