Step | Hyp | Ref
| Expression |
1 | | shsel 30430 |
. 2
โข ((๐ด โ
Sโ โง ๐ต โ Sโ )
โ (๐ถ โ (๐ด +โ ๐ต) โ โ๐ฅ โ ๐ด โ๐ง โ ๐ต ๐ถ = (๐ฅ +โ ๐ง))) |
2 | | id 22 |
. . . . . . 7
โข (๐ถ = (๐ฅ +โ ๐ง) โ ๐ถ = (๐ฅ +โ ๐ง)) |
3 | | shel 30327 |
. . . . . . . . . 10
โข ((๐ด โ
Sโ โง ๐ฅ โ ๐ด) โ ๐ฅ โ โ) |
4 | | shel 30327 |
. . . . . . . . . 10
โข ((๐ต โ
Sโ โง ๐ง โ ๐ต) โ ๐ง โ โ) |
5 | | hvaddsubval 30149 |
. . . . . . . . . 10
โข ((๐ฅ โ โ โง ๐ง โ โ) โ (๐ฅ +โ ๐ง) = (๐ฅ โโ (-1
ยทโ ๐ง))) |
6 | 3, 4, 5 | syl2an 596 |
. . . . . . . . 9
โข (((๐ด โ
Sโ โง ๐ฅ โ ๐ด) โง (๐ต โ Sโ
โง ๐ง โ ๐ต)) โ (๐ฅ +โ ๐ง) = (๐ฅ โโ (-1
ยทโ ๐ง))) |
7 | 6 | an4s 658 |
. . . . . . . 8
โข (((๐ด โ
Sโ โง ๐ต โ Sโ )
โง (๐ฅ โ ๐ด โง ๐ง โ ๐ต)) โ (๐ฅ +โ ๐ง) = (๐ฅ โโ (-1
ยทโ ๐ง))) |
8 | 7 | anassrs 468 |
. . . . . . 7
โข ((((๐ด โ
Sโ โง ๐ต โ Sโ )
โง ๐ฅ โ ๐ด) โง ๐ง โ ๐ต) โ (๐ฅ +โ ๐ง) = (๐ฅ โโ (-1
ยทโ ๐ง))) |
9 | 2, 8 | sylan9eqr 2793 |
. . . . . 6
โข
(((((๐ด โ
Sโ โง ๐ต โ Sโ )
โง ๐ฅ โ ๐ด) โง ๐ง โ ๐ต) โง ๐ถ = (๐ฅ +โ ๐ง)) โ ๐ถ = (๐ฅ โโ (-1
ยทโ ๐ง))) |
10 | | neg1cn 12308 |
. . . . . . . . . 10
โข -1 โ
โ |
11 | | shmulcl 30334 |
. . . . . . . . . 10
โข ((๐ต โ
Sโ โง -1 โ โ โง ๐ง โ ๐ต) โ (-1
ยทโ ๐ง) โ ๐ต) |
12 | 10, 11 | mp3an2 1449 |
. . . . . . . . 9
โข ((๐ต โ
Sโ โง ๐ง โ ๐ต) โ (-1
ยทโ ๐ง) โ ๐ต) |
13 | 12 | adantll 712 |
. . . . . . . 8
โข (((๐ด โ
Sโ โง ๐ต โ Sโ )
โง ๐ง โ ๐ต) โ (-1
ยทโ ๐ง) โ ๐ต) |
14 | 13 | adantlr 713 |
. . . . . . 7
โข ((((๐ด โ
Sโ โง ๐ต โ Sโ )
โง ๐ฅ โ ๐ด) โง ๐ง โ ๐ต) โ (-1
ยทโ ๐ง) โ ๐ต) |
15 | | oveq2 7401 |
. . . . . . . 8
โข (๐ฆ = (-1
ยทโ ๐ง) โ (๐ฅ โโ ๐ฆ) = (๐ฅ โโ (-1
ยทโ ๐ง))) |
16 | 15 | rspceeqv 3629 |
. . . . . . 7
โข (((-1
ยทโ ๐ง) โ ๐ต โง ๐ถ = (๐ฅ โโ (-1
ยทโ ๐ง))) โ โ๐ฆ โ ๐ต ๐ถ = (๐ฅ โโ ๐ฆ)) |
17 | 14, 16 | sylan 580 |
. . . . . 6
โข
(((((๐ด โ
Sโ โง ๐ต โ Sโ )
โง ๐ฅ โ ๐ด) โง ๐ง โ ๐ต) โง ๐ถ = (๐ฅ โโ (-1
ยทโ ๐ง))) โ โ๐ฆ โ ๐ต ๐ถ = (๐ฅ โโ ๐ฆ)) |
18 | 9, 17 | syldan 591 |
. . . . 5
โข
(((((๐ด โ
Sโ โง ๐ต โ Sโ )
โง ๐ฅ โ ๐ด) โง ๐ง โ ๐ต) โง ๐ถ = (๐ฅ +โ ๐ง)) โ โ๐ฆ โ ๐ต ๐ถ = (๐ฅ โโ ๐ฆ)) |
19 | 18 | rexlimdva2 3156 |
. . . 4
โข (((๐ด โ
Sโ โง ๐ต โ Sโ )
โง ๐ฅ โ ๐ด) โ (โ๐ง โ ๐ต ๐ถ = (๐ฅ +โ ๐ง) โ โ๐ฆ โ ๐ต ๐ถ = (๐ฅ โโ ๐ฆ))) |
20 | | id 22 |
. . . . . . 7
โข (๐ถ = (๐ฅ โโ ๐ฆ) โ ๐ถ = (๐ฅ โโ ๐ฆ)) |
21 | | shel 30327 |
. . . . . . . . . 10
โข ((๐ต โ
Sโ โง ๐ฆ โ ๐ต) โ ๐ฆ โ โ) |
22 | | hvsubval 30132 |
. . . . . . . . . 10
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (๐ฅ โโ
๐ฆ) = (๐ฅ +โ (-1
ยทโ ๐ฆ))) |
23 | 3, 21, 22 | syl2an 596 |
. . . . . . . . 9
โข (((๐ด โ
Sโ โง ๐ฅ โ ๐ด) โง (๐ต โ Sโ
โง ๐ฆ โ ๐ต)) โ (๐ฅ โโ ๐ฆ) = (๐ฅ +โ (-1
ยทโ ๐ฆ))) |
24 | 23 | an4s 658 |
. . . . . . . 8
โข (((๐ด โ
Sโ โง ๐ต โ Sโ )
โง (๐ฅ โ ๐ด โง ๐ฆ โ ๐ต)) โ (๐ฅ โโ ๐ฆ) = (๐ฅ +โ (-1
ยทโ ๐ฆ))) |
25 | 24 | anassrs 468 |
. . . . . . 7
โข ((((๐ด โ
Sโ โง ๐ต โ Sโ )
โง ๐ฅ โ ๐ด) โง ๐ฆ โ ๐ต) โ (๐ฅ โโ ๐ฆ) = (๐ฅ +โ (-1
ยทโ ๐ฆ))) |
26 | 20, 25 | sylan9eqr 2793 |
. . . . . 6
โข
(((((๐ด โ
Sโ โง ๐ต โ Sโ )
โง ๐ฅ โ ๐ด) โง ๐ฆ โ ๐ต) โง ๐ถ = (๐ฅ โโ ๐ฆ)) โ ๐ถ = (๐ฅ +โ (-1
ยทโ ๐ฆ))) |
27 | | shmulcl 30334 |
. . . . . . . . . 10
โข ((๐ต โ
Sโ โง -1 โ โ โง ๐ฆ โ ๐ต) โ (-1
ยทโ ๐ฆ) โ ๐ต) |
28 | 10, 27 | mp3an2 1449 |
. . . . . . . . 9
โข ((๐ต โ
Sโ โง ๐ฆ โ ๐ต) โ (-1
ยทโ ๐ฆ) โ ๐ต) |
29 | 28 | adantll 712 |
. . . . . . . 8
โข (((๐ด โ
Sโ โง ๐ต โ Sโ )
โง ๐ฆ โ ๐ต) โ (-1
ยทโ ๐ฆ) โ ๐ต) |
30 | 29 | adantlr 713 |
. . . . . . 7
โข ((((๐ด โ
Sโ โง ๐ต โ Sโ )
โง ๐ฅ โ ๐ด) โง ๐ฆ โ ๐ต) โ (-1
ยทโ ๐ฆ) โ ๐ต) |
31 | | oveq2 7401 |
. . . . . . . 8
โข (๐ง = (-1
ยทโ ๐ฆ) โ (๐ฅ +โ ๐ง) = (๐ฅ +โ (-1
ยทโ ๐ฆ))) |
32 | 31 | rspceeqv 3629 |
. . . . . . 7
โข (((-1
ยทโ ๐ฆ) โ ๐ต โง ๐ถ = (๐ฅ +โ (-1
ยทโ ๐ฆ))) โ โ๐ง โ ๐ต ๐ถ = (๐ฅ +โ ๐ง)) |
33 | 30, 32 | sylan 580 |
. . . . . 6
โข
(((((๐ด โ
Sโ โง ๐ต โ Sโ )
โง ๐ฅ โ ๐ด) โง ๐ฆ โ ๐ต) โง ๐ถ = (๐ฅ +โ (-1
ยทโ ๐ฆ))) โ โ๐ง โ ๐ต ๐ถ = (๐ฅ +โ ๐ง)) |
34 | 26, 33 | syldan 591 |
. . . . 5
โข
(((((๐ด โ
Sโ โง ๐ต โ Sโ )
โง ๐ฅ โ ๐ด) โง ๐ฆ โ ๐ต) โง ๐ถ = (๐ฅ โโ ๐ฆ)) โ โ๐ง โ ๐ต ๐ถ = (๐ฅ +โ ๐ง)) |
35 | 34 | rexlimdva2 3156 |
. . . 4
โข (((๐ด โ
Sโ โง ๐ต โ Sโ )
โง ๐ฅ โ ๐ด) โ (โ๐ฆ โ ๐ต ๐ถ = (๐ฅ โโ ๐ฆ) โ โ๐ง โ ๐ต ๐ถ = (๐ฅ +โ ๐ง))) |
36 | 19, 35 | impbid 211 |
. . 3
โข (((๐ด โ
Sโ โง ๐ต โ Sโ )
โง ๐ฅ โ ๐ด) โ (โ๐ง โ ๐ต ๐ถ = (๐ฅ +โ ๐ง) โ โ๐ฆ โ ๐ต ๐ถ = (๐ฅ โโ ๐ฆ))) |
37 | 36 | rexbidva 3175 |
. 2
โข ((๐ด โ
Sโ โง ๐ต โ Sโ )
โ (โ๐ฅ โ
๐ด โ๐ง โ ๐ต ๐ถ = (๐ฅ +โ ๐ง) โ โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ถ = (๐ฅ โโ ๐ฆ))) |
38 | 1, 37 | bitrd 278 |
1
โข ((๐ด โ
Sโ โง ๐ต โ Sโ )
โ (๐ถ โ (๐ด +โ ๐ต) โ โ๐ฅ โ ๐ด โ๐ฆ โ ๐ต ๐ถ = (๐ฅ โโ ๐ฆ))) |