Step | Hyp | Ref
| Expression |
1 | | lnopco.1 |
. . . 4
โข ๐ โ LinOp |
2 | 1 | lnopfi 30960 |
. . 3
โข ๐: โโถ
โ |
3 | | lnopco.2 |
. . . 4
โข ๐ โ LinOp |
4 | 3 | lnopfi 30960 |
. . 3
โข ๐: โโถ
โ |
5 | 2, 4 | hoaddcli 30759 |
. 2
โข (๐ +op ๐): โโถ
โ |
6 | | hvmulcl 30004 |
. . . . . . 7
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (๐ฅ
ยทโ ๐ฆ) โ โ) |
7 | 1 | lnopaddi 30962 |
. . . . . . . 8
โข (((๐ฅ
ยทโ ๐ฆ) โ โ โง ๐ง โ โ) โ (๐โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) = ((๐โ(๐ฅ ยทโ ๐ฆ)) +โ (๐โ๐ง))) |
8 | 3 | lnopaddi 30962 |
. . . . . . . 8
โข (((๐ฅ
ยทโ ๐ฆ) โ โ โง ๐ง โ โ) โ (๐โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) = ((๐โ(๐ฅ ยทโ ๐ฆ)) +โ (๐โ๐ง))) |
9 | 7, 8 | oveq12d 7379 |
. . . . . . 7
โข (((๐ฅ
ยทโ ๐ฆ) โ โ โง ๐ง โ โ) โ ((๐โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) +โ (๐โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง))) = (((๐โ(๐ฅ ยทโ ๐ฆ)) +โ (๐โ๐ง)) +โ ((๐โ(๐ฅ ยทโ ๐ฆ)) +โ (๐โ๐ง)))) |
10 | 6, 9 | sylan 581 |
. . . . . 6
โข (((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ) โ ((๐โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) +โ (๐โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง))) = (((๐โ(๐ฅ ยทโ ๐ฆ)) +โ (๐โ๐ง)) +โ ((๐โ(๐ฅ ยทโ ๐ฆ)) +โ (๐โ๐ง)))) |
11 | 2 | ffvelcdmi 7038 |
. . . . . . . . 9
โข ((๐ฅ
ยทโ ๐ฆ) โ โ โ (๐โ(๐ฅ ยทโ ๐ฆ)) โ
โ) |
12 | 6, 11 | syl 17 |
. . . . . . . 8
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (๐โ(๐ฅ ยทโ ๐ฆ)) โ
โ) |
13 | 2 | ffvelcdmi 7038 |
. . . . . . . 8
โข (๐ง โ โ โ (๐โ๐ง) โ โ) |
14 | 12, 13 | anim12i 614 |
. . . . . . 7
โข (((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ) โ ((๐โ(๐ฅ ยทโ ๐ฆ)) โ โ โง (๐โ๐ง) โ โ)) |
15 | 4 | ffvelcdmi 7038 |
. . . . . . . . 9
โข ((๐ฅ
ยทโ ๐ฆ) โ โ โ (๐โ(๐ฅ ยทโ ๐ฆ)) โ
โ) |
16 | 6, 15 | syl 17 |
. . . . . . . 8
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (๐โ(๐ฅ ยทโ ๐ฆ)) โ
โ) |
17 | 4 | ffvelcdmi 7038 |
. . . . . . . 8
โข (๐ง โ โ โ (๐โ๐ง) โ โ) |
18 | 16, 17 | anim12i 614 |
. . . . . . 7
โข (((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ) โ ((๐โ(๐ฅ ยทโ ๐ฆ)) โ โ โง (๐โ๐ง) โ โ)) |
19 | | hvadd4 30027 |
. . . . . . 7
โข ((((๐โ(๐ฅ ยทโ ๐ฆ)) โ โ โง (๐โ๐ง) โ โ) โง ((๐โ(๐ฅ ยทโ ๐ฆ)) โ โ โง (๐โ๐ง) โ โ)) โ (((๐โ(๐ฅ ยทโ ๐ฆ)) +โ (๐โ๐ง)) +โ ((๐โ(๐ฅ ยทโ ๐ฆ)) +โ (๐โ๐ง))) = (((๐โ(๐ฅ ยทโ ๐ฆ)) +โ (๐โ(๐ฅ ยทโ ๐ฆ))) +โ ((๐โ๐ง) +โ (๐โ๐ง)))) |
20 | 14, 18, 19 | syl2anc 585 |
. . . . . 6
โข (((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ) โ (((๐โ(๐ฅ ยทโ ๐ฆ)) +โ (๐โ๐ง)) +โ ((๐โ(๐ฅ ยทโ ๐ฆ)) +โ (๐โ๐ง))) = (((๐โ(๐ฅ ยทโ ๐ฆ)) +โ (๐โ(๐ฅ ยทโ ๐ฆ))) +โ ((๐โ๐ง) +โ (๐โ๐ง)))) |
21 | 10, 20 | eqtrd 2773 |
. . . . 5
โข (((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ) โ ((๐โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) +โ (๐โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง))) = (((๐โ(๐ฅ ยทโ ๐ฆ)) +โ (๐โ(๐ฅ ยทโ ๐ฆ))) +โ ((๐โ๐ง) +โ (๐โ๐ง)))) |
22 | | hvaddcl 30003 |
. . . . . . 7
โข (((๐ฅ
ยทโ ๐ฆ) โ โ โง ๐ง โ โ) โ ((๐ฅ ยทโ ๐ฆ) +โ ๐ง) โ
โ) |
23 | 6, 22 | sylan 581 |
. . . . . 6
โข (((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ) โ ((๐ฅ
ยทโ ๐ฆ) +โ ๐ง) โ โ) |
24 | | hosval 30731 |
. . . . . . 7
โข ((๐: โโถ โ โง
๐: โโถ โ
โง ((๐ฅ
ยทโ ๐ฆ) +โ ๐ง) โ โ) โ ((๐ +op ๐)โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) = ((๐โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) +โ (๐โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)))) |
25 | 2, 4, 24 | mp3an12 1452 |
. . . . . 6
โข (((๐ฅ
ยทโ ๐ฆ) +โ ๐ง) โ โ โ ((๐ +op ๐)โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) = ((๐โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) +โ (๐โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)))) |
26 | 23, 25 | syl 17 |
. . . . 5
โข (((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ) โ ((๐ +op ๐)โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) = ((๐โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) +โ (๐โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)))) |
27 | 2 | ffvelcdmi 7038 |
. . . . . . . . 9
โข (๐ฆ โ โ โ (๐โ๐ฆ) โ โ) |
28 | 4 | ffvelcdmi 7038 |
. . . . . . . . 9
โข (๐ฆ โ โ โ (๐โ๐ฆ) โ โ) |
29 | 27, 28 | jca 513 |
. . . . . . . 8
โข (๐ฆ โ โ โ ((๐โ๐ฆ) โ โ โง (๐โ๐ฆ) โ โ)) |
30 | | ax-hvdistr1 29999 |
. . . . . . . . 9
โข ((๐ฅ โ โ โง (๐โ๐ฆ) โ โ โง (๐โ๐ฆ) โ โ) โ (๐ฅ ยทโ ((๐โ๐ฆ) +โ (๐โ๐ฆ))) = ((๐ฅ ยทโ (๐โ๐ฆ)) +โ (๐ฅ ยทโ (๐โ๐ฆ)))) |
31 | 30 | 3expb 1121 |
. . . . . . . 8
โข ((๐ฅ โ โ โง ((๐โ๐ฆ) โ โ โง (๐โ๐ฆ) โ โ)) โ (๐ฅ ยทโ ((๐โ๐ฆ) +โ (๐โ๐ฆ))) = ((๐ฅ ยทโ (๐โ๐ฆ)) +โ (๐ฅ ยทโ (๐โ๐ฆ)))) |
32 | 29, 31 | sylan2 594 |
. . . . . . 7
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (๐ฅ
ยทโ ((๐โ๐ฆ) +โ (๐โ๐ฆ))) = ((๐ฅ ยทโ (๐โ๐ฆ)) +โ (๐ฅ ยทโ (๐โ๐ฆ)))) |
33 | | hosval 30731 |
. . . . . . . . . 10
โข ((๐: โโถ โ โง
๐: โโถ โ
โง ๐ฆ โ โ)
โ ((๐ +op
๐)โ๐ฆ) = ((๐โ๐ฆ) +โ (๐โ๐ฆ))) |
34 | 2, 4, 33 | mp3an12 1452 |
. . . . . . . . 9
โข (๐ฆ โ โ โ ((๐ +op ๐)โ๐ฆ) = ((๐โ๐ฆ) +โ (๐โ๐ฆ))) |
35 | 34 | oveq2d 7377 |
. . . . . . . 8
โข (๐ฆ โ โ โ (๐ฅ
ยทโ ((๐ +op ๐)โ๐ฆ)) = (๐ฅ ยทโ ((๐โ๐ฆ) +โ (๐โ๐ฆ)))) |
36 | 35 | adantl 483 |
. . . . . . 7
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (๐ฅ
ยทโ ((๐ +op ๐)โ๐ฆ)) = (๐ฅ ยทโ ((๐โ๐ฆ) +โ (๐โ๐ฆ)))) |
37 | 1 | lnopmuli 30963 |
. . . . . . . 8
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (๐โ(๐ฅ ยทโ ๐ฆ)) = (๐ฅ ยทโ (๐โ๐ฆ))) |
38 | 3 | lnopmuli 30963 |
. . . . . . . 8
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (๐โ(๐ฅ ยทโ ๐ฆ)) = (๐ฅ ยทโ (๐โ๐ฆ))) |
39 | 37, 38 | oveq12d 7379 |
. . . . . . 7
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ ((๐โ(๐ฅ ยทโ ๐ฆ)) +โ (๐โ(๐ฅ ยทโ ๐ฆ))) = ((๐ฅ ยทโ (๐โ๐ฆ)) +โ (๐ฅ ยทโ (๐โ๐ฆ)))) |
40 | 32, 36, 39 | 3eqtr4d 2783 |
. . . . . 6
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ (๐ฅ
ยทโ ((๐ +op ๐)โ๐ฆ)) = ((๐โ(๐ฅ ยทโ ๐ฆ)) +โ (๐โ(๐ฅ ยทโ ๐ฆ)))) |
41 | | hosval 30731 |
. . . . . . 7
โข ((๐: โโถ โ โง
๐: โโถ โ
โง ๐ง โ โ)
โ ((๐ +op
๐)โ๐ง) = ((๐โ๐ง) +โ (๐โ๐ง))) |
42 | 2, 4, 41 | mp3an12 1452 |
. . . . . 6
โข (๐ง โ โ โ ((๐ +op ๐)โ๐ง) = ((๐โ๐ง) +โ (๐โ๐ง))) |
43 | 40, 42 | oveqan12d 7380 |
. . . . 5
โข (((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ) โ ((๐ฅ
ยทโ ((๐ +op ๐)โ๐ฆ)) +โ ((๐ +op ๐)โ๐ง)) = (((๐โ(๐ฅ ยทโ ๐ฆ)) +โ (๐โ(๐ฅ ยทโ ๐ฆ))) +โ ((๐โ๐ง) +โ (๐โ๐ง)))) |
44 | 21, 26, 43 | 3eqtr4d 2783 |
. . . 4
โข (((๐ฅ โ โ โง ๐ฆ โ โ) โง ๐ง โ โ) โ ((๐ +op ๐)โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) = ((๐ฅ ยทโ ((๐ +op ๐)โ๐ฆ)) +โ ((๐ +op ๐)โ๐ง))) |
45 | 44 | ralrimiva 3140 |
. . 3
โข ((๐ฅ โ โ โง ๐ฆ โ โ) โ
โ๐ง โ โ
((๐ +op ๐)โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) = ((๐ฅ ยทโ ((๐ +op ๐)โ๐ฆ)) +โ ((๐ +op ๐)โ๐ง))) |
46 | 45 | rgen2 3191 |
. 2
โข
โ๐ฅ โ
โ โ๐ฆ โ
โ โ๐ง โ
โ ((๐ +op
๐)โ((๐ฅ
ยทโ ๐ฆ) +โ ๐ง)) = ((๐ฅ ยทโ ((๐ +op ๐)โ๐ฆ)) +โ ((๐ +op ๐)โ๐ง)) |
47 | | ellnop 30849 |
. 2
โข ((๐ +op ๐) โ LinOp โ ((๐ +op ๐): โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
โ๐ง โ โ
((๐ +op ๐)โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) = ((๐ฅ ยทโ ((๐ +op ๐)โ๐ฆ)) +โ ((๐ +op ๐)โ๐ง)))) |
48 | 5, 46, 47 | mpbir2an 710 |
1
โข (๐ +op ๐) โ LinOp |