Step | Hyp | Ref
| Expression |
1 | | shsel 30567 |
. 2
โข ((๐ด โ
Sโ โง ๐ต โ Sโ )
โ (๐ถ โ (๐ด +โ ๐ต) โ โ๐ฅ โ ๐ด โ๐ง โ ๐ต ๐ถ = (๐ฅ +โ ๐ง))) |
2 | | id 22 |
. . . . . . 7
โข (๐ถ = (๐ฅ +โ ๐ง) โ ๐ถ = (๐ฅ +โ ๐ง)) |
3 | | shel 30464 |
. . . . . . . . . 10
โข ((๐ด โ
Sโ โง ๐ฅ โ ๐ด) โ ๐ฅ โ โ) |
4 | | shel 30464 |
. . . . . . . . . 10
โข ((๐ต โ
Sโ โง ๐ง โ ๐ต) โ ๐ง โ โ) |
5 | | hvaddsubval 30286 |
. . . . . . . . . 10
โข ((๐ฅ โ โ โง ๐ง โ โ) โ (๐ฅ +โ ๐ง) = (๐ฅ โโ (-1
ยทโ ๐ง))) |
6 | 3, 4, 5 | syl2an 597 |
. . . . . . . . 9
โข (((๐ด โ
Sโ โง ๐ฅ โ ๐ด) โง (๐ต โ Sโ
โง ๐ง โ ๐ต)) โ (๐ฅ +โ ๐ง) = (๐ฅ โโ (-1
ยทโ ๐ง))) |
7 | 6 | an4s 659 |
. . . . . . . 8
โข (((๐ด โ
Sโ โง ๐ต โ Sโ )
โง (๐ฅ โ ๐ด โง ๐ง โ ๐ต)) โ (๐ฅ +โ ๐ง) = (๐ฅ โโ (-1
ยทโ ๐ง))) |
8 | 7 | anassrs 469 |
. . . . . . 7
โข ((((๐ด โ
Sโ โง ๐ต โ Sโ )
โง ๐ฅ โ ๐ด) โง ๐ง โ ๐ต) โ (๐ฅ +โ ๐ง) = (๐ฅ โโ (-1
ยทโ ๐ง))) |
9 | 2, 8 | sylan9eqr 2795 |
. . . . . 6
โข
(((((๐ด โ
Sโ โง ๐ต โ Sโ )
โง ๐ฅ โ ๐ด) โง ๐ง โ ๐ต) โง ๐ถ = (๐ฅ +โ ๐ง)) โ ๐ถ = (๐ฅ โโ (-1
ยทโ ๐ง))) |
10 | | neg1cn 12326 |
. . . . . . . . . 10
โข -1 โ
โ |
11 | | shmulcl 30471 |
. . . . . . . . . 10
โข ((๐ต โ
Sโ โง -1 โ โ โง ๐ง โ ๐ต) โ (-1
ยทโ ๐ง) โ ๐ต) |
12 | 10, 11 | mp3an2 1450 |
. . . . . . . . 9
โข ((๐ต โ
Sโ โง ๐ง โ ๐ต) โ (-1
ยทโ ๐ง) โ ๐ต) |
13 | 12 | adantll 713 |
. . . . . . . 8
โข (((๐ด โ
Sโ โง ๐ต โ Sโ )
โง ๐ง โ ๐ต) โ (-1
ยทโ ๐ง) โ ๐ต) |
14 | 13 | adantlr 714 |
. . . . . . 7
โข ((((๐ด โ
Sโ โง ๐ต โ Sโ )
โง ๐ฅ โ ๐ด) โง ๐ง โ ๐ต) โ (-1
ยทโ ๐ง) โ ๐ต) |
15 | | oveq2 7417 |
. . . . . . . 8
โข (๐ฆ = (-1
ยทโ ๐ง) โ (๐ฅ โโ ๐ฆ) = (๐ฅ โโ (-1
ยทโ ๐ง))) |
16 | 15 | rspceeqv 3634 |
. . . . . . 7
โข (((-1
ยทโ ๐ง) โ ๐ต โง ๐ถ = (๐ฅ โโ (-1
ยทโ ๐ง))) โ โ๐ฆ โ ๐ต ๐ถ = (๐ฅ โโ ๐ฆ)) |
17 | 14, 16 | sylan 581 |
. . . . . 6
โข
(((((๐ด โ
Sโ โง ๐ต โ Sโ )
โง ๐ฅ โ ๐ด) โง ๐ง โ ๐ต) โง ๐ถ = (๐ฅ โโ (-1
ยทโ ๐ง))) โ โ๐ฆ โ ๐ต ๐ถ = (๐ฅ โโ ๐ฆ)) |
18 | 9, 17 | syldan 592 |
. . . . 5
โข
(((((๐ด โ
Sโ โง ๐ต โ Sโ )
โง ๐ฅ โ ๐ด) โง ๐ง โ ๐ต) โง ๐ถ = (๐ฅ +โ ๐ง)) โ โ๐ฆ โ ๐ต ๐ถ = (๐ฅ โโ ๐ฆ)) |
19 | 18 | rexlimdva2 3158 |
. . . 4
โข (((๐ด โ
Sโ โง ๐ต โ Sโ )
โง ๐ฅ โ ๐ด) โ (โ๐ง โ ๐ต ๐ถ = (๐ฅ +โ ๐ง) โ โ๐ฆ โ ๐ต ๐ถ = (๐ฅ โโ ๐ฆ))) |
20 | | id 22 |
. . . . . . 7
โข (๐ถ = (๐ฅ โโ ๐ฆ) โ ๐ถ = (๐ฅ โโ ๐ฆ)) |
21 | | shel 30464 |
. . . . . . . . . 10
โข ((๐ต โ
Sโ โง ๐ฆ โ ๐ต) โ ๐ฆ โ โ) |
22 | | hvsubval 30269 |
. . . . . . . . . 10
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (๐ฅ โโ
๐ฆ) = (๐ฅ +โ (-1
ยทโ ๐ฆ))) |
23 | 3, 21, 22 | syl2an 597 |
. . . . . . . . 9
โข (((๐ด โ
Sโ โง ๐ฅ โ ๐ด) โง (๐ต โ Sโ
โง ๐ฆ โ ๐ต)) โ (๐ฅ โโ ๐ฆ) = (๐ฅ +โ (-1
ยทโ ๐ฆ))) |
24 | 23 | an4s 659 |
. . . . . . . 8
โข (((๐ด โ
Sโ โง ๐ต โ Sโ )
โง (๐ฅ โ ๐ด โง ๐ฆ โ ๐ต)) โ (๐ฅ โโ ๐ฆ) = (๐ฅ +โ (-1
ยทโ ๐ฆ))) |
25 | 24 | anassrs 469 |
. . . . . . 7
โข ((((๐ด โ
Sโ โง ๐ต โ Sโ )
โง ๐ฅ โ ๐ด) โง ๐ฆ โ ๐ต) โ (๐ฅ โโ ๐ฆ) = (๐ฅ +โ (-1
ยทโ ๐ฆ))) |
26 | 20, 25 | sylan9eqr 2795 |
. . . . . 6
โข
(((((๐ด โ
Sโ โง ๐ต โ Sโ )
โง ๐ฅ โ ๐ด) โง ๐ฆ โ ๐ต) โง ๐ถ = (๐ฅ โโ ๐ฆ)) โ ๐ถ = (๐ฅ +โ (-1
ยทโ ๐ฆ))) |
27 | | shmulcl 30471 |
. . . . . . . . . 10
โข ((๐ต โ
Sโ โง -1 โ โ โง ๐ฆ โ ๐ต) โ (-1
ยทโ ๐ฆ) โ ๐ต) |
28 | 10, 27 | mp3an2 1450 |
. . . . . . . . 9
โข ((๐ต โ
Sโ โง ๐ฆ โ ๐ต) โ (-1
ยทโ ๐ฆ) โ ๐ต) |
29 | 28 | adantll 713 |
. . . . . . . 8
โข (((๐ด โ
Sโ โง ๐ต โ Sโ )
โง ๐ฆ โ ๐ต) โ (-1
ยทโ ๐ฆ) โ ๐ต) |
30 | 29 | adantlr 714 |
. . . . . . 7
โข ((((๐ด โ
Sโ โง ๐ต โ Sโ )
โง ๐ฅ โ ๐ด) โง ๐ฆ โ ๐ต) โ (-1
ยทโ ๐ฆ) โ ๐ต) |
31 | | oveq2 7417 |
. . . . . . . 8
โข (๐ง = (-1
ยทโ ๐ฆ) โ (๐ฅ +โ ๐ง) = (๐ฅ +โ (-1
ยทโ ๐ฆ))) |
32 | 31 | rspceeqv 3634 |
. . . . . . 7
โข (((-1
ยทโ ๐ฆ) โ ๐ต โง ๐ถ = (๐ฅ +โ (-1
ยทโ ๐ฆ))) โ โ๐ง โ ๐ต ๐ถ = (๐ฅ +โ ๐ง)) |
33 | 30, 32 | sylan 581 |
. . . . . 6
โข
(((((๐ด โ
Sโ โง ๐ต โ Sโ )
โง ๐ฅ โ ๐ด) โง ๐ฆ โ ๐ต) โง ๐ถ = (๐ฅ +โ (-1
ยทโ ๐ฆ))) โ โ๐ง โ ๐ต ๐ถ = (๐ฅ +โ ๐ง)) |
34 | 26, 33 | syldan 592 |
. . . . 5
โข
(((((๐ด โ
Sโ โง ๐ต โ Sโ )
โง ๐ฅ โ ๐ด) โง ๐ฆ โ ๐ต) โง ๐ถ = (๐ฅ โโ ๐ฆ)) โ โ๐ง โ ๐ต ๐ถ = (๐ฅ +โ ๐ง)) |
35 | 34 | rexlimdva2 3158 |
. . . 4
โข (((๐ด โ
Sโ โง ๐ต โ Sโ )
โง ๐ฅ โ ๐ด) โ (โ๐ฆ โ ๐ต ๐ถ = (๐ฅ โโ ๐ฆ) โ โ๐ง โ ๐ต ๐ถ = (๐ฅ +โ ๐ง))) |
36 | 19, 35 | impbid 211 |
. . 3
โข (((๐ด โ
Sโ โง ๐ต โ Sโ )
โง ๐ฅ โ ๐ด) โ (โ๐ง โ ๐ต ๐ถ = (๐ฅ +โ ๐ง) โ โ๐ฆ โ ๐ต ๐ถ = (๐ฅ โโ ๐ฆ))) |
37 | 36 | rexbidva 3177 |
. 2
โข ((๐ด โ
Sโ โง ๐ต โ Sโ )
โ (โ๐ฅ โ
๐ด โ๐ง โ ๐ต ๐ถ = (๐ฅ +โ ๐ง) โ โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ถ = (๐ฅ โโ ๐ฆ))) |
38 | 1, 37 | bitrd 279 |
1
โข ((๐ด โ
Sโ โง ๐ต โ Sโ )
โ (๐ถ โ (๐ด +โ ๐ต) โ โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ถ = (๐ฅ โโ ๐ฆ))) |