Step | Hyp | Ref
| Expression |
1 | | kbval 31070 |
. . . . . . . 8
โข ((๐ถ โ โ โง ๐ท โ โ โง ๐ฅ โ โ) โ ((๐ถ ketbra ๐ท)โ๐ฅ) = ((๐ฅ ยทih ๐ท)
ยทโ ๐ถ)) |
2 | 1 | 3expa 1118 |
. . . . . . 7
โข (((๐ถ โ โ โง ๐ท โ โ) โง ๐ฅ โ โ) โ ((๐ถ ketbra ๐ท)โ๐ฅ) = ((๐ฅ ยทih ๐ท)
ยทโ ๐ถ)) |
3 | 2 | adantll 712 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง ๐ฅ โ โ) โ ((๐ถ ketbra ๐ท)โ๐ฅ) = ((๐ฅ ยทih ๐ท)
ยทโ ๐ถ)) |
4 | 3 | fveq2d 6882 |
. . . . 5
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง ๐ฅ โ โ) โ ((๐ด ketbra ๐ต)โ((๐ถ ketbra ๐ท)โ๐ฅ)) = ((๐ด ketbra ๐ต)โ((๐ฅ ยทih ๐ท)
ยทโ ๐ถ))) |
5 | | simplll 773 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง ๐ฅ โ โ) โ ๐ด โ
โ) |
6 | | simpllr 774 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง ๐ฅ โ โ) โ ๐ต โ
โ) |
7 | | simpr 485 |
. . . . . . . 8
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง ๐ฅ โ โ) โ ๐ฅ โ
โ) |
8 | | simplrr 776 |
. . . . . . . 8
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง ๐ฅ โ โ) โ ๐ท โ
โ) |
9 | | hicl 30196 |
. . . . . . . 8
โข ((๐ฅ โ โ โง ๐ท โ โ) โ (๐ฅ
ยทih ๐ท) โ โ) |
10 | 7, 8, 9 | syl2anc 584 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง ๐ฅ โ โ) โ (๐ฅ
ยทih ๐ท) โ โ) |
11 | | simplrl 775 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง ๐ฅ โ โ) โ ๐ถ โ
โ) |
12 | | hvmulcl 30129 |
. . . . . . 7
โข (((๐ฅ
ยทih ๐ท) โ โ โง ๐ถ โ โ) โ ((๐ฅ ยทih ๐ท)
ยทโ ๐ถ) โ โ) |
13 | 10, 11, 12 | syl2anc 584 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง ๐ฅ โ โ) โ ((๐ฅ
ยทih ๐ท) ยทโ ๐ถ) โ
โ) |
14 | | kbval 31070 |
. . . . . 6
โข ((๐ด โ โ โง ๐ต โ โ โง ((๐ฅ
ยทih ๐ท) ยทโ ๐ถ) โ โ) โ ((๐ด ketbra ๐ต)โ((๐ฅ ยทih ๐ท)
ยทโ ๐ถ)) = ((((๐ฅ ยทih ๐ท)
ยทโ ๐ถ) ยทih ๐ต)
ยทโ ๐ด)) |
15 | 5, 6, 13, 14 | syl3anc 1371 |
. . . . 5
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง ๐ฅ โ โ) โ ((๐ด ketbra ๐ต)โ((๐ฅ ยทih ๐ท)
ยทโ ๐ถ)) = ((((๐ฅ ยทih ๐ท)
ยทโ ๐ถ) ยทih ๐ต)
ยทโ ๐ด)) |
16 | 4, 15 | eqtrd 2771 |
. . . 4
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง ๐ฅ โ โ) โ ((๐ด ketbra ๐ต)โ((๐ถ ketbra ๐ท)โ๐ฅ)) = ((((๐ฅ ยทih ๐ท)
ยทโ ๐ถ) ยทih ๐ต)
ยทโ ๐ด)) |
17 | | kbop 31069 |
. . . . . 6
โข ((๐ถ โ โ โง ๐ท โ โ) โ (๐ถ ketbra ๐ท): โโถ โ) |
18 | 17 | adantl 482 |
. . . . 5
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ (๐ถ ketbra ๐ท): โโถ โ) |
19 | | fvco3 6976 |
. . . . 5
โข (((๐ถ ketbra ๐ท): โโถ โ โง ๐ฅ โ โ) โ (((๐ด ketbra ๐ต) โ (๐ถ ketbra ๐ท))โ๐ฅ) = ((๐ด ketbra ๐ต)โ((๐ถ ketbra ๐ท)โ๐ฅ))) |
20 | 18, 19 | sylan 580 |
. . . 4
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง ๐ฅ โ โ) โ (((๐ด ketbra ๐ต) โ (๐ถ ketbra ๐ท))โ๐ฅ) = ((๐ด ketbra ๐ต)โ((๐ถ ketbra ๐ท)โ๐ฅ))) |
21 | | kbval 31070 |
. . . . . . 7
โข ((๐ด โ โ โง ๐ต โ โ โง ๐ถ โ โ) โ ((๐ด ketbra ๐ต)โ๐ถ) = ((๐ถ ยทih ๐ต)
ยทโ ๐ด)) |
22 | 5, 6, 11, 21 | syl3anc 1371 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง ๐ฅ โ โ) โ ((๐ด ketbra ๐ต)โ๐ถ) = ((๐ถ ยทih ๐ต)
ยทโ ๐ด)) |
23 | 22 | oveq2d 7409 |
. . . . 5
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง ๐ฅ โ โ) โ ((๐ฅ
ยทih ๐ท) ยทโ ((๐ด ketbra ๐ต)โ๐ถ)) = ((๐ฅ ยทih ๐ท)
ยทโ ((๐ถ ยทih ๐ต)
ยทโ ๐ด))) |
24 | | kbop 31069 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ต โ โ) โ (๐ด ketbra ๐ต): โโถ โ) |
25 | 24 | ffvelcdmda 7071 |
. . . . . . . 8
โข (((๐ด โ โ โง ๐ต โ โ) โง ๐ถ โ โ) โ ((๐ด ketbra ๐ต)โ๐ถ) โ โ) |
26 | 25 | adantrr 715 |
. . . . . . 7
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ ((๐ด ketbra ๐ต)โ๐ถ) โ โ) |
27 | 26 | adantr 481 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง ๐ฅ โ โ) โ ((๐ด ketbra ๐ต)โ๐ถ) โ โ) |
28 | | kbval 31070 |
. . . . . 6
โข ((((๐ด ketbra ๐ต)โ๐ถ) โ โ โง ๐ท โ โ โง ๐ฅ โ โ) โ ((((๐ด ketbra ๐ต)โ๐ถ) ketbra ๐ท)โ๐ฅ) = ((๐ฅ ยทih ๐ท)
ยทโ ((๐ด ketbra ๐ต)โ๐ถ))) |
29 | 27, 8, 7, 28 | syl3anc 1371 |
. . . . 5
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง ๐ฅ โ โ) โ
((((๐ด ketbra ๐ต)โ๐ถ) ketbra ๐ท)โ๐ฅ) = ((๐ฅ ยทih ๐ท)
ยทโ ((๐ด ketbra ๐ต)โ๐ถ))) |
30 | | ax-his3 30200 |
. . . . . . . 8
โข (((๐ฅ
ยทih ๐ท) โ โ โง ๐ถ โ โ โง ๐ต โ โ) โ (((๐ฅ
ยทih ๐ท) ยทโ ๐ถ)
ยทih ๐ต) = ((๐ฅ ยทih ๐ท) ยท (๐ถ ยทih ๐ต))) |
31 | 10, 11, 6, 30 | syl3anc 1371 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง ๐ฅ โ โ) โ (((๐ฅ
ยทih ๐ท) ยทโ ๐ถ)
ยทih ๐ต) = ((๐ฅ ยทih ๐ท) ยท (๐ถ ยทih ๐ต))) |
32 | 31 | oveq1d 7408 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง ๐ฅ โ โ) โ
((((๐ฅ
ยทih ๐ท) ยทโ ๐ถ)
ยทih ๐ต) ยทโ ๐ด) = (((๐ฅ ยทih ๐ท) ยท (๐ถ ยทih ๐ต))
ยทโ ๐ด)) |
33 | | hicl 30196 |
. . . . . . . 8
โข ((๐ถ โ โ โง ๐ต โ โ) โ (๐ถ
ยทih ๐ต) โ โ) |
34 | 11, 6, 33 | syl2anc 584 |
. . . . . . 7
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง ๐ฅ โ โ) โ (๐ถ
ยทih ๐ต) โ โ) |
35 | | ax-hvmulass 30123 |
. . . . . . 7
โข (((๐ฅ
ยทih ๐ท) โ โ โง (๐ถ ยทih ๐ต) โ โ โง ๐ด โ โ) โ (((๐ฅ
ยทih ๐ท) ยท (๐ถ ยทih ๐ต))
ยทโ ๐ด) = ((๐ฅ ยทih ๐ท)
ยทโ ((๐ถ ยทih ๐ต)
ยทโ ๐ด))) |
36 | 10, 34, 5, 35 | syl3anc 1371 |
. . . . . 6
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง ๐ฅ โ โ) โ (((๐ฅ
ยทih ๐ท) ยท (๐ถ ยทih ๐ต))
ยทโ ๐ด) = ((๐ฅ ยทih ๐ท)
ยทโ ((๐ถ ยทih ๐ต)
ยทโ ๐ด))) |
37 | 32, 36 | eqtrd 2771 |
. . . . 5
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง ๐ฅ โ โ) โ
((((๐ฅ
ยทih ๐ท) ยทโ ๐ถ)
ยทih ๐ต) ยทโ ๐ด) = ((๐ฅ ยทih ๐ท)
ยทโ ((๐ถ ยทih ๐ต)
ยทโ ๐ด))) |
38 | 23, 29, 37 | 3eqtr4d 2781 |
. . . 4
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง ๐ฅ โ โ) โ
((((๐ด ketbra ๐ต)โ๐ถ) ketbra ๐ท)โ๐ฅ) = ((((๐ฅ ยทih ๐ท)
ยทโ ๐ถ) ยทih ๐ต)
ยทโ ๐ด)) |
39 | 16, 20, 38 | 3eqtr4d 2781 |
. . 3
โข ((((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โง ๐ฅ โ โ) โ (((๐ด ketbra ๐ต) โ (๐ถ ketbra ๐ท))โ๐ฅ) = ((((๐ด ketbra ๐ต)โ๐ถ) ketbra ๐ท)โ๐ฅ)) |
40 | 39 | ralrimiva 3145 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ
โ๐ฅ โ โ
(((๐ด ketbra ๐ต) โ (๐ถ ketbra ๐ท))โ๐ฅ) = ((((๐ด ketbra ๐ต)โ๐ถ) ketbra ๐ท)โ๐ฅ)) |
41 | | fco 6728 |
. . . 4
โข (((๐ด ketbra ๐ต): โโถ โ โง (๐ถ ketbra ๐ท): โโถ โ) โ ((๐ด ketbra ๐ต) โ (๐ถ ketbra ๐ท)): โโถ
โ) |
42 | 24, 17, 41 | syl2an 596 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ ((๐ด ketbra ๐ต) โ (๐ถ ketbra ๐ท)): โโถ
โ) |
43 | | kbop 31069 |
. . . . 5
โข ((((๐ด ketbra ๐ต)โ๐ถ) โ โ โง ๐ท โ โ) โ (((๐ด ketbra ๐ต)โ๐ถ) ketbra ๐ท): โโถ โ) |
44 | 25, 43 | sylan 580 |
. . . 4
โข ((((๐ด โ โ โง ๐ต โ โ) โง ๐ถ โ โ) โง ๐ท โ โ) โ (((๐ด ketbra ๐ต)โ๐ถ) ketbra ๐ท): โโถ โ) |
45 | 44 | anasss 467 |
. . 3
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ
(((๐ด ketbra ๐ต)โ๐ถ) ketbra ๐ท): โโถ โ) |
46 | | ffn 6704 |
. . . 4
โข (((๐ด ketbra ๐ต) โ (๐ถ ketbra ๐ท)): โโถ โ โ ((๐ด ketbra ๐ต) โ (๐ถ ketbra ๐ท)) Fn โ) |
47 | | ffn 6704 |
. . . 4
โข ((((๐ด ketbra ๐ต)โ๐ถ) ketbra ๐ท): โโถ โ โ (((๐ด ketbra ๐ต)โ๐ถ) ketbra ๐ท) Fn โ) |
48 | | eqfnfv 7018 |
. . . 4
โข ((((๐ด ketbra ๐ต) โ (๐ถ ketbra ๐ท)) Fn โ โง (((๐ด ketbra ๐ต)โ๐ถ) ketbra ๐ท) Fn โ) โ (((๐ด ketbra ๐ต) โ (๐ถ ketbra ๐ท)) = (((๐ด ketbra ๐ต)โ๐ถ) ketbra ๐ท) โ โ๐ฅ โ โ (((๐ด ketbra ๐ต) โ (๐ถ ketbra ๐ท))โ๐ฅ) = ((((๐ด ketbra ๐ต)โ๐ถ) ketbra ๐ท)โ๐ฅ))) |
49 | 46, 47, 48 | syl2an 596 |
. . 3
โข ((((๐ด ketbra ๐ต) โ (๐ถ ketbra ๐ท)): โโถ โ โง (((๐ด ketbra ๐ต)โ๐ถ) ketbra ๐ท): โโถ โ) โ (((๐ด ketbra ๐ต) โ (๐ถ ketbra ๐ท)) = (((๐ด ketbra ๐ต)โ๐ถ) ketbra ๐ท) โ โ๐ฅ โ โ (((๐ด ketbra ๐ต) โ (๐ถ ketbra ๐ท))โ๐ฅ) = ((((๐ด ketbra ๐ต)โ๐ถ) ketbra ๐ท)โ๐ฅ))) |
50 | 42, 45, 49 | syl2anc 584 |
. 2
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ
(((๐ด ketbra ๐ต) โ (๐ถ ketbra ๐ท)) = (((๐ด ketbra ๐ต)โ๐ถ) ketbra ๐ท) โ โ๐ฅ โ โ (((๐ด ketbra ๐ต) โ (๐ถ ketbra ๐ท))โ๐ฅ) = ((((๐ด ketbra ๐ต)โ๐ถ) ketbra ๐ท)โ๐ฅ))) |
51 | 40, 50 | mpbird 256 |
1
โข (((๐ด โ โ โง ๐ต โ โ) โง (๐ถ โ โ โง ๐ท โ โ)) โ ((๐ด ketbra ๐ต) โ (๐ถ ketbra ๐ท)) = (((๐ด ketbra ๐ต)โ๐ถ) ketbra ๐ท)) |