Step | Hyp | Ref
| Expression |
1 | | hmopf 30858 |
. 2
โข (๐ โ HrmOp โ ๐: โโถ
โ) |
2 | | simplll 774 |
. . . . . . . 8
โข ((((๐ โ HrmOp โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ง โ โ) โง ๐ค โ โ) โ ๐ โ HrmOp) |
3 | | hvmulcl 29997 |
. . . . . . . . . . 11
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (๐ฅ
ยทโ ๐ฆ) โ โ) |
4 | | hvaddcl 29996 |
. . . . . . . . . . 11
โข (((๐ฅ
ยทโ ๐ฆ) โ โ โง ๐ง โ โ) โ ((๐ฅ ยทโ ๐ฆ) +โ ๐ง) โ
โ) |
5 | 3, 4 | sylan 581 |
. . . . . . . . . 10
โข (((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ) โ ((๐ฅ
ยทโ ๐ฆ) +โ ๐ง) โ โ) |
6 | 5 | adantll 713 |
. . . . . . . . 9
โข (((๐ โ HrmOp โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ง โ โ) โ ((๐ฅ
ยทโ ๐ฆ) +โ ๐ง) โ โ) |
7 | 6 | adantr 482 |
. . . . . . . 8
โข ((((๐ โ HrmOp โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ง โ โ) โง ๐ค โ โ) โ ((๐ฅ
ยทโ ๐ฆ) +โ ๐ง) โ โ) |
8 | | simpr 486 |
. . . . . . . 8
โข ((((๐ โ HrmOp โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ง โ โ) โง ๐ค โ โ) โ ๐ค โ
โ) |
9 | | hmop 30906 |
. . . . . . . . 9
โข ((๐ โ HrmOp โง ((๐ฅ
ยทโ ๐ฆ) +โ ๐ง) โ โ โง ๐ค โ โ) โ (((๐ฅ ยทโ ๐ฆ) +โ ๐ง)
ยทih (๐โ๐ค)) = ((๐โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง))
ยทih ๐ค)) |
10 | 9 | eqcomd 2743 |
. . . . . . . 8
โข ((๐ โ HrmOp โง ((๐ฅ
ยทโ ๐ฆ) +โ ๐ง) โ โ โง ๐ค โ โ) โ ((๐โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง))
ยทih ๐ค) = (((๐ฅ ยทโ ๐ฆ) +โ ๐ง)
ยทih (๐โ๐ค))) |
11 | 2, 7, 8, 10 | syl3anc 1372 |
. . . . . . 7
โข ((((๐ โ HrmOp โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ง โ โ) โง ๐ค โ โ) โ ((๐โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง))
ยทih ๐ค) = (((๐ฅ ยทโ ๐ฆ) +โ ๐ง)
ยทih (๐โ๐ค))) |
12 | | simprl 770 |
. . . . . . . . 9
โข ((๐ โ HrmOp โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ ๐ฅ โ
โ) |
13 | 12 | ad2antrr 725 |
. . . . . . . 8
โข ((((๐ โ HrmOp โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ง โ โ) โง ๐ค โ โ) โ ๐ฅ โ
โ) |
14 | | simprr 772 |
. . . . . . . . 9
โข ((๐ โ HrmOp โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ ๐ฆ โ
โ) |
15 | 14 | ad2antrr 725 |
. . . . . . . 8
โข ((((๐ โ HrmOp โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ง โ โ) โง ๐ค โ โ) โ ๐ฆ โ
โ) |
16 | | simplr 768 |
. . . . . . . 8
โข ((((๐ โ HrmOp โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ง โ โ) โง ๐ค โ โ) โ ๐ง โ
โ) |
17 | 1 | ffvelcdmda 7040 |
. . . . . . . . . 10
โข ((๐ โ HrmOp โง ๐ค โ โ) โ (๐โ๐ค) โ โ) |
18 | 17 | adantlr 714 |
. . . . . . . . 9
โข (((๐ โ HrmOp โง ๐ง โ โ) โง ๐ค โ โ) โ (๐โ๐ค) โ โ) |
19 | 18 | adantllr 718 |
. . . . . . . 8
โข ((((๐ โ HrmOp โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ง โ โ) โง ๐ค โ โ) โ (๐โ๐ค) โ โ) |
20 | | hiassdi 30075 |
. . . . . . . 8
โข (((๐ฅ โ โ โง ๐ฆ โ โ) โง (๐ง โ โ โง (๐โ๐ค) โ โ)) โ (((๐ฅ
ยทโ ๐ฆ) +โ ๐ง) ยทih (๐โ๐ค)) = ((๐ฅ ยท (๐ฆ ยทih (๐โ๐ค))) + (๐ง ยทih (๐โ๐ค)))) |
21 | 13, 15, 16, 19, 20 | syl22anc 838 |
. . . . . . 7
โข ((((๐ โ HrmOp โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ง โ โ) โง ๐ค โ โ) โ (((๐ฅ
ยทโ ๐ฆ) +โ ๐ง) ยทih (๐โ๐ค)) = ((๐ฅ ยท (๐ฆ ยทih (๐โ๐ค))) + (๐ง ยทih (๐โ๐ค)))) |
22 | 1 | ffvelcdmda 7040 |
. . . . . . . . . . 11
โข ((๐ โ HrmOp โง ๐ฆ โ โ) โ (๐โ๐ฆ) โ โ) |
23 | 22 | adantrl 715 |
. . . . . . . . . 10
โข ((๐ โ HrmOp โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ (๐โ๐ฆ) โ โ) |
24 | 23 | ad2antrr 725 |
. . . . . . . . 9
โข ((((๐ โ HrmOp โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ง โ โ) โง ๐ค โ โ) โ (๐โ๐ฆ) โ โ) |
25 | 1 | ffvelcdmda 7040 |
. . . . . . . . . . 11
โข ((๐ โ HrmOp โง ๐ง โ โ) โ (๐โ๐ง) โ โ) |
26 | 25 | adantr 482 |
. . . . . . . . . 10
โข (((๐ โ HrmOp โง ๐ง โ โ) โง ๐ค โ โ) โ (๐โ๐ง) โ โ) |
27 | 26 | adantllr 718 |
. . . . . . . . 9
โข ((((๐ โ HrmOp โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ง โ โ) โง ๐ค โ โ) โ (๐โ๐ง) โ โ) |
28 | | hiassdi 30075 |
. . . . . . . . 9
โข (((๐ฅ โ โ โง (๐โ๐ฆ) โ โ) โง ((๐โ๐ง) โ โ โง ๐ค โ โ)) โ (((๐ฅ
ยทโ (๐โ๐ฆ)) +โ (๐โ๐ง)) ยทih ๐ค) = ((๐ฅ ยท ((๐โ๐ฆ) ยทih ๐ค)) + ((๐โ๐ง) ยทih ๐ค))) |
29 | 13, 24, 27, 8, 28 | syl22anc 838 |
. . . . . . . 8
โข ((((๐ โ HrmOp โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ง โ โ) โง ๐ค โ โ) โ (((๐ฅ
ยทโ (๐โ๐ฆ)) +โ (๐โ๐ง)) ยทih ๐ค) = ((๐ฅ ยท ((๐โ๐ฆ) ยทih ๐ค)) + ((๐โ๐ง) ยทih ๐ค))) |
30 | | hmop 30906 |
. . . . . . . . . . . . . 14
โข ((๐ โ HrmOp โง ๐ฆ โ โ โง ๐ค โ โ) โ (๐ฆ
ยทih (๐โ๐ค)) = ((๐โ๐ฆ) ยทih ๐ค)) |
31 | 30 | eqcomd 2743 |
. . . . . . . . . . . . 13
โข ((๐ โ HrmOp โง ๐ฆ โ โ โง ๐ค โ โ) โ ((๐โ๐ฆ) ยทih ๐ค) = (๐ฆ ยทih (๐โ๐ค))) |
32 | 31 | 3expa 1119 |
. . . . . . . . . . . 12
โข (((๐ โ HrmOp โง ๐ฆ โ โ) โง ๐ค โ โ) โ ((๐โ๐ฆ) ยทih ๐ค) = (๐ฆ ยทih (๐โ๐ค))) |
33 | 32 | oveq2d 7378 |
. . . . . . . . . . 11
โข (((๐ โ HrmOp โง ๐ฆ โ โ) โง ๐ค โ โ) โ (๐ฅ ยท ((๐โ๐ฆ) ยทih ๐ค)) = (๐ฅ ยท (๐ฆ ยทih (๐โ๐ค)))) |
34 | 33 | adantlrl 719 |
. . . . . . . . . 10
โข (((๐ โ HrmOp โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ค โ โ) โ (๐ฅ ยท ((๐โ๐ฆ) ยทih ๐ค)) = (๐ฅ ยท (๐ฆ ยทih (๐โ๐ค)))) |
35 | 34 | adantlr 714 |
. . . . . . . . 9
โข ((((๐ โ HrmOp โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ง โ โ) โง ๐ค โ โ) โ (๐ฅ ยท ((๐โ๐ฆ) ยทih ๐ค)) = (๐ฅ ยท (๐ฆ ยทih (๐โ๐ค)))) |
36 | | hmop 30906 |
. . . . . . . . . . . 12
โข ((๐ โ HrmOp โง ๐ง โ โ โง ๐ค โ โ) โ (๐ง
ยทih (๐โ๐ค)) = ((๐โ๐ง) ยทih ๐ค)) |
37 | 36 | eqcomd 2743 |
. . . . . . . . . . 11
โข ((๐ โ HrmOp โง ๐ง โ โ โง ๐ค โ โ) โ ((๐โ๐ง) ยทih ๐ค) = (๐ง ยทih (๐โ๐ค))) |
38 | 37 | 3expa 1119 |
. . . . . . . . . 10
โข (((๐ โ HrmOp โง ๐ง โ โ) โง ๐ค โ โ) โ ((๐โ๐ง) ยทih ๐ค) = (๐ง ยทih (๐โ๐ค))) |
39 | 38 | adantllr 718 |
. . . . . . . . 9
โข ((((๐ โ HrmOp โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ง โ โ) โง ๐ค โ โ) โ ((๐โ๐ง) ยทih ๐ค) = (๐ง ยทih (๐โ๐ค))) |
40 | 35, 39 | oveq12d 7380 |
. . . . . . . 8
โข ((((๐ โ HrmOp โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ง โ โ) โง ๐ค โ โ) โ ((๐ฅ ยท ((๐โ๐ฆ) ยทih ๐ค)) + ((๐โ๐ง) ยทih ๐ค)) = ((๐ฅ ยท (๐ฆ ยทih (๐โ๐ค))) + (๐ง ยทih (๐โ๐ค)))) |
41 | 29, 40 | eqtr2d 2778 |
. . . . . . 7
โข ((((๐ โ HrmOp โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ง โ โ) โง ๐ค โ โ) โ ((๐ฅ ยท (๐ฆ ยทih (๐โ๐ค))) + (๐ง ยทih (๐โ๐ค))) = (((๐ฅ ยทโ (๐โ๐ฆ)) +โ (๐โ๐ง)) ยทih ๐ค)) |
42 | 11, 21, 41 | 3eqtrd 2781 |
. . . . . 6
โข ((((๐ โ HrmOp โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ง โ โ) โง ๐ค โ โ) โ ((๐โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง))
ยทih ๐ค) = (((๐ฅ ยทโ (๐โ๐ฆ)) +โ (๐โ๐ง)) ยทih ๐ค)) |
43 | 42 | ralrimiva 3144 |
. . . . 5
โข (((๐ โ HrmOp โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ง โ โ) โ
โ๐ค โ โ
((๐โ((๐ฅ
ยทโ ๐ฆ) +โ ๐ง)) ยทih ๐ค) = (((๐ฅ ยทโ (๐โ๐ฆ)) +โ (๐โ๐ง)) ยทih ๐ค)) |
44 | | ffvelcdm 7037 |
. . . . . . . . 9
โข ((๐: โโถ โ โง
((๐ฅ
ยทโ ๐ฆ) +โ ๐ง) โ โ) โ (๐โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) โ
โ) |
45 | 5, 44 | sylan2 594 |
. . . . . . . 8
โข ((๐: โโถ โ โง
((๐ฅ โ โ โง
๐ฆ โ โ) โง
๐ง โ โ)) โ
(๐โ((๐ฅ
ยทโ ๐ฆ) +โ ๐ง)) โ โ) |
46 | 45 | anassrs 469 |
. . . . . . 7
โข (((๐: โโถ โ โง
(๐ฅ โ โ โง
๐ฆ โ โ)) โง
๐ง โ โ) โ
(๐โ((๐ฅ
ยทโ ๐ฆ) +โ ๐ง)) โ โ) |
47 | | ffvelcdm 7037 |
. . . . . . . . . . 11
โข ((๐: โโถ โ โง
๐ฆ โ โ) โ
(๐โ๐ฆ) โ โ) |
48 | | hvmulcl 29997 |
. . . . . . . . . . 11
โข ((๐ฅ โ โ โง (๐โ๐ฆ) โ โ) โ (๐ฅ ยทโ (๐โ๐ฆ)) โ โ) |
49 | 47, 48 | sylan2 594 |
. . . . . . . . . 10
โข ((๐ฅ โ โ โง (๐: โโถ โ โง
๐ฆ โ โ)) โ
(๐ฅ
ยทโ (๐โ๐ฆ)) โ โ) |
50 | 49 | an12s 648 |
. . . . . . . . 9
โข ((๐: โโถ โ โง
(๐ฅ โ โ โง
๐ฆ โ โ)) โ
(๐ฅ
ยทโ (๐โ๐ฆ)) โ โ) |
51 | 50 | adantr 482 |
. . . . . . . 8
โข (((๐: โโถ โ โง
(๐ฅ โ โ โง
๐ฆ โ โ)) โง
๐ง โ โ) โ
(๐ฅ
ยทโ (๐โ๐ฆ)) โ โ) |
52 | | ffvelcdm 7037 |
. . . . . . . . 9
โข ((๐: โโถ โ โง
๐ง โ โ) โ
(๐โ๐ง) โ โ) |
53 | 52 | adantlr 714 |
. . . . . . . 8
โข (((๐: โโถ โ โง
(๐ฅ โ โ โง
๐ฆ โ โ)) โง
๐ง โ โ) โ
(๐โ๐ง) โ โ) |
54 | | hvaddcl 29996 |
. . . . . . . 8
โข (((๐ฅ
ยทโ (๐โ๐ฆ)) โ โ โง (๐โ๐ง) โ โ) โ ((๐ฅ ยทโ (๐โ๐ฆ)) +โ (๐โ๐ง)) โ โ) |
55 | 51, 53, 54 | syl2anc 585 |
. . . . . . 7
โข (((๐: โโถ โ โง
(๐ฅ โ โ โง
๐ฆ โ โ)) โง
๐ง โ โ) โ
((๐ฅ
ยทโ (๐โ๐ฆ)) +โ (๐โ๐ง)) โ โ) |
56 | | hial2eq 30090 |
. . . . . . 7
โข (((๐โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) โ โ โง ((๐ฅ
ยทโ (๐โ๐ฆ)) +โ (๐โ๐ง)) โ โ) โ (โ๐ค โ โ ((๐โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง))
ยทih ๐ค) = (((๐ฅ ยทโ (๐โ๐ฆ)) +โ (๐โ๐ง)) ยทih ๐ค) โ (๐โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) = ((๐ฅ ยทโ (๐โ๐ฆ)) +โ (๐โ๐ง)))) |
57 | 46, 55, 56 | syl2anc 585 |
. . . . . 6
โข (((๐: โโถ โ โง
(๐ฅ โ โ โง
๐ฆ โ โ)) โง
๐ง โ โ) โ
(โ๐ค โ โ
((๐โ((๐ฅ
ยทโ ๐ฆ) +โ ๐ง)) ยทih ๐ค) = (((๐ฅ ยทโ (๐โ๐ฆ)) +โ (๐โ๐ง)) ยทih ๐ค) โ (๐โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) = ((๐ฅ ยทโ (๐โ๐ฆ)) +โ (๐โ๐ง)))) |
58 | 1, 57 | sylanl1 679 |
. . . . 5
โข (((๐ โ HrmOp โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ง โ โ) โ
(โ๐ค โ โ
((๐โ((๐ฅ
ยทโ ๐ฆ) +โ ๐ง)) ยทih ๐ค) = (((๐ฅ ยทโ (๐โ๐ฆ)) +โ (๐โ๐ง)) ยทih ๐ค) โ (๐โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) = ((๐ฅ ยทโ (๐โ๐ฆ)) +โ (๐โ๐ง)))) |
59 | 43, 58 | mpbid 231 |
. . . 4
โข (((๐ โ HrmOp โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง ๐ง โ โ) โ (๐โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) = ((๐ฅ ยทโ (๐โ๐ฆ)) +โ (๐โ๐ง))) |
60 | 59 | ralrimiva 3144 |
. . 3
โข ((๐ โ HrmOp โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ
โ๐ง โ โ
(๐โ((๐ฅ
ยทโ ๐ฆ) +โ ๐ง)) = ((๐ฅ ยทโ (๐โ๐ฆ)) +โ (๐โ๐ง))) |
61 | 60 | ralrimivva 3198 |
. 2
โข (๐ โ HrmOp โ
โ๐ฅ โ โ
โ๐ฆ โ โ
โ๐ง โ โ
(๐โ((๐ฅ
ยทโ ๐ฆ) +โ ๐ง)) = ((๐ฅ ยทโ (๐โ๐ฆ)) +โ (๐โ๐ง))) |
62 | | ellnop 30842 |
. 2
โข (๐ โ LinOp โ (๐: โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
โ๐ง โ โ
(๐โ((๐ฅ
ยทโ ๐ฆ) +โ ๐ง)) = ((๐ฅ ยทโ (๐โ๐ฆ)) +โ (๐โ๐ง)))) |
63 | 1, 61, 62 | sylanbrc 584 |
1
โข (๐ โ HrmOp โ ๐ โ LinOp) |