Step | Hyp | Ref
| Expression |
1 | | lnopm.1 |
. . . 4
โข ๐ โ LinOp |
2 | 1 | lnopfi 30960 |
. . 3
โข ๐: โโถ
โ |
3 | | homulcl 30750 |
. . 3
โข ((๐ด โ โ โง ๐: โโถ โ)
โ (๐ด
ยทop ๐): โโถ โ) |
4 | 2, 3 | mpan2 690 |
. 2
โข (๐ด โ โ โ (๐ด ยทop
๐): โโถ
โ) |
5 | | hvmulcl 30004 |
. . . . . . . 8
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (๐ฅ
ยทโ ๐ฆ) โ โ) |
6 | | hvaddcl 30003 |
. . . . . . . 8
โข (((๐ฅ
ยทโ ๐ฆ) โ โ โง ๐ง โ โ) โ ((๐ฅ ยทโ ๐ฆ) +โ ๐ง) โ
โ) |
7 | 5, 6 | sylan 581 |
. . . . . . 7
โข (((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ) โ ((๐ฅ
ยทโ ๐ฆ) +โ ๐ง) โ โ) |
8 | | homval 30732 |
. . . . . . . 8
โข ((๐ด โ โ โง ๐: โโถ โ โง
((๐ฅ
ยทโ ๐ฆ) +โ ๐ง) โ โ) โ ((๐ด ยทop ๐)โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) = (๐ด ยทโ (๐โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)))) |
9 | 2, 8 | mp3an2 1450 |
. . . . . . 7
โข ((๐ด โ โ โง ((๐ฅ
ยทโ ๐ฆ) +โ ๐ง) โ โ) โ ((๐ด ยทop ๐)โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) = (๐ด ยทโ (๐โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)))) |
10 | 7, 9 | sylan2 594 |
. . . . . 6
โข ((๐ด โ โ โง ((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ)) โ ((๐ด ยทop
๐)โ((๐ฅ
ยทโ ๐ฆ) +โ ๐ง)) = (๐ด ยทโ (๐โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)))) |
11 | | id 22 |
. . . . . . . . 9
โข (๐ด โ โ โ ๐ด โ
โ) |
12 | 2 | ffvelcdmi 7038 |
. . . . . . . . . 10
โข (๐ฆ โ โ โ (๐โ๐ฆ) โ โ) |
13 | | hvmulcl 30004 |
. . . . . . . . . 10
โข ((๐ฅ โ โ โง (๐โ๐ฆ) โ โ) โ (๐ฅ ยทโ (๐โ๐ฆ)) โ โ) |
14 | 12, 13 | sylan2 594 |
. . . . . . . . 9
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (๐ฅ
ยทโ (๐โ๐ฆ)) โ โ) |
15 | 2 | ffvelcdmi 7038 |
. . . . . . . . 9
โข (๐ง โ โ โ (๐โ๐ง) โ โ) |
16 | | ax-hvdistr1 29999 |
. . . . . . . . 9
โข ((๐ด โ โ โง (๐ฅ
ยทโ (๐โ๐ฆ)) โ โ โง (๐โ๐ง) โ โ) โ (๐ด ยทโ ((๐ฅ
ยทโ (๐โ๐ฆ)) +โ (๐โ๐ง))) = ((๐ด ยทโ (๐ฅ
ยทโ (๐โ๐ฆ))) +โ (๐ด ยทโ (๐โ๐ง)))) |
17 | 11, 14, 15, 16 | syl3an 1161 |
. . . . . . . 8
โข ((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ) โ (๐ด
ยทโ ((๐ฅ ยทโ (๐โ๐ฆ)) +โ (๐โ๐ง))) = ((๐ด ยทโ (๐ฅ
ยทโ (๐โ๐ฆ))) +โ (๐ด ยทโ (๐โ๐ง)))) |
18 | 17 | 3expb 1121 |
. . . . . . 7
โข ((๐ด โ โ โง ((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ)) โ (๐ด
ยทโ ((๐ฅ ยทโ (๐โ๐ฆ)) +โ (๐โ๐ง))) = ((๐ด ยทโ (๐ฅ
ยทโ (๐โ๐ฆ))) +โ (๐ด ยทโ (๐โ๐ง)))) |
19 | 1 | lnopli 30959 |
. . . . . . . . . 10
โข ((๐ฅ โ โ โง ๐ฆ โ โ โง ๐ง โ โ) โ (๐โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) = ((๐ฅ ยทโ (๐โ๐ฆ)) +โ (๐โ๐ง))) |
20 | 19 | 3expa 1119 |
. . . . . . . . 9
โข (((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ) โ (๐โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) = ((๐ฅ ยทโ (๐โ๐ฆ)) +โ (๐โ๐ง))) |
21 | 20 | oveq2d 7377 |
. . . . . . . 8
โข (((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ) โ (๐ด
ยทโ (๐โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง))) = (๐ด ยทโ ((๐ฅ
ยทโ (๐โ๐ฆ)) +โ (๐โ๐ง)))) |
22 | 21 | adantl 483 |
. . . . . . 7
โข ((๐ด โ โ โง ((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ)) โ (๐ด
ยทโ (๐โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง))) = (๐ด ยทโ ((๐ฅ
ยทโ (๐โ๐ฆ)) +โ (๐โ๐ง)))) |
23 | | homval 30732 |
. . . . . . . . . . . . 13
โข ((๐ด โ โ โง ๐: โโถ โ โง
๐ฆ โ โ) โ
((๐ด
ยทop ๐)โ๐ฆ) = (๐ด ยทโ (๐โ๐ฆ))) |
24 | 2, 23 | mp3an2 1450 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ฆ โ โ) โ ((๐ด ยทop
๐)โ๐ฆ) = (๐ด ยทโ (๐โ๐ฆ))) |
25 | 24 | adantrl 715 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ ((๐ด ยทop
๐)โ๐ฆ) = (๐ด ยทโ (๐โ๐ฆ))) |
26 | 25 | oveq2d 7377 |
. . . . . . . . . 10
โข ((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ (๐ฅ
ยทโ ((๐ด ยทop ๐)โ๐ฆ)) = (๐ฅ ยทโ (๐ด
ยทโ (๐โ๐ฆ)))) |
27 | | hvmulcom 30034 |
. . . . . . . . . . . 12
โข ((๐ด โ โ โง ๐ฅ โ โ โง (๐โ๐ฆ) โ โ) โ (๐ด ยทโ (๐ฅ
ยทโ (๐โ๐ฆ))) = (๐ฅ ยทโ (๐ด
ยทโ (๐โ๐ฆ)))) |
28 | 12, 27 | syl3an3 1166 |
. . . . . . . . . . 11
โข ((๐ด โ โ โง ๐ฅ โ โ โง ๐ฆ โ โ) โ (๐ด
ยทโ (๐ฅ ยทโ (๐โ๐ฆ))) = (๐ฅ ยทโ (๐ด
ยทโ (๐โ๐ฆ)))) |
29 | 28 | 3expb 1121 |
. . . . . . . . . 10
โข ((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ (๐ด
ยทโ (๐ฅ ยทโ (๐โ๐ฆ))) = (๐ฅ ยทโ (๐ด
ยทโ (๐โ๐ฆ)))) |
30 | 26, 29 | eqtr4d 2776 |
. . . . . . . . 9
โข ((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โ (๐ฅ
ยทโ ((๐ด ยทop ๐)โ๐ฆ)) = (๐ด ยทโ (๐ฅ
ยทโ (๐โ๐ฆ)))) |
31 | | homval 30732 |
. . . . . . . . . 10
โข ((๐ด โ โ โง ๐: โโถ โ โง
๐ง โ โ) โ
((๐ด
ยทop ๐)โ๐ง) = (๐ด ยทโ (๐โ๐ง))) |
32 | 2, 31 | mp3an2 1450 |
. . . . . . . . 9
โข ((๐ด โ โ โง ๐ง โ โ) โ ((๐ด ยทop
๐)โ๐ง) = (๐ด ยทโ (๐โ๐ง))) |
33 | 30, 32 | oveqan12d 7380 |
. . . . . . . 8
โข (((๐ด โ โ โง (๐ฅ โ โ โง ๐ฆ โ โ)) โง (๐ด โ โ โง ๐ง โ โ)) โ ((๐ฅ
ยทโ ((๐ด ยทop ๐)โ๐ฆ)) +โ ((๐ด ยทop ๐)โ๐ง)) = ((๐ด ยทโ (๐ฅ
ยทโ (๐โ๐ฆ))) +โ (๐ด ยทโ (๐โ๐ง)))) |
34 | 33 | anandis 677 |
. . . . . . 7
โข ((๐ด โ โ โง ((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ)) โ ((๐ฅ
ยทโ ((๐ด ยทop ๐)โ๐ฆ)) +โ ((๐ด ยทop ๐)โ๐ง)) = ((๐ด ยทโ (๐ฅ
ยทโ (๐โ๐ฆ))) +โ (๐ด ยทโ (๐โ๐ง)))) |
35 | 18, 22, 34 | 3eqtr4rd 2784 |
. . . . . 6
โข ((๐ด โ โ โง ((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ)) โ ((๐ฅ
ยทโ ((๐ด ยทop ๐)โ๐ฆ)) +โ ((๐ด ยทop ๐)โ๐ง)) = (๐ด ยทโ (๐โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)))) |
36 | 10, 35 | eqtr4d 2776 |
. . . . 5
โข ((๐ด โ โ โง ((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ)) โ ((๐ด ยทop
๐)โ((๐ฅ
ยทโ ๐ฆ) +โ ๐ง)) = ((๐ฅ ยทโ ((๐ด ยทop
๐)โ๐ฆ)) +โ ((๐ด ยทop ๐)โ๐ง))) |
37 | 36 | exp32 422 |
. . . 4
โข (๐ด โ โ โ ((๐ฅ โ โ โง ๐ฆ โ โ) โ (๐ง โ โ โ ((๐ด ยทop
๐)โ((๐ฅ
ยทโ ๐ฆ) +โ ๐ง)) = ((๐ฅ ยทโ ((๐ด ยทop
๐)โ๐ฆ)) +โ ((๐ด ยทop ๐)โ๐ง))))) |
38 | 37 | ralrimdv 3146 |
. . 3
โข (๐ด โ โ โ ((๐ฅ โ โ โง ๐ฆ โ โ) โ
โ๐ง โ โ
((๐ด
ยทop ๐)โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) = ((๐ฅ ยทโ ((๐ด ยทop
๐)โ๐ฆ)) +โ ((๐ด ยทop ๐)โ๐ง)))) |
39 | 38 | ralrimivv 3192 |
. 2
โข (๐ด โ โ โ
โ๐ฅ โ โ
โ๐ฆ โ โ
โ๐ง โ โ
((๐ด
ยทop ๐)โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) = ((๐ฅ ยทโ ((๐ด ยทop
๐)โ๐ฆ)) +โ ((๐ด ยทop ๐)โ๐ง))) |
40 | | ellnop 30849 |
. 2
โข ((๐ด ยทop
๐) โ LinOp โ
((๐ด
ยทop ๐): โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
โ๐ง โ โ
((๐ด
ยทop ๐)โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) = ((๐ฅ ยทโ ((๐ด ยทop
๐)โ๐ฆ)) +โ ((๐ด ยทop ๐)โ๐ง)))) |
41 | 4, 39, 40 | sylanbrc 584 |
1
โข (๐ด โ โ โ (๐ด ยทop
๐) โ
LinOp) |