Step | Hyp | Ref
| Expression |
1 | | fveq1 6883 |
. . . . . 6
โข (๐ก = ๐ โ (๐กโ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) = (๐โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง))) |
2 | | fveq1 6883 |
. . . . . . . 8
โข (๐ก = ๐ โ (๐กโ๐ฆ) = (๐โ๐ฆ)) |
3 | 2 | oveq2d 7420 |
. . . . . . 7
โข (๐ก = ๐ โ (๐ฅ ยทโ (๐กโ๐ฆ)) = (๐ฅ ยทโ (๐โ๐ฆ))) |
4 | | fveq1 6883 |
. . . . . . 7
โข (๐ก = ๐ โ (๐กโ๐ง) = (๐โ๐ง)) |
5 | 3, 4 | oveq12d 7422 |
. . . . . 6
โข (๐ก = ๐ โ ((๐ฅ ยทโ (๐กโ๐ฆ)) +โ (๐กโ๐ง)) = ((๐ฅ ยทโ (๐โ๐ฆ)) +โ (๐โ๐ง))) |
6 | 1, 5 | eqeq12d 2742 |
. . . . 5
โข (๐ก = ๐ โ ((๐กโ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) = ((๐ฅ ยทโ (๐กโ๐ฆ)) +โ (๐กโ๐ง)) โ (๐โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) = ((๐ฅ ยทโ (๐โ๐ฆ)) +โ (๐โ๐ง)))) |
7 | 6 | ralbidv 3171 |
. . . 4
โข (๐ก = ๐ โ (โ๐ง โ โ (๐กโ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) = ((๐ฅ ยทโ (๐กโ๐ฆ)) +โ (๐กโ๐ง)) โ โ๐ง โ โ (๐โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) = ((๐ฅ ยทโ (๐โ๐ฆ)) +โ (๐โ๐ง)))) |
8 | 7 | 2ralbidv 3212 |
. . 3
โข (๐ก = ๐ โ (โ๐ฅ โ โ โ๐ฆ โ โ โ๐ง โ โ (๐กโ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) = ((๐ฅ ยทโ (๐กโ๐ฆ)) +โ (๐กโ๐ง)) โ โ๐ฅ โ โ โ๐ฆ โ โ โ๐ง โ โ (๐โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) = ((๐ฅ ยทโ (๐โ๐ฆ)) +โ (๐โ๐ง)))) |
9 | | df-lnop 31599 |
. . 3
โข LinOp =
{๐ก โ ( โ
โm โ) โฃ โ๐ฅ โ โ โ๐ฆ โ โ โ๐ง โ โ (๐กโ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) = ((๐ฅ ยทโ (๐กโ๐ฆ)) +โ (๐กโ๐ง))} |
10 | 8, 9 | elrab2 3681 |
. 2
โข (๐ โ LinOp โ (๐ โ ( โ
โm โ) โง โ๐ฅ โ โ โ๐ฆ โ โ โ๐ง โ โ (๐โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) = ((๐ฅ ยทโ (๐โ๐ฆ)) +โ (๐โ๐ง)))) |
11 | | ax-hilex 30757 |
. . . 4
โข โ
โ V |
12 | 11, 11 | elmap 8864 |
. . 3
โข (๐ โ ( โ
โm โ) โ ๐: โโถ โ) |
13 | 12 | anbi1i 623 |
. 2
โข ((๐ โ ( โ
โm โ) โง โ๐ฅ โ โ โ๐ฆ โ โ โ๐ง โ โ (๐โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) = ((๐ฅ ยทโ (๐โ๐ฆ)) +โ (๐โ๐ง))) โ (๐: โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
โ๐ง โ โ
(๐โ((๐ฅ
ยทโ ๐ฆ) +โ ๐ง)) = ((๐ฅ ยทโ (๐โ๐ฆ)) +โ (๐โ๐ง)))) |
14 | 10, 13 | bitri 275 |
1
โข (๐ โ LinOp โ (๐: โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
โ๐ง โ โ
(๐โ((๐ฅ
ยทโ ๐ฆ) +โ ๐ง)) = ((๐ฅ ยทโ (๐โ๐ฆ)) +โ (๐โ๐ง)))) |