Step | Hyp | Ref
| Expression |
1 | | oveq1 7408 |
. . . . . . . . . . 11
โข (๐ฅ๐ = ๐ฅ โ (๐ฅ๐ ยทs
๐ต) = (๐ฅ ยทs ๐ต)) |
2 | 1 | oveq1d 7416 |
. . . . . . . . . 10
โข (๐ฅ๐ = ๐ฅ โ ((๐ฅ๐ ยทs
๐ต) ยทs
๐ถ) = ((๐ฅ ยทs ๐ต) ยทs ๐ถ)) |
3 | | oveq1 7408 |
. . . . . . . . . 10
โข (๐ฅ๐ = ๐ฅ โ (๐ฅ๐ ยทs
(๐ต ยทs
๐ถ)) = (๐ฅ ยทs (๐ต ยทs ๐ถ))) |
4 | 2, 3 | eqeq12d 2740 |
. . . . . . . . 9
โข (๐ฅ๐ = ๐ฅ โ (((๐ฅ๐ ยทs
๐ต) ยทs
๐ถ) = (๐ฅ๐ ยทs
(๐ต ยทs
๐ถ)) โ ((๐ฅ ยทs ๐ต) ยทs ๐ถ) = (๐ฅ ยทs (๐ต ยทs ๐ถ)))) |
5 | | mulsasslem3.11 |
. . . . . . . . . 10
โข (๐ โ โ๐ฅ๐ โ (( L โ๐ด) โช ( R โ๐ด))((๐ฅ๐ ยทs
๐ต) ยทs
๐ถ) = (๐ฅ๐ ยทs
(๐ต ยทs
๐ถ))) |
6 | 5 | adantr 480 |
. . . . . . . . 9
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ โ๐ฅ๐ โ (( L โ๐ด) โช ( R โ๐ด))((๐ฅ๐ ยทs
๐ต) ยทs
๐ถ) = (๐ฅ๐ ยทs
(๐ต ยทs
๐ถ))) |
7 | | mulsasslem3.4 |
. . . . . . . . . 10
โข ๐ โ (( L โ๐ด) โช ( R โ๐ด)) |
8 | | simprll 776 |
. . . . . . . . . 10
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ๐ฅ โ ๐) |
9 | 7, 8 | sselid 3972 |
. . . . . . . . 9
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ๐ฅ โ (( L โ๐ด) โช ( R โ๐ด))) |
10 | 4, 6, 9 | rspcdva 3605 |
. . . . . . . 8
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ((๐ฅ ยทs ๐ต) ยทs ๐ถ) = (๐ฅ ยทs (๐ต ยทs ๐ถ))) |
11 | | oveq2 7409 |
. . . . . . . . . . . . 13
โข (๐ฆ๐ = ๐ฆ โ (๐ด ยทs ๐ฆ๐) = (๐ด ยทs ๐ฆ)) |
12 | 11 | oveq1d 7416 |
. . . . . . . . . . . 12
โข (๐ฆ๐ = ๐ฆ โ ((๐ด ยทs ๐ฆ๐) ยทs
๐ถ) = ((๐ด ยทs ๐ฆ) ยทs ๐ถ)) |
13 | | oveq1 7408 |
. . . . . . . . . . . . 13
โข (๐ฆ๐ = ๐ฆ โ (๐ฆ๐ ยทs
๐ถ) = (๐ฆ ยทs ๐ถ)) |
14 | 13 | oveq2d 7417 |
. . . . . . . . . . . 12
โข (๐ฆ๐ = ๐ฆ โ (๐ด ยทs (๐ฆ๐ ยทs
๐ถ)) = (๐ด ยทs (๐ฆ ยทs ๐ถ))) |
15 | 12, 14 | eqeq12d 2740 |
. . . . . . . . . . 11
โข (๐ฆ๐ = ๐ฆ โ (((๐ด ยทs ๐ฆ๐) ยทs
๐ถ) = (๐ด ยทs (๐ฆ๐ ยทs
๐ถ)) โ ((๐ด ยทs ๐ฆ) ยทs ๐ถ) = (๐ด ยทs (๐ฆ ยทs ๐ถ)))) |
16 | | mulsasslem3.12 |
. . . . . . . . . . . 12
โข (๐ โ โ๐ฆ๐ โ (( L โ๐ต) โช ( R โ๐ต))((๐ด ยทs ๐ฆ๐) ยทs
๐ถ) = (๐ด ยทs (๐ฆ๐ ยทs
๐ถ))) |
17 | 16 | adantr 480 |
. . . . . . . . . . 11
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ โ๐ฆ๐ โ (( L โ๐ต) โช ( R โ๐ต))((๐ด ยทs ๐ฆ๐) ยทs
๐ถ) = (๐ด ยทs (๐ฆ๐ ยทs
๐ถ))) |
18 | | mulsasslem3.5 |
. . . . . . . . . . . 12
โข ๐ โ (( L โ๐ต) โช ( R โ๐ต)) |
19 | | simprlr 777 |
. . . . . . . . . . . 12
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ๐ฆ โ ๐) |
20 | 18, 19 | sselid 3972 |
. . . . . . . . . . 11
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ๐ฆ โ (( L โ๐ต) โช ( R โ๐ต))) |
21 | 15, 17, 20 | rspcdva 3605 |
. . . . . . . . . 10
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ((๐ด ยทs ๐ฆ) ยทs ๐ถ) = (๐ด ยทs (๐ฆ ยทs ๐ถ))) |
22 | | oveq2 7409 |
. . . . . . . . . . . . . 14
โข (๐ง๐ = ๐ง โ ((๐ด ยทs ๐ต) ยทs ๐ง๐) = ((๐ด ยทs ๐ต) ยทs ๐ง)) |
23 | | oveq2 7409 |
. . . . . . . . . . . . . . 15
โข (๐ง๐ = ๐ง โ (๐ต ยทs ๐ง๐) = (๐ต ยทs ๐ง)) |
24 | 23 | oveq2d 7417 |
. . . . . . . . . . . . . 14
โข (๐ง๐ = ๐ง โ (๐ด ยทs (๐ต ยทs ๐ง๐)) = (๐ด ยทs (๐ต ยทs ๐ง))) |
25 | 22, 24 | eqeq12d 2740 |
. . . . . . . . . . . . 13
โข (๐ง๐ = ๐ง โ (((๐ด ยทs ๐ต) ยทs ๐ง๐) = (๐ด ยทs (๐ต ยทs ๐ง๐)) โ ((๐ด ยทs ๐ต) ยทs ๐ง) = (๐ด ยทs (๐ต ยทs ๐ง)))) |
26 | | mulsasslem3.13 |
. . . . . . . . . . . . . 14
โข (๐ โ โ๐ง๐ โ (( L โ๐ถ) โช ( R โ๐ถ))((๐ด ยทs ๐ต) ยทs ๐ง๐) = (๐ด ยทs (๐ต ยทs ๐ง๐))) |
27 | 26 | adantr 480 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ โ๐ง๐ โ (( L โ๐ถ) โช ( R โ๐ถ))((๐ด ยทs ๐ต) ยทs ๐ง๐) = (๐ด ยทs (๐ต ยทs ๐ง๐))) |
28 | | mulsasslem3.6 |
. . . . . . . . . . . . . 14
โข ๐
โ (( L โ๐ถ) โช ( R โ๐ถ)) |
29 | | simprr 770 |
. . . . . . . . . . . . . 14
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ๐ง โ ๐
) |
30 | 28, 29 | sselid 3972 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ๐ง โ (( L โ๐ถ) โช ( R โ๐ถ))) |
31 | 25, 27, 30 | rspcdva 3605 |
. . . . . . . . . . . 12
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ((๐ด ยทs ๐ต) ยทs ๐ง) = (๐ด ยทs (๐ต ยทs ๐ง))) |
32 | | leftssno 27723 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ( L
โ๐ด) โ No |
33 | | rightssno 27724 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ( R
โ๐ด) โ No |
34 | 32, 33 | unssi 4177 |
. . . . . . . . . . . . . . . . . . . . 21
โข (( L
โ๐ด) โช ( R
โ๐ด)) โ No |
35 | 7, 34 | sstri 3983 |
. . . . . . . . . . . . . . . . . . . 20
โข ๐ โ
No |
36 | 35, 8 | sselid 3972 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ๐ฅ โ No
) |
37 | | mulsasslem3.2 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ ๐ต โ No
) |
38 | 37 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ๐ต โ No
) |
39 | 36, 38 | mulscld 27951 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ (๐ฅ ยทs ๐ต) โ No
) |
40 | | leftssno 27723 |
. . . . . . . . . . . . . . . . . . . . 21
โข ( L
โ๐ถ) โ No |
41 | | rightssno 27724 |
. . . . . . . . . . . . . . . . . . . . 21
โข ( R
โ๐ถ) โ No |
42 | 40, 41 | unssi 4177 |
. . . . . . . . . . . . . . . . . . . 20
โข (( L
โ๐ถ) โช ( R
โ๐ถ)) โ No |
43 | 28, 42 | sstri 3983 |
. . . . . . . . . . . . . . . . . . 19
โข ๐
โ
No |
44 | 43, 29 | sselid 3972 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ๐ง โ No
) |
45 | 39, 44 | mulscld 27951 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ((๐ฅ ยทs ๐ต) ยทs ๐ง) โ No
) |
46 | | mulsasslem3.1 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ ๐ด โ No
) |
47 | 46 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ๐ด โ No
) |
48 | | leftssno 27723 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ( L
โ๐ต) โ No |
49 | | rightssno 27724 |
. . . . . . . . . . . . . . . . . . . . . 22
โข ( R
โ๐ต) โ No |
50 | 48, 49 | unssi 4177 |
. . . . . . . . . . . . . . . . . . . . 21
โข (( L
โ๐ต) โช ( R
โ๐ต)) โ No |
51 | 18, 50 | sstri 3983 |
. . . . . . . . . . . . . . . . . . . 20
โข ๐ โ
No |
52 | 51, 19 | sselid 3972 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ๐ฆ โ No
) |
53 | 47, 52 | mulscld 27951 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ (๐ด ยทs ๐ฆ) โ No
) |
54 | 53, 44 | mulscld 27951 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ((๐ด ยทs ๐ฆ) ยทs ๐ง) โ No
) |
55 | 45, 54 | addscomd 27800 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ (((๐ฅ ยทs ๐ต) ยทs ๐ง) +s ((๐ด ยทs ๐ฆ) ยทs ๐ง)) = (((๐ด ยทs ๐ฆ) ยทs ๐ง) +s ((๐ฅ ยทs ๐ต) ยทs ๐ง))) |
56 | 55 | oveq1d 7416 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ((((๐ฅ ยทs ๐ต) ยทs ๐ง) +s ((๐ด ยทs ๐ฆ) ยทs ๐ง)) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ง)) = ((((๐ด ยทs ๐ฆ) ยทs ๐ง) +s ((๐ฅ ยทs ๐ต) ยทs ๐ง)) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ง))) |
57 | 36, 52 | mulscld 27951 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ (๐ฅ ยทs ๐ฆ) โ No
) |
58 | 57, 44 | mulscld 27951 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ((๐ฅ ยทs ๐ฆ) ยทs ๐ง) โ No
) |
59 | 54, 45, 58 | addsubsassd 27905 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ((((๐ด ยทs ๐ฆ) ยทs ๐ง) +s ((๐ฅ ยทs ๐ต) ยทs ๐ง)) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ง)) = (((๐ด ยทs ๐ฆ) ยทs ๐ง) +s (((๐ฅ ยทs ๐ต) ยทs ๐ง) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ง)))) |
60 | 56, 59 | eqtrd 2764 |
. . . . . . . . . . . . . 14
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ((((๐ฅ ยทs ๐ต) ยทs ๐ง) +s ((๐ด ยทs ๐ฆ) ยทs ๐ง)) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ง)) = (((๐ด ยทs ๐ฆ) ยทs ๐ง) +s (((๐ฅ ยทs ๐ต) ยทs ๐ง) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ง)))) |
61 | 60 | oveq1d 7416 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ (((((๐ฅ ยทs ๐ต) ยทs ๐ง) +s ((๐ด ยทs ๐ฆ) ยทs ๐ง)) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ง)) +s ((๐ฅ ยทs ๐ฆ) ยทs ๐ถ)) = ((((๐ด ยทs ๐ฆ) ยทs ๐ง) +s (((๐ฅ ยทs ๐ต) ยทs ๐ง) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ง))) +s ((๐ฅ ยทs ๐ฆ) ยทs ๐ถ))) |
62 | 45, 58 | subscld 27889 |
. . . . . . . . . . . . . 14
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ (((๐ฅ ยทs ๐ต) ยทs ๐ง) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ง)) โ No
) |
63 | | mulsasslem3.3 |
. . . . . . . . . . . . . . . 16
โข (๐ โ ๐ถ โ No
) |
64 | 63 | adantr 480 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ๐ถ โ No
) |
65 | 57, 64 | mulscld 27951 |
. . . . . . . . . . . . . 14
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ((๐ฅ ยทs ๐ฆ) ยทs ๐ถ) โ No
) |
66 | 54, 62, 65 | addsassd 27839 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ((((๐ด ยทs ๐ฆ) ยทs ๐ง) +s (((๐ฅ ยทs ๐ต) ยทs ๐ง) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ง))) +s ((๐ฅ ยทs ๐ฆ) ยทs ๐ถ)) = (((๐ด ยทs ๐ฆ) ยทs ๐ง) +s ((((๐ฅ ยทs ๐ต) ยทs ๐ง) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ง)) +s ((๐ฅ ยทs ๐ฆ) ยทs ๐ถ)))) |
67 | 11 | oveq1d 7416 |
. . . . . . . . . . . . . . . 16
โข (๐ฆ๐ = ๐ฆ โ ((๐ด ยทs ๐ฆ๐) ยทs
๐ง๐) =
((๐ด ยทs
๐ฆ) ยทs
๐ง๐)) |
68 | | oveq1 7408 |
. . . . . . . . . . . . . . . . 17
โข (๐ฆ๐ = ๐ฆ โ (๐ฆ๐ ยทs
๐ง๐) =
(๐ฆ ยทs
๐ง๐)) |
69 | 68 | oveq2d 7417 |
. . . . . . . . . . . . . . . 16
โข (๐ฆ๐ = ๐ฆ โ (๐ด ยทs (๐ฆ๐ ยทs
๐ง๐)) =
(๐ด ยทs
(๐ฆ ยทs
๐ง๐))) |
70 | 67, 69 | eqeq12d 2740 |
. . . . . . . . . . . . . . 15
โข (๐ฆ๐ = ๐ฆ โ (((๐ด ยทs ๐ฆ๐) ยทs
๐ง๐) =
(๐ด ยทs
(๐ฆ๐
ยทs ๐ง๐)) โ ((๐ด ยทs ๐ฆ) ยทs ๐ง๐) = (๐ด ยทs (๐ฆ ยทs ๐ง๐)))) |
71 | | oveq2 7409 |
. . . . . . . . . . . . . . . 16
โข (๐ง๐ = ๐ง โ ((๐ด ยทs ๐ฆ) ยทs ๐ง๐) = ((๐ด ยทs ๐ฆ) ยทs ๐ง)) |
72 | | oveq2 7409 |
. . . . . . . . . . . . . . . . 17
โข (๐ง๐ = ๐ง โ (๐ฆ ยทs ๐ง๐) = (๐ฆ ยทs ๐ง)) |
73 | 72 | oveq2d 7417 |
. . . . . . . . . . . . . . . 16
โข (๐ง๐ = ๐ง โ (๐ด ยทs (๐ฆ ยทs ๐ง๐)) = (๐ด ยทs (๐ฆ ยทs ๐ง))) |
74 | 71, 73 | eqeq12d 2740 |
. . . . . . . . . . . . . . 15
โข (๐ง๐ = ๐ง โ (((๐ด ยทs ๐ฆ) ยทs ๐ง๐) = (๐ด ยทs (๐ฆ ยทs ๐ง๐)) โ ((๐ด ยทs ๐ฆ) ยทs ๐ง) = (๐ด ยทs (๐ฆ ยทs ๐ง)))) |
75 | | mulsasslem3.10 |
. . . . . . . . . . . . . . . 16
โข (๐ โ โ๐ฆ๐ โ (( L โ๐ต) โช ( R โ๐ต))โ๐ง๐ โ (( L โ๐ถ) โช ( R โ๐ถ))((๐ด ยทs ๐ฆ๐) ยทs
๐ง๐) =
(๐ด ยทs
(๐ฆ๐
ยทs ๐ง๐))) |
76 | 75 | adantr 480 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ โ๐ฆ๐ โ (( L โ๐ต) โช ( R โ๐ต))โ๐ง๐ โ (( L โ๐ถ) โช ( R โ๐ถ))((๐ด ยทs ๐ฆ๐) ยทs
๐ง๐) =
(๐ด ยทs
(๐ฆ๐
ยทs ๐ง๐))) |
77 | 70, 74, 76, 20, 30 | rspc2dv 3618 |
. . . . . . . . . . . . . 14
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ((๐ด ยทs ๐ฆ) ยทs ๐ง) = (๐ด ยทs (๐ฆ ยทs ๐ง))) |
78 | 45, 65, 58 | addsubsd 27906 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ((((๐ฅ ยทs ๐ต) ยทs ๐ง) +s ((๐ฅ ยทs ๐ฆ) ยทs ๐ถ)) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ง)) = ((((๐ฅ ยทs ๐ต) ยทs ๐ง) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ง)) +s ((๐ฅ ยทs ๐ฆ) ยทs ๐ถ))) |
79 | 1 | oveq1d 7416 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ฅ๐ = ๐ฅ โ ((๐ฅ๐ ยทs
๐ต) ยทs
๐ง๐) =
((๐ฅ ยทs
๐ต) ยทs
๐ง๐)) |
80 | | oveq1 7408 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ฅ๐ = ๐ฅ โ (๐ฅ๐ ยทs
(๐ต ยทs
๐ง๐)) =
(๐ฅ ยทs
(๐ต ยทs
๐ง๐))) |
81 | 79, 80 | eqeq12d 2740 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฅ๐ = ๐ฅ โ (((๐ฅ๐ ยทs
๐ต) ยทs
๐ง๐) =
(๐ฅ๐
ยทs (๐ต
ยทs ๐ง๐)) โ ((๐ฅ ยทs ๐ต) ยทs ๐ง๐) = (๐ฅ ยทs (๐ต ยทs ๐ง๐)))) |
82 | | oveq2 7409 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ง๐ = ๐ง โ ((๐ฅ ยทs ๐ต) ยทs ๐ง๐) = ((๐ฅ ยทs ๐ต) ยทs ๐ง)) |
83 | 23 | oveq2d 7417 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ง๐ = ๐ง โ (๐ฅ ยทs (๐ต ยทs ๐ง๐)) = (๐ฅ ยทs (๐ต ยทs ๐ง))) |
84 | 82, 83 | eqeq12d 2740 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ง๐ = ๐ง โ (((๐ฅ ยทs ๐ต) ยทs ๐ง๐) = (๐ฅ ยทs (๐ต ยทs ๐ง๐)) โ ((๐ฅ ยทs ๐ต) ยทs ๐ง) = (๐ฅ ยทs (๐ต ยทs ๐ง)))) |
85 | | mulsasslem3.9 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โ๐ฅ๐ โ (( L โ๐ด) โช ( R โ๐ด))โ๐ง๐ โ (( L โ๐ถ) โช ( R โ๐ถ))((๐ฅ๐ ยทs
๐ต) ยทs
๐ง๐) =
(๐ฅ๐
ยทs (๐ต
ยทs ๐ง๐))) |
86 | 85 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ โ๐ฅ๐ โ (( L โ๐ด) โช ( R โ๐ด))โ๐ง๐ โ (( L โ๐ถ) โช ( R โ๐ถ))((๐ฅ๐ ยทs
๐ต) ยทs
๐ง๐) =
(๐ฅ๐
ยทs (๐ต
ยทs ๐ง๐))) |
87 | 81, 84, 86, 9, 30 | rspc2dv 3618 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ((๐ฅ ยทs ๐ต) ยทs ๐ง) = (๐ฅ ยทs (๐ต ยทs ๐ง))) |
88 | | oveq1 7408 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ฅ๐ = ๐ฅ โ (๐ฅ๐ ยทs
๐ฆ๐) =
(๐ฅ ยทs
๐ฆ๐)) |
89 | 88 | oveq1d 7416 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ฅ๐ = ๐ฅ โ ((๐ฅ๐ ยทs
๐ฆ๐)
ยทs ๐ถ) =
((๐ฅ ยทs
๐ฆ๐)
ยทs ๐ถ)) |
90 | | oveq1 7408 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ฅ๐ = ๐ฅ โ (๐ฅ๐ ยทs
(๐ฆ๐
ยทs ๐ถ)) =
(๐ฅ ยทs
(๐ฆ๐
ยทs ๐ถ))) |
91 | 89, 90 | eqeq12d 2740 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฅ๐ = ๐ฅ โ (((๐ฅ๐ ยทs
๐ฆ๐)
ยทs ๐ถ) =
(๐ฅ๐
ยทs (๐ฆ๐ ยทs
๐ถ)) โ ((๐ฅ ยทs ๐ฆ๐)
ยทs ๐ถ) =
(๐ฅ ยทs
(๐ฆ๐
ยทs ๐ถ)))) |
92 | | oveq2 7409 |
. . . . . . . . . . . . . . . . . . . . 21
โข (๐ฆ๐ = ๐ฆ โ (๐ฅ ยทs ๐ฆ๐) = (๐ฅ ยทs ๐ฆ)) |
93 | 92 | oveq1d 7416 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ฆ๐ = ๐ฆ โ ((๐ฅ ยทs ๐ฆ๐) ยทs
๐ถ) = ((๐ฅ ยทs ๐ฆ) ยทs ๐ถ)) |
94 | 13 | oveq2d 7417 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ฆ๐ = ๐ฆ โ (๐ฅ ยทs (๐ฆ๐ ยทs
๐ถ)) = (๐ฅ ยทs (๐ฆ ยทs ๐ถ))) |
95 | 93, 94 | eqeq12d 2740 |
. . . . . . . . . . . . . . . . . . 19
โข (๐ฆ๐ = ๐ฆ โ (((๐ฅ ยทs ๐ฆ๐) ยทs
๐ถ) = (๐ฅ ยทs (๐ฆ๐ ยทs
๐ถ)) โ ((๐ฅ ยทs ๐ฆ) ยทs ๐ถ) = (๐ฅ ยทs (๐ฆ ยทs ๐ถ)))) |
96 | | mulsasslem3.8 |
. . . . . . . . . . . . . . . . . . . 20
โข (๐ โ โ๐ฅ๐ โ (( L โ๐ด) โช ( R โ๐ด))โ๐ฆ๐ โ (( L โ๐ต) โช ( R โ๐ต))((๐ฅ๐ ยทs
๐ฆ๐)
ยทs ๐ถ) =
(๐ฅ๐
ยทs (๐ฆ๐ ยทs
๐ถ))) |
97 | 96 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ โ๐ฅ๐ โ (( L โ๐ด) โช ( R โ๐ด))โ๐ฆ๐ โ (( L โ๐ต) โช ( R โ๐ต))((๐ฅ๐ ยทs
๐ฆ๐)
ยทs ๐ถ) =
(๐ฅ๐
ยทs (๐ฆ๐ ยทs
๐ถ))) |
98 | 91, 95, 97, 9, 20 | rspc2dv 3618 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ((๐ฅ ยทs ๐ฆ) ยทs ๐ถ) = (๐ฅ ยทs (๐ฆ ยทs ๐ถ))) |
99 | 87, 98 | oveq12d 7419 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ (((๐ฅ ยทs ๐ต) ยทs ๐ง) +s ((๐ฅ ยทs ๐ฆ) ยทs ๐ถ)) = ((๐ฅ ยทs (๐ต ยทs ๐ง)) +s (๐ฅ ยทs (๐ฆ ยทs ๐ถ)))) |
100 | 38, 44 | mulscld 27951 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ (๐ต ยทs ๐ง) โ No
) |
101 | 36, 100 | mulscld 27951 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ (๐ฅ ยทs (๐ต ยทs ๐ง)) โ No
) |
102 | 52, 64 | mulscld 27951 |
. . . . . . . . . . . . . . . . . . 19
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ (๐ฆ ยทs ๐ถ) โ No
) |
103 | 36, 102 | mulscld 27951 |
. . . . . . . . . . . . . . . . . 18
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ (๐ฅ ยทs (๐ฆ ยทs ๐ถ)) โ No
) |
104 | 101, 103 | addscomd 27800 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ((๐ฅ ยทs (๐ต ยทs ๐ง)) +s (๐ฅ ยทs (๐ฆ ยทs ๐ถ))) = ((๐ฅ ยทs (๐ฆ ยทs ๐ถ)) +s (๐ฅ ยทs (๐ต ยทs ๐ง)))) |
105 | 99, 104 | eqtrd 2764 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ (((๐ฅ ยทs ๐ต) ยทs ๐ง) +s ((๐ฅ ยทs ๐ฆ) ยทs ๐ถ)) = ((๐ฅ ยทs (๐ฆ ยทs ๐ถ)) +s (๐ฅ ยทs (๐ต ยทs ๐ง)))) |
106 | 88 | oveq1d 7416 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฅ๐ = ๐ฅ โ ((๐ฅ๐ ยทs
๐ฆ๐)
ยทs ๐ง๐) = ((๐ฅ ยทs ๐ฆ๐) ยทs
๐ง๐)) |
107 | | oveq1 7408 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฅ๐ = ๐ฅ โ (๐ฅ๐ ยทs
(๐ฆ๐
ยทs ๐ง๐)) = (๐ฅ ยทs (๐ฆ๐ ยทs
๐ง๐))) |
108 | 106, 107 | eqeq12d 2740 |
. . . . . . . . . . . . . . . . 17
โข (๐ฅ๐ = ๐ฅ โ (((๐ฅ๐ ยทs
๐ฆ๐)
ยทs ๐ง๐) = (๐ฅ๐ ยทs
(๐ฆ๐
ยทs ๐ง๐)) โ ((๐ฅ ยทs ๐ฆ๐)
ยทs ๐ง๐) = (๐ฅ ยทs (๐ฆ๐ ยทs
๐ง๐)))) |
109 | 92 | oveq1d 7416 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฆ๐ = ๐ฆ โ ((๐ฅ ยทs ๐ฆ๐) ยทs
๐ง๐) =
((๐ฅ ยทs
๐ฆ) ยทs
๐ง๐)) |
110 | 68 | oveq2d 7417 |
. . . . . . . . . . . . . . . . . 18
โข (๐ฆ๐ = ๐ฆ โ (๐ฅ ยทs (๐ฆ๐ ยทs
๐ง๐)) =
(๐ฅ ยทs
(๐ฆ ยทs
๐ง๐))) |
111 | 109, 110 | eqeq12d 2740 |
. . . . . . . . . . . . . . . . 17
โข (๐ฆ๐ = ๐ฆ โ (((๐ฅ ยทs ๐ฆ๐) ยทs
๐ง๐) =
(๐ฅ ยทs
(๐ฆ๐
ยทs ๐ง๐)) โ ((๐ฅ ยทs ๐ฆ) ยทs ๐ง๐) = (๐ฅ ยทs (๐ฆ ยทs ๐ง๐)))) |
112 | | oveq2 7409 |
. . . . . . . . . . . . . . . . . 18
โข (๐ง๐ = ๐ง โ ((๐ฅ ยทs ๐ฆ) ยทs ๐ง๐) = ((๐ฅ ยทs ๐ฆ) ยทs ๐ง)) |
113 | 72 | oveq2d 7417 |
. . . . . . . . . . . . . . . . . 18
โข (๐ง๐ = ๐ง โ (๐ฅ ยทs (๐ฆ ยทs ๐ง๐)) = (๐ฅ ยทs (๐ฆ ยทs ๐ง))) |
114 | 112, 113 | eqeq12d 2740 |
. . . . . . . . . . . . . . . . 17
โข (๐ง๐ = ๐ง โ (((๐ฅ ยทs ๐ฆ) ยทs ๐ง๐) = (๐ฅ ยทs (๐ฆ ยทs ๐ง๐)) โ ((๐ฅ ยทs ๐ฆ) ยทs ๐ง) = (๐ฅ ยทs (๐ฆ ยทs ๐ง)))) |
115 | | mulsasslem3.7 |
. . . . . . . . . . . . . . . . . 18
โข (๐ โ โ๐ฅ๐ โ (( L โ๐ด) โช ( R โ๐ด))โ๐ฆ๐ โ (( L โ๐ต) โช ( R โ๐ต))โ๐ง๐ โ (( L โ๐ถ) โช ( R โ๐ถ))((๐ฅ๐ ยทs
๐ฆ๐)
ยทs ๐ง๐) = (๐ฅ๐ ยทs
(๐ฆ๐
ยทs ๐ง๐))) |
116 | 115 | adantr 480 |
. . . . . . . . . . . . . . . . 17
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ โ๐ฅ๐ โ (( L โ๐ด) โช ( R โ๐ด))โ๐ฆ๐ โ (( L โ๐ต) โช ( R โ๐ต))โ๐ง๐ โ (( L โ๐ถ) โช ( R โ๐ถ))((๐ฅ๐ ยทs
๐ฆ๐)
ยทs ๐ง๐) = (๐ฅ๐ ยทs
(๐ฆ๐
ยทs ๐ง๐))) |
117 | 108, 111,
114, 116, 9, 20, 30 | rspc3dv 3621 |
. . . . . . . . . . . . . . . 16
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ((๐ฅ ยทs ๐ฆ) ยทs ๐ง) = (๐ฅ ยทs (๐ฆ ยทs ๐ง))) |
118 | 105, 117 | oveq12d 7419 |
. . . . . . . . . . . . . . 15
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ((((๐ฅ ยทs ๐ต) ยทs ๐ง) +s ((๐ฅ ยทs ๐ฆ) ยทs ๐ถ)) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ง)) = (((๐ฅ ยทs (๐ฆ ยทs ๐ถ)) +s (๐ฅ ยทs (๐ต ยทs ๐ง))) -s (๐ฅ ยทs (๐ฆ ยทs ๐ง)))) |
119 | 78, 118 | eqtr3d 2766 |
. . . . . . . . . . . . . 14
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ((((๐ฅ ยทs ๐ต) ยทs ๐ง) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ง)) +s ((๐ฅ ยทs ๐ฆ) ยทs ๐ถ)) = (((๐ฅ ยทs (๐ฆ ยทs ๐ถ)) +s (๐ฅ ยทs (๐ต ยทs ๐ง))) -s (๐ฅ ยทs (๐ฆ ยทs ๐ง)))) |
120 | 77, 119 | oveq12d 7419 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ (((๐ด ยทs ๐ฆ) ยทs ๐ง) +s ((((๐ฅ ยทs ๐ต) ยทs ๐ง) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ง)) +s ((๐ฅ ยทs ๐ฆ) ยทs ๐ถ))) = ((๐ด ยทs (๐ฆ ยทs ๐ง)) +s (((๐ฅ ยทs (๐ฆ ยทs ๐ถ)) +s (๐ฅ ยทs (๐ต ยทs ๐ง))) -s (๐ฅ ยทs (๐ฆ ยทs ๐ง))))) |
121 | 61, 66, 120 | 3eqtrd 2768 |
. . . . . . . . . . . 12
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ (((((๐ฅ ยทs ๐ต) ยทs ๐ง) +s ((๐ด ยทs ๐ฆ) ยทs ๐ง)) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ง)) +s ((๐ฅ ยทs ๐ฆ) ยทs ๐ถ)) = ((๐ด ยทs (๐ฆ ยทs ๐ง)) +s (((๐ฅ ยทs (๐ฆ ยทs ๐ถ)) +s (๐ฅ ยทs (๐ต ยทs ๐ง))) -s (๐ฅ ยทs (๐ฆ ยทs ๐ง))))) |
122 | 31, 121 | oveq12d 7419 |
. . . . . . . . . . 11
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ (((๐ด ยทs ๐ต) ยทs ๐ง) -s (((((๐ฅ ยทs ๐ต) ยทs ๐ง) +s ((๐ด ยทs ๐ฆ) ยทs ๐ง)) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ง)) +s ((๐ฅ ยทs ๐ฆ) ยทs ๐ถ))) = ((๐ด ยทs (๐ต ยทs ๐ง)) -s ((๐ด ยทs (๐ฆ ยทs ๐ง)) +s (((๐ฅ ยทs (๐ฆ ยทs ๐ถ)) +s (๐ฅ ยทs (๐ต ยทs ๐ง))) -s (๐ฅ ยทs (๐ฆ ยทs ๐ง)))))) |
123 | 47, 38 | mulscld 27951 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ (๐ด ยทs ๐ต) โ No
) |
124 | 123, 44 | mulscld 27951 |
. . . . . . . . . . . 12
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ((๐ด ยทs ๐ต) ยทs ๐ง) โ No
) |
125 | 45, 54 | addscld 27813 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ (((๐ฅ ยทs ๐ต) ยทs ๐ง) +s ((๐ด ยทs ๐ฆ) ยทs ๐ง)) โ No
) |
126 | 125, 58 | subscld 27889 |
. . . . . . . . . . . 12
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ((((๐ฅ ยทs ๐ต) ยทs ๐ง) +s ((๐ด ยทs ๐ฆ) ยทs ๐ง)) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ง)) โ No
) |
127 | 124, 126,
65 | subsubs4d 27917 |
. . . . . . . . . . 11
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ((((๐ด ยทs ๐ต) ยทs ๐ง) -s ((((๐ฅ ยทs ๐ต) ยทs ๐ง) +s ((๐ด ยทs ๐ฆ) ยทs ๐ง)) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ง))) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ถ)) = (((๐ด ยทs ๐ต) ยทs ๐ง) -s (((((๐ฅ ยทs ๐ต) ยทs ๐ง) +s ((๐ด ยทs ๐ฆ) ยทs ๐ง)) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ง)) +s ((๐ฅ ยทs ๐ฆ) ยทs ๐ถ)))) |
128 | 47, 100 | mulscld 27951 |
. . . . . . . . . . . 12
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ (๐ด ยทs (๐ต ยทs ๐ง)) โ No
) |
129 | 52, 44 | mulscld 27951 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ (๐ฆ ยทs ๐ง) โ No
) |
130 | 47, 129 | mulscld 27951 |
. . . . . . . . . . . 12
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ (๐ด ยทs (๐ฆ ยทs ๐ง)) โ No
) |
131 | 103, 101 | addscld 27813 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ((๐ฅ ยทs (๐ฆ ยทs ๐ถ)) +s (๐ฅ ยทs (๐ต ยทs ๐ง))) โ No
) |
132 | 36, 129 | mulscld 27951 |
. . . . . . . . . . . . 13
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ (๐ฅ ยทs (๐ฆ ยทs ๐ง)) โ No
) |
133 | 131, 132 | subscld 27889 |
. . . . . . . . . . . 12
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ (((๐ฅ ยทs (๐ฆ ยทs ๐ถ)) +s (๐ฅ ยทs (๐ต ยทs ๐ง))) -s (๐ฅ ยทs (๐ฆ ยทs ๐ง))) โ No
) |
134 | 128, 130,
133 | subsubs4d 27917 |
. . . . . . . . . . 11
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ (((๐ด ยทs (๐ต ยทs ๐ง)) -s (๐ด ยทs (๐ฆ ยทs ๐ง))) -s (((๐ฅ ยทs (๐ฆ ยทs ๐ถ)) +s (๐ฅ ยทs (๐ต ยทs ๐ง))) -s (๐ฅ ยทs (๐ฆ ยทs ๐ง)))) = ((๐ด ยทs (๐ต ยทs ๐ง)) -s ((๐ด ยทs (๐ฆ ยทs ๐ง)) +s (((๐ฅ ยทs (๐ฆ ยทs ๐ถ)) +s (๐ฅ ยทs (๐ต ยทs ๐ง))) -s (๐ฅ ยทs (๐ฆ ยทs ๐ง)))))) |
135 | 122, 127,
134 | 3eqtr4d 2774 |
. . . . . . . . . 10
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ((((๐ด ยทs ๐ต) ยทs ๐ง) -s ((((๐ฅ ยทs ๐ต) ยทs ๐ง) +s ((๐ด ยทs ๐ฆ) ยทs ๐ง)) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ง))) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ถ)) = (((๐ด ยทs (๐ต ยทs ๐ง)) -s (๐ด ยทs (๐ฆ ยทs ๐ง))) -s (((๐ฅ ยทs (๐ฆ ยทs ๐ถ)) +s (๐ฅ ยทs (๐ต ยทs ๐ง))) -s (๐ฅ ยทs (๐ฆ ยทs ๐ง))))) |
136 | 21, 135 | oveq12d 7419 |
. . . . . . . . 9
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ (((๐ด ยทs ๐ฆ) ยทs ๐ถ) +s ((((๐ด ยทs ๐ต) ยทs ๐ง) -s ((((๐ฅ ยทs ๐ต) ยทs ๐ง) +s ((๐ด ยทs ๐ฆ) ยทs ๐ง)) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ง))) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ถ))) = ((๐ด ยทs (๐ฆ ยทs ๐ถ)) +s (((๐ด ยทs (๐ต ยทs ๐ง)) -s (๐ด ยทs (๐ฆ ยทs ๐ง))) -s (((๐ฅ ยทs (๐ฆ ยทs ๐ถ)) +s (๐ฅ ยทs (๐ต ยทs ๐ง))) -s (๐ฅ ยทs (๐ฆ ยทs ๐ง)))))) |
137 | 53, 64 | mulscld 27951 |
. . . . . . . . . . 11
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ((๐ด ยทs ๐ฆ) ยทs ๐ถ) โ No
) |
138 | 124, 126 | subscld 27889 |
. . . . . . . . . . 11
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ (((๐ด ยทs ๐ต) ยทs ๐ง) -s ((((๐ฅ ยทs ๐ต) ยทs ๐ง) +s ((๐ด ยทs ๐ฆ) ยทs ๐ง)) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ง))) โ No
) |
139 | 137, 138,
65 | addsubsd 27906 |
. . . . . . . . . 10
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ((((๐ด ยทs ๐ฆ) ยทs ๐ถ) +s (((๐ด ยทs ๐ต) ยทs ๐ง) -s ((((๐ฅ ยทs ๐ต) ยทs ๐ง) +s ((๐ด ยทs ๐ฆ) ยทs ๐ง)) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ง)))) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ถ)) = ((((๐ด ยทs ๐ฆ) ยทs ๐ถ) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ถ)) +s (((๐ด ยทs ๐ต) ยทs ๐ง) -s ((((๐ฅ ยทs ๐ต) ยทs ๐ง) +s ((๐ด ยทs ๐ฆ) ยทs ๐ง)) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ง))))) |
140 | 137, 138,
65 | addsubsassd 27905 |
. . . . . . . . . 10
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ((((๐ด ยทs ๐ฆ) ยทs ๐ถ) +s (((๐ด ยทs ๐ต) ยทs ๐ง) -s ((((๐ฅ ยทs ๐ต) ยทs ๐ง) +s ((๐ด ยทs ๐ฆ) ยทs ๐ง)) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ง)))) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ถ)) = (((๐ด ยทs ๐ฆ) ยทs ๐ถ) +s ((((๐ด ยทs ๐ต) ยทs ๐ง) -s ((((๐ฅ ยทs ๐ต) ยทs ๐ง) +s ((๐ด ยทs ๐ฆ) ยทs ๐ง)) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ง))) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ถ)))) |
141 | 139, 140 | eqtr3d 2766 |
. . . . . . . . 9
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ((((๐ด ยทs ๐ฆ) ยทs ๐ถ) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ถ)) +s (((๐ด ยทs ๐ต) ยทs ๐ง) -s ((((๐ฅ ยทs ๐ต) ยทs ๐ง) +s ((๐ด ยทs ๐ฆ) ยทs ๐ง)) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ง)))) = (((๐ด ยทs ๐ฆ) ยทs ๐ถ) +s ((((๐ด ยทs ๐ต) ยทs ๐ง) -s ((((๐ฅ ยทs ๐ต) ยทs ๐ง) +s ((๐ด ยทs ๐ฆ) ยทs ๐ง)) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ง))) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ถ)))) |
142 | 47, 102 | mulscld 27951 |
. . . . . . . . . . . 12
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ (๐ด ยทs (๐ฆ ยทs ๐ถ)) โ No
) |
143 | 142, 128,
130 | addsubsassd 27905 |
. . . . . . . . . . 11
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ (((๐ด ยทs (๐ฆ ยทs ๐ถ)) +s (๐ด ยทs (๐ต ยทs ๐ง))) -s (๐ด ยทs (๐ฆ ยทs ๐ง))) = ((๐ด ยทs (๐ฆ ยทs ๐ถ)) +s ((๐ด ยทs (๐ต ยทs ๐ง)) -s (๐ด ยทs (๐ฆ ยทs ๐ง))))) |
144 | 143 | oveq1d 7416 |
. . . . . . . . . 10
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ((((๐ด ยทs (๐ฆ ยทs ๐ถ)) +s (๐ด ยทs (๐ต ยทs ๐ง))) -s (๐ด ยทs (๐ฆ ยทs ๐ง))) -s (((๐ฅ ยทs (๐ฆ ยทs ๐ถ)) +s (๐ฅ ยทs (๐ต ยทs ๐ง))) -s (๐ฅ ยทs (๐ฆ ยทs ๐ง)))) = (((๐ด ยทs (๐ฆ ยทs ๐ถ)) +s ((๐ด ยทs (๐ต ยทs ๐ง)) -s (๐ด ยทs (๐ฆ ยทs ๐ง)))) -s (((๐ฅ ยทs (๐ฆ ยทs ๐ถ)) +s (๐ฅ ยทs (๐ต ยทs ๐ง))) -s (๐ฅ ยทs (๐ฆ ยทs ๐ง))))) |
145 | 128, 130 | subscld 27889 |
. . . . . . . . . . 11
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ((๐ด ยทs (๐ต ยทs ๐ง)) -s (๐ด ยทs (๐ฆ ยทs ๐ง))) โ No
) |
146 | 142, 145,
133 | addsubsassd 27905 |
. . . . . . . . . 10
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ (((๐ด ยทs (๐ฆ ยทs ๐ถ)) +s ((๐ด ยทs (๐ต ยทs ๐ง)) -s (๐ด ยทs (๐ฆ ยทs ๐ง)))) -s (((๐ฅ ยทs (๐ฆ ยทs ๐ถ)) +s (๐ฅ ยทs (๐ต ยทs ๐ง))) -s (๐ฅ ยทs (๐ฆ ยทs ๐ง)))) = ((๐ด ยทs (๐ฆ ยทs ๐ถ)) +s (((๐ด ยทs (๐ต ยทs ๐ง)) -s (๐ด ยทs (๐ฆ ยทs ๐ง))) -s (((๐ฅ ยทs (๐ฆ ยทs ๐ถ)) +s (๐ฅ ยทs (๐ต ยทs ๐ง))) -s (๐ฅ ยทs (๐ฆ ยทs ๐ง)))))) |
147 | 144, 146 | eqtrd 2764 |
. . . . . . . . 9
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ((((๐ด ยทs (๐ฆ ยทs ๐ถ)) +s (๐ด ยทs (๐ต ยทs ๐ง))) -s (๐ด ยทs (๐ฆ ยทs ๐ง))) -s (((๐ฅ ยทs (๐ฆ ยทs ๐ถ)) +s (๐ฅ ยทs (๐ต ยทs ๐ง))) -s (๐ฅ ยทs (๐ฆ ยทs ๐ง)))) = ((๐ด ยทs (๐ฆ ยทs ๐ถ)) +s (((๐ด ยทs (๐ต ยทs ๐ง)) -s (๐ด ยทs (๐ฆ ยทs ๐ง))) -s (((๐ฅ ยทs (๐ฆ ยทs ๐ถ)) +s (๐ฅ ยทs (๐ต ยทs ๐ง))) -s (๐ฅ ยทs (๐ฆ ยทs ๐ง)))))) |
148 | 136, 141,
147 | 3eqtr4d 2774 |
. . . . . . . 8
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ((((๐ด ยทs ๐ฆ) ยทs ๐ถ) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ถ)) +s (((๐ด ยทs ๐ต) ยทs ๐ง) -s ((((๐ฅ ยทs ๐ต) ยทs ๐ง) +s ((๐ด ยทs ๐ฆ) ยทs ๐ง)) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ง)))) = ((((๐ด ยทs (๐ฆ ยทs ๐ถ)) +s (๐ด ยทs (๐ต ยทs ๐ง))) -s (๐ด ยทs (๐ฆ ยทs ๐ง))) -s (((๐ฅ ยทs (๐ฆ ยทs ๐ถ)) +s (๐ฅ ยทs (๐ต ยทs ๐ง))) -s (๐ฅ ยทs (๐ฆ ยทs ๐ง))))) |
149 | 10, 148 | oveq12d 7419 |
. . . . . . 7
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ (((๐ฅ ยทs ๐ต) ยทs ๐ถ) +s ((((๐ด ยทs ๐ฆ) ยทs ๐ถ) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ถ)) +s (((๐ด ยทs ๐ต) ยทs ๐ง) -s ((((๐ฅ ยทs ๐ต) ยทs ๐ง) +s ((๐ด ยทs ๐ฆ) ยทs ๐ง)) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ง))))) = ((๐ฅ ยทs (๐ต ยทs ๐ถ)) +s ((((๐ด ยทs (๐ฆ ยทs ๐ถ)) +s (๐ด ยทs (๐ต ยทs ๐ง))) -s (๐ด ยทs (๐ฆ ยทs ๐ง))) -s (((๐ฅ ยทs (๐ฆ ยทs ๐ถ)) +s (๐ฅ ยทs (๐ต ยทs ๐ง))) -s (๐ฅ ยทs (๐ฆ ยทs ๐ง)))))) |
150 | 39, 64 | mulscld 27951 |
. . . . . . . . . . 11
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ((๐ฅ ยทs ๐ต) ยทs ๐ถ) โ No
) |
151 | 150, 137 | addscld 27813 |
. . . . . . . . . 10
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ (((๐ฅ ยทs ๐ต) ยทs ๐ถ) +s ((๐ด ยทs ๐ฆ) ยทs ๐ถ)) โ No
) |
152 | 151, 65 | subscld 27889 |
. . . . . . . . 9
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ((((๐ฅ ยทs ๐ต) ยทs ๐ถ) +s ((๐ด ยทs ๐ฆ) ยทs ๐ถ)) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ถ)) โ No
) |
153 | 152, 124,
126 | addsubsassd 27905 |
. . . . . . . 8
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ((((((๐ฅ ยทs ๐ต) ยทs ๐ถ) +s ((๐ด ยทs ๐ฆ) ยทs ๐ถ)) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ถ)) +s ((๐ด ยทs ๐ต) ยทs ๐ง)) -s ((((๐ฅ ยทs ๐ต) ยทs ๐ง) +s ((๐ด ยทs ๐ฆ) ยทs ๐ง)) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ง))) = (((((๐ฅ ยทs ๐ต) ยทs ๐ถ) +s ((๐ด ยทs ๐ฆ) ยทs ๐ถ)) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ถ)) +s (((๐ด ยทs ๐ต) ยทs ๐ง) -s ((((๐ฅ ยทs ๐ต) ยทs ๐ง) +s ((๐ด ยทs ๐ฆ) ยทs ๐ง)) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ง))))) |
154 | 150, 137,
65 | addsubsassd 27905 |
. . . . . . . . 9
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ((((๐ฅ ยทs ๐ต) ยทs ๐ถ) +s ((๐ด ยทs ๐ฆ) ยทs ๐ถ)) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ถ)) = (((๐ฅ ยทs ๐ต) ยทs ๐ถ) +s (((๐ด ยทs ๐ฆ) ยทs ๐ถ) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ถ)))) |
155 | 154 | oveq1d 7416 |
. . . . . . . 8
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ (((((๐ฅ ยทs ๐ต) ยทs ๐ถ) +s ((๐ด ยทs ๐ฆ) ยทs ๐ถ)) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ถ)) +s (((๐ด ยทs ๐ต) ยทs ๐ง) -s ((((๐ฅ ยทs ๐ต) ยทs ๐ง) +s ((๐ด ยทs ๐ฆ) ยทs ๐ง)) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ง)))) = ((((๐ฅ ยทs ๐ต) ยทs ๐ถ) +s (((๐ด ยทs ๐ฆ) ยทs ๐ถ) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ถ))) +s (((๐ด ยทs ๐ต) ยทs ๐ง) -s ((((๐ฅ ยทs ๐ต) ยทs ๐ง) +s ((๐ด ยทs ๐ฆ) ยทs ๐ง)) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ง))))) |
156 | 137, 65 | subscld 27889 |
. . . . . . . . 9
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ (((๐ด ยทs ๐ฆ) ยทs ๐ถ) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ถ)) โ No
) |
157 | 150, 156,
138 | addsassd 27839 |
. . . . . . . 8
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ((((๐ฅ ยทs ๐ต) ยทs ๐ถ) +s (((๐ด ยทs ๐ฆ) ยทs ๐ถ) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ถ))) +s (((๐ด ยทs ๐ต) ยทs ๐ง) -s ((((๐ฅ ยทs ๐ต) ยทs ๐ง) +s ((๐ด ยทs ๐ฆ) ยทs ๐ง)) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ง)))) = (((๐ฅ ยทs ๐ต) ยทs ๐ถ) +s ((((๐ด ยทs ๐ฆ) ยทs ๐ถ) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ถ)) +s (((๐ด ยทs ๐ต) ยทs ๐ง) -s ((((๐ฅ ยทs ๐ต) ยทs ๐ง) +s ((๐ด ยทs ๐ฆ) ยทs ๐ง)) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ง)))))) |
158 | 153, 155,
157 | 3eqtrd 2768 |
. . . . . . 7
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ((((((๐ฅ ยทs ๐ต) ยทs ๐ถ) +s ((๐ด ยทs ๐ฆ) ยทs ๐ถ)) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ถ)) +s ((๐ด ยทs ๐ต) ยทs ๐ง)) -s ((((๐ฅ ยทs ๐ต) ยทs ๐ง) +s ((๐ด ยทs ๐ฆ) ยทs ๐ง)) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ง))) = (((๐ฅ ยทs ๐ต) ยทs ๐ถ) +s ((((๐ด ยทs ๐ฆ) ยทs ๐ถ) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ถ)) +s (((๐ด ยทs ๐ต) ยทs ๐ง) -s ((((๐ฅ ยทs ๐ต) ยทs ๐ง) +s ((๐ด ยทs ๐ฆ) ยทs ๐ง)) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ง)))))) |
159 | 38, 64 | mulscld 27951 |
. . . . . . . . 9
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ (๐ต ยทs ๐ถ) โ No
) |
160 | 36, 159 | mulscld 27951 |
. . . . . . . 8
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ (๐ฅ ยทs (๐ต ยทs ๐ถ)) โ No
) |
161 | 142, 128 | addscld 27813 |
. . . . . . . . 9
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ((๐ด ยทs (๐ฆ ยทs ๐ถ)) +s (๐ด ยทs (๐ต ยทs ๐ง))) โ No
) |
162 | 161, 130 | subscld 27889 |
. . . . . . . 8
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ (((๐ด ยทs (๐ฆ ยทs ๐ถ)) +s (๐ด ยทs (๐ต ยทs ๐ง))) -s (๐ด ยทs (๐ฆ ยทs ๐ง))) โ No
) |
163 | 160, 162,
133 | addsubsassd 27905 |
. . . . . . 7
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ (((๐ฅ ยทs (๐ต ยทs ๐ถ)) +s (((๐ด ยทs (๐ฆ ยทs ๐ถ)) +s (๐ด ยทs (๐ต ยทs ๐ง))) -s (๐ด ยทs (๐ฆ ยทs ๐ง)))) -s (((๐ฅ ยทs (๐ฆ ยทs ๐ถ)) +s (๐ฅ ยทs (๐ต ยทs ๐ง))) -s (๐ฅ ยทs (๐ฆ ยทs ๐ง)))) = ((๐ฅ ยทs (๐ต ยทs ๐ถ)) +s ((((๐ด ยทs (๐ฆ ยทs ๐ถ)) +s (๐ด ยทs (๐ต ยทs ๐ง))) -s (๐ด ยทs (๐ฆ ยทs ๐ง))) -s (((๐ฅ ยทs (๐ฆ ยทs ๐ถ)) +s (๐ฅ ยทs (๐ต ยทs ๐ง))) -s (๐ฅ ยทs (๐ฆ ยทs ๐ง)))))) |
164 | 149, 158,
163 | 3eqtr4d 2774 |
. . . . . 6
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ((((((๐ฅ ยทs ๐ต) ยทs ๐ถ) +s ((๐ด ยทs ๐ฆ) ยทs ๐ถ)) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ถ)) +s ((๐ด ยทs ๐ต) ยทs ๐ง)) -s ((((๐ฅ ยทs ๐ต) ยทs ๐ง) +s ((๐ด ยทs ๐ฆ) ยทs ๐ง)) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ง))) = (((๐ฅ ยทs (๐ต ยทs ๐ถ)) +s (((๐ด ยทs (๐ฆ ยทs ๐ถ)) +s (๐ด ยทs (๐ต ยทs ๐ง))) -s (๐ด ยทs (๐ฆ ยทs ๐ง)))) -s (((๐ฅ ยทs (๐ฆ ยทs ๐ถ)) +s (๐ฅ ยทs (๐ต ยทs ๐ง))) -s (๐ฅ ยทs (๐ฆ ยทs ๐ง))))) |
165 | 39, 53 | addscld 27813 |
. . . . . . . . . 10
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ((๐ฅ ยทs ๐ต) +s (๐ด ยทs ๐ฆ)) โ No
) |
166 | 165, 57, 64 | subsdird 27975 |
. . . . . . . . 9
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ((((๐ฅ ยทs ๐ต) +s (๐ด ยทs ๐ฆ)) -s (๐ฅ ยทs ๐ฆ)) ยทs ๐ถ) = ((((๐ฅ ยทs ๐ต) +s (๐ด ยทs ๐ฆ)) ยทs ๐ถ) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ถ))) |
167 | 39, 53, 64 | addsdird 27973 |
. . . . . . . . . 10
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ (((๐ฅ ยทs ๐ต) +s (๐ด ยทs ๐ฆ)) ยทs ๐ถ) = (((๐ฅ ยทs ๐ต) ยทs ๐ถ) +s ((๐ด ยทs ๐ฆ) ยทs ๐ถ))) |
168 | 167 | oveq1d 7416 |
. . . . . . . . 9
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ((((๐ฅ ยทs ๐ต) +s (๐ด ยทs ๐ฆ)) ยทs ๐ถ) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ถ)) = ((((๐ฅ ยทs ๐ต) ยทs ๐ถ) +s ((๐ด ยทs ๐ฆ) ยทs ๐ถ)) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ถ))) |
169 | 166, 168 | eqtrd 2764 |
. . . . . . . 8
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ((((๐ฅ ยทs ๐ต) +s (๐ด ยทs ๐ฆ)) -s (๐ฅ ยทs ๐ฆ)) ยทs ๐ถ) = ((((๐ฅ ยทs ๐ต) ยทs ๐ถ) +s ((๐ด ยทs ๐ฆ) ยทs ๐ถ)) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ถ))) |
170 | 169 | oveq1d 7416 |
. . . . . . 7
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ (((((๐ฅ ยทs ๐ต) +s (๐ด ยทs ๐ฆ)) -s (๐ฅ ยทs ๐ฆ)) ยทs ๐ถ) +s ((๐ด ยทs ๐ต) ยทs ๐ง)) = (((((๐ฅ ยทs ๐ต) ยทs ๐ถ) +s ((๐ด ยทs ๐ฆ) ยทs ๐ถ)) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ถ)) +s ((๐ด ยทs ๐ต) ยทs ๐ง))) |
171 | 165, 57, 44 | subsdird 27975 |
. . . . . . . 8
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ((((๐ฅ ยทs ๐ต) +s (๐ด ยทs ๐ฆ)) -s (๐ฅ ยทs ๐ฆ)) ยทs ๐ง) = ((((๐ฅ ยทs ๐ต) +s (๐ด ยทs ๐ฆ)) ยทs ๐ง) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ง))) |
172 | 39, 53, 44 | addsdird 27973 |
. . . . . . . . 9
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ (((๐ฅ ยทs ๐ต) +s (๐ด ยทs ๐ฆ)) ยทs ๐ง) = (((๐ฅ ยทs ๐ต) ยทs ๐ง) +s ((๐ด ยทs ๐ฆ) ยทs ๐ง))) |
173 | 172 | oveq1d 7416 |
. . . . . . . 8
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ((((๐ฅ ยทs ๐ต) +s (๐ด ยทs ๐ฆ)) ยทs ๐ง) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ง)) = ((((๐ฅ ยทs ๐ต) ยทs ๐ง) +s ((๐ด ยทs ๐ฆ) ยทs ๐ง)) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ง))) |
174 | 171, 173 | eqtrd 2764 |
. . . . . . 7
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ((((๐ฅ ยทs ๐ต) +s (๐ด ยทs ๐ฆ)) -s (๐ฅ ยทs ๐ฆ)) ยทs ๐ง) = ((((๐ฅ ยทs ๐ต) ยทs ๐ง) +s ((๐ด ยทs ๐ฆ) ยทs ๐ง)) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ง))) |
175 | 170, 174 | oveq12d 7419 |
. . . . . 6
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ((((((๐ฅ ยทs ๐ต) +s (๐ด ยทs ๐ฆ)) -s (๐ฅ ยทs ๐ฆ)) ยทs ๐ถ) +s ((๐ด ยทs ๐ต) ยทs ๐ง)) -s ((((๐ฅ ยทs ๐ต) +s (๐ด ยทs ๐ฆ)) -s (๐ฅ ยทs ๐ฆ)) ยทs ๐ง)) = ((((((๐ฅ ยทs ๐ต) ยทs ๐ถ) +s ((๐ด ยทs ๐ฆ) ยทs ๐ถ)) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ถ)) +s ((๐ด ยทs ๐ต) ยทs ๐ง)) -s ((((๐ฅ ยทs ๐ต) ยทs ๐ง) +s ((๐ด ยทs ๐ฆ) ยทs ๐ง)) -s ((๐ฅ ยทs ๐ฆ) ยทs ๐ง)))) |
176 | 102, 100 | addscld 27813 |
. . . . . . . . . 10
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ((๐ฆ ยทs ๐ถ) +s (๐ต ยทs ๐ง)) โ No
) |
177 | 47, 176, 129 | subsdid 27974 |
. . . . . . . . 9
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ (๐ด ยทs (((๐ฆ ยทs ๐ถ) +s (๐ต ยทs ๐ง)) -s (๐ฆ ยทs ๐ง))) = ((๐ด ยทs ((๐ฆ ยทs ๐ถ) +s (๐ต ยทs ๐ง))) -s (๐ด ยทs (๐ฆ ยทs ๐ง)))) |
178 | 47, 102, 100 | addsdid 27972 |
. . . . . . . . . 10
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ (๐ด ยทs ((๐ฆ ยทs ๐ถ) +s (๐ต ยทs ๐ง))) = ((๐ด ยทs (๐ฆ ยทs ๐ถ)) +s (๐ด ยทs (๐ต ยทs ๐ง)))) |
179 | 178 | oveq1d 7416 |
. . . . . . . . 9
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ((๐ด ยทs ((๐ฆ ยทs ๐ถ) +s (๐ต ยทs ๐ง))) -s (๐ด ยทs (๐ฆ ยทs ๐ง))) = (((๐ด ยทs (๐ฆ ยทs ๐ถ)) +s (๐ด ยทs (๐ต ยทs ๐ง))) -s (๐ด ยทs (๐ฆ ยทs ๐ง)))) |
180 | 177, 179 | eqtrd 2764 |
. . . . . . . 8
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ (๐ด ยทs (((๐ฆ ยทs ๐ถ) +s (๐ต ยทs ๐ง)) -s (๐ฆ ยทs ๐ง))) = (((๐ด ยทs (๐ฆ ยทs ๐ถ)) +s (๐ด ยทs (๐ต ยทs ๐ง))) -s (๐ด ยทs (๐ฆ ยทs ๐ง)))) |
181 | 180 | oveq2d 7417 |
. . . . . . 7
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ((๐ฅ ยทs (๐ต ยทs ๐ถ)) +s (๐ด ยทs (((๐ฆ ยทs ๐ถ) +s (๐ต ยทs ๐ง)) -s (๐ฆ ยทs ๐ง)))) = ((๐ฅ ยทs (๐ต ยทs ๐ถ)) +s (((๐ด ยทs (๐ฆ ยทs ๐ถ)) +s (๐ด ยทs (๐ต ยทs ๐ง))) -s (๐ด ยทs (๐ฆ ยทs ๐ง))))) |
182 | 36, 176, 129 | subsdid 27974 |
. . . . . . . 8
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ (๐ฅ ยทs (((๐ฆ ยทs ๐ถ) +s (๐ต ยทs ๐ง)) -s (๐ฆ ยทs ๐ง))) = ((๐ฅ ยทs ((๐ฆ ยทs ๐ถ) +s (๐ต ยทs ๐ง))) -s (๐ฅ ยทs (๐ฆ ยทs ๐ง)))) |
183 | 36, 102, 100 | addsdid 27972 |
. . . . . . . . 9
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ (๐ฅ ยทs ((๐ฆ ยทs ๐ถ) +s (๐ต ยทs ๐ง))) = ((๐ฅ ยทs (๐ฆ ยทs ๐ถ)) +s (๐ฅ ยทs (๐ต ยทs ๐ง)))) |
184 | 183 | oveq1d 7416 |
. . . . . . . 8
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ((๐ฅ ยทs ((๐ฆ ยทs ๐ถ) +s (๐ต ยทs ๐ง))) -s (๐ฅ ยทs (๐ฆ ยทs ๐ง))) = (((๐ฅ ยทs (๐ฆ ยทs ๐ถ)) +s (๐ฅ ยทs (๐ต ยทs ๐ง))) -s (๐ฅ ยทs (๐ฆ ยทs ๐ง)))) |
185 | 182, 184 | eqtrd 2764 |
. . . . . . 7
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ (๐ฅ ยทs (((๐ฆ ยทs ๐ถ) +s (๐ต ยทs ๐ง)) -s (๐ฆ ยทs ๐ง))) = (((๐ฅ ยทs (๐ฆ ยทs ๐ถ)) +s (๐ฅ ยทs (๐ต ยทs ๐ง))) -s (๐ฅ ยทs (๐ฆ ยทs ๐ง)))) |
186 | 181, 185 | oveq12d 7419 |
. . . . . 6
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ (((๐ฅ ยทs (๐ต ยทs ๐ถ)) +s (๐ด ยทs (((๐ฆ ยทs ๐ถ) +s (๐ต ยทs ๐ง)) -s (๐ฆ ยทs ๐ง)))) -s (๐ฅ ยทs (((๐ฆ ยทs ๐ถ) +s (๐ต ยทs ๐ง)) -s (๐ฆ ยทs ๐ง)))) = (((๐ฅ ยทs (๐ต ยทs ๐ถ)) +s (((๐ด ยทs (๐ฆ ยทs ๐ถ)) +s (๐ด ยทs (๐ต ยทs ๐ง))) -s (๐ด ยทs (๐ฆ ยทs ๐ง)))) -s (((๐ฅ ยทs (๐ฆ ยทs ๐ถ)) +s (๐ฅ ยทs (๐ต ยทs ๐ง))) -s (๐ฅ ยทs (๐ฆ ยทs ๐ง))))) |
187 | 164, 175,
186 | 3eqtr4d 2774 |
. . . . 5
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ ((((((๐ฅ ยทs ๐ต) +s (๐ด ยทs ๐ฆ)) -s (๐ฅ ยทs ๐ฆ)) ยทs ๐ถ) +s ((๐ด ยทs ๐ต) ยทs ๐ง)) -s ((((๐ฅ ยทs ๐ต) +s (๐ด ยทs ๐ฆ)) -s (๐ฅ ยทs ๐ฆ)) ยทs ๐ง)) = (((๐ฅ ยทs (๐ต ยทs ๐ถ)) +s (๐ด ยทs (((๐ฆ ยทs ๐ถ) +s (๐ต ยทs ๐ง)) -s (๐ฆ ยทs ๐ง)))) -s (๐ฅ ยทs (((๐ฆ ยทs ๐ถ) +s (๐ต ยทs ๐ง)) -s (๐ฆ ยทs ๐ง))))) |
188 | 187 | eqeq2d 2735 |
. . . 4
โข ((๐ โง ((๐ฅ โ ๐ โง ๐ฆ โ ๐) โง ๐ง โ ๐
)) โ (๐ = ((((((๐ฅ ยทs ๐ต) +s (๐ด ยทs ๐ฆ)) -s (๐ฅ ยทs ๐ฆ)) ยทs ๐ถ) +s ((๐ด ยทs ๐ต) ยทs ๐ง)) -s ((((๐ฅ ยทs ๐ต) +s (๐ด ยทs ๐ฆ)) -s (๐ฅ ยทs ๐ฆ)) ยทs ๐ง)) โ ๐ = (((๐ฅ ยทs (๐ต ยทs ๐ถ)) +s (๐ด ยทs (((๐ฆ ยทs ๐ถ) +s (๐ต ยทs ๐ง)) -s (๐ฆ ยทs ๐ง)))) -s (๐ฅ ยทs (((๐ฆ ยทs ๐ถ) +s (๐ต ยทs ๐ง)) -s (๐ฆ ยทs ๐ง)))))) |
189 | 188 | anassrs 467 |
. . 3
โข (((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐)) โง ๐ง โ ๐
) โ (๐ = ((((((๐ฅ ยทs ๐ต) +s (๐ด ยทs ๐ฆ)) -s (๐ฅ ยทs ๐ฆ)) ยทs ๐ถ) +s ((๐ด ยทs ๐ต) ยทs ๐ง)) -s ((((๐ฅ ยทs ๐ต) +s (๐ด ยทs ๐ฆ)) -s (๐ฅ ยทs ๐ฆ)) ยทs ๐ง)) โ ๐ = (((๐ฅ ยทs (๐ต ยทs ๐ถ)) +s (๐ด ยทs (((๐ฆ ยทs ๐ถ) +s (๐ต ยทs ๐ง)) -s (๐ฆ ยทs ๐ง)))) -s (๐ฅ ยทs (((๐ฆ ยทs ๐ถ) +s (๐ต ยทs ๐ง)) -s (๐ฆ ยทs ๐ง)))))) |
190 | 189 | rexbidva 3168 |
. 2
โข ((๐ โง (๐ฅ โ ๐ โง ๐ฆ โ ๐)) โ (โ๐ง โ ๐
๐ = ((((((๐ฅ ยทs ๐ต) +s (๐ด ยทs ๐ฆ)) -s (๐ฅ ยทs ๐ฆ)) ยทs ๐ถ) +s ((๐ด ยทs ๐ต) ยทs ๐ง)) -s ((((๐ฅ ยทs ๐ต) +s (๐ด ยทs ๐ฆ)) -s (๐ฅ ยทs ๐ฆ)) ยทs ๐ง)) โ โ๐ง โ ๐
๐ = (((๐ฅ ยทs (๐ต ยทs ๐ถ)) +s (๐ด ยทs (((๐ฆ ยทs ๐ถ) +s (๐ต ยทs ๐ง)) -s (๐ฆ ยทs ๐ง)))) -s (๐ฅ ยทs (((๐ฆ ยทs ๐ถ) +s (๐ต ยทs ๐ง)) -s (๐ฆ ยทs ๐ง)))))) |
191 | 190 | 2rexbidva 3209 |
1
โข (๐ โ (โ๐ฅ โ ๐ โ๐ฆ โ ๐ โ๐ง โ ๐
๐ = ((((((๐ฅ ยทs ๐ต) +s (๐ด ยทs ๐ฆ)) -s (๐ฅ ยทs ๐ฆ)) ยทs ๐ถ) +s ((๐ด ยทs ๐ต) ยทs ๐ง)) -s ((((๐ฅ ยทs ๐ต) +s (๐ด ยทs ๐ฆ)) -s (๐ฅ ยทs ๐ฆ)) ยทs ๐ง)) โ โ๐ฅ โ ๐ โ๐ฆ โ ๐ โ๐ง โ ๐
๐ = (((๐ฅ ยทs (๐ต ยทs ๐ถ)) +s (๐ด ยทs (((๐ฆ ยทs ๐ถ) +s (๐ต ยทs ๐ง)) -s (๐ฆ ยทs ๐ง)))) -s (๐ฅ ยทs (((๐ฆ ยทs ๐ถ) +s (๐ต ยทs ๐ง)) -s (๐ฆ ยทs ๐ง)))))) |