Step | Hyp | Ref
| Expression |
1 | | simp2 1134 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ๐ต โ
โ) |
2 | | simp3 1135 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ๐ถ โ
โ) |
3 | 1, 2 | subcld 11575 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ต โ ๐ถ) โ โ) |
4 | | sigar |
. . . 4
โข ๐บ = (๐ฅ โ โ, ๐ฆ โ โ โฆ
(โโ((โโ๐ฅ) ยท ๐ฆ))) |
5 | 4 | sigarmf 46142 |
. . 3
โข ((๐ด โ โ โง (๐ต โ ๐ถ) โ โ โง ๐ถ โ โ) โ ((๐ด โ ๐ถ)๐บ(๐ต โ ๐ถ)) = ((๐ด๐บ(๐ต โ ๐ถ)) โ (๐ถ๐บ(๐ต โ ๐ถ)))) |
6 | 3, 5 | syld3an2 1408 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด โ ๐ถ)๐บ(๐ต โ ๐ถ)) = ((๐ด๐บ(๐ต โ ๐ถ)) โ (๐ถ๐บ(๐ต โ ๐ถ)))) |
7 | 4 | sigarms 46144 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ด๐บ(๐ต โ ๐ถ)) = ((๐ด๐บ๐ต) โ (๐ด๐บ๐ถ))) |
8 | 7 | oveq1d 7420 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด๐บ(๐ต โ ๐ถ)) โ (๐ถ๐บ(๐ต โ ๐ถ))) = (((๐ด๐บ๐ต) โ (๐ด๐บ๐ถ)) โ (๐ถ๐บ(๐ต โ ๐ถ)))) |
9 | 4 | sigarms 46144 |
. . . . 5
โข ((๐ถ โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ถ๐บ(๐ต โ ๐ถ)) = ((๐ถ๐บ๐ต) โ (๐ถ๐บ๐ถ))) |
10 | 2, 9 | syld3an1 1407 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ถ๐บ(๐ต โ ๐ถ)) = ((๐ถ๐บ๐ต) โ (๐ถ๐บ๐ถ))) |
11 | 4 | sigarid 46146 |
. . . . . 6
โข (๐ถ โ โ โ (๐ถ๐บ๐ถ) = 0) |
12 | 2, 11 | syl 17 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ถ๐บ๐ถ) = 0) |
13 | 12 | oveq2d 7421 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ถ๐บ๐ต) โ (๐ถ๐บ๐ถ)) = ((๐ถ๐บ๐ต) โ 0)) |
14 | 4 | sigarim 46139 |
. . . . . . 7
โข ((๐ถ โ โ โง ๐ต โ โ) โ (๐ถ๐บ๐ต) โ โ) |
15 | 14 | recnd 11246 |
. . . . . 6
โข ((๐ถ โ โ โง ๐ต โ โ) โ (๐ถ๐บ๐ต) โ โ) |
16 | 2, 1, 15 | syl2anc 583 |
. . . . 5
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ถ๐บ๐ต) โ โ) |
17 | 16 | subid1d 11564 |
. . . 4
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ถ๐บ๐ต) โ 0) = (๐ถ๐บ๐ต)) |
18 | 10, 13, 17 | 3eqtrd 2770 |
. . 3
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (๐ถ๐บ(๐ต โ ๐ถ)) = (๐ถ๐บ๐ต)) |
19 | 18 | oveq2d 7421 |
. 2
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ (((๐ด๐บ๐ต) โ (๐ด๐บ๐ถ)) โ (๐ถ๐บ(๐ต โ ๐ถ))) = (((๐ด๐บ๐ต) โ (๐ด๐บ๐ถ)) โ (๐ถ๐บ๐ต))) |
20 | 6, 8, 19 | 3eqtrd 2770 |
1
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด โ ๐ถ)๐บ(๐ต โ ๐ถ)) = (((๐ด๐บ๐ต) โ (๐ด๐บ๐ถ)) โ (๐ถ๐บ๐ต))) |