Step | Hyp | Ref
| Expression |
1 | | fveq1 6842 |
. . . . . 6
โข (๐ก = ๐ โ (๐กโ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) = (๐โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง))) |
2 | | fveq1 6842 |
. . . . . . . 8
โข (๐ก = ๐ โ (๐กโ๐ฆ) = (๐โ๐ฆ)) |
3 | 2 | oveq2d 7374 |
. . . . . . 7
โข (๐ก = ๐ โ (๐ฅ ยทโ (๐กโ๐ฆ)) = (๐ฅ ยทโ (๐โ๐ฆ))) |
4 | | fveq1 6842 |
. . . . . . 7
โข (๐ก = ๐ โ (๐กโ๐ง) = (๐โ๐ง)) |
5 | 3, 4 | oveq12d 7376 |
. . . . . 6
โข (๐ก = ๐ โ ((๐ฅ ยทโ (๐กโ๐ฆ)) +โ (๐กโ๐ง)) = ((๐ฅ ยทโ (๐โ๐ฆ)) +โ (๐โ๐ง))) |
6 | 1, 5 | eqeq12d 2749 |
. . . . 5
โข (๐ก = ๐ โ ((๐กโ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) = ((๐ฅ ยทโ (๐กโ๐ฆ)) +โ (๐กโ๐ง)) โ (๐โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) = ((๐ฅ ยทโ (๐โ๐ฆ)) +โ (๐โ๐ง)))) |
7 | 6 | ralbidv 3171 |
. . . 4
โข (๐ก = ๐ โ (โ๐ง โ โ (๐กโ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) = ((๐ฅ ยทโ (๐กโ๐ฆ)) +โ (๐กโ๐ง)) โ โ๐ง โ โ (๐โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) = ((๐ฅ ยทโ (๐โ๐ฆ)) +โ (๐โ๐ง)))) |
8 | 7 | 2ralbidv 3209 |
. . 3
โข (๐ก = ๐ โ (โ๐ฅ โ โ โ๐ฆ โ โ โ๐ง โ โ (๐กโ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) = ((๐ฅ ยทโ (๐กโ๐ฆ)) +โ (๐กโ๐ง)) โ โ๐ฅ โ โ โ๐ฆ โ โ โ๐ง โ โ (๐โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) = ((๐ฅ ยทโ (๐โ๐ฆ)) +โ (๐โ๐ง)))) |
9 | | df-lnop 30825 |
. . 3
โข LinOp =
{๐ก โ ( โ
โm โ) โฃ โ๐ฅ โ โ โ๐ฆ โ โ โ๐ง โ โ (๐กโ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) = ((๐ฅ ยทโ (๐กโ๐ฆ)) +โ (๐กโ๐ง))} |
10 | 8, 9 | elrab2 3649 |
. 2
โข (๐ โ LinOp โ (๐ โ ( โ
โm โ) โง โ๐ฅ โ โ โ๐ฆ โ โ โ๐ง โ โ (๐โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) = ((๐ฅ ยทโ (๐โ๐ฆ)) +โ (๐โ๐ง)))) |
11 | | ax-hilex 29983 |
. . . 4
โข โ
โ V |
12 | 11, 11 | elmap 8812 |
. . 3
โข (๐ โ ( โ
โm โ) โ ๐: โโถ โ) |
13 | 12 | anbi1i 625 |
. 2
โข ((๐ โ ( โ
โm โ) โง โ๐ฅ โ โ โ๐ฆ โ โ โ๐ง โ โ (๐โ((๐ฅ ยทโ ๐ฆ) +โ ๐ง)) = ((๐ฅ ยทโ (๐โ๐ฆ)) +โ (๐โ๐ง))) โ (๐: โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
โ๐ง โ โ
(๐โ((๐ฅ
ยทโ ๐ฆ) +โ ๐ง)) = ((๐ฅ ยทโ (๐โ๐ฆ)) +โ (๐โ๐ง)))) |
14 | 10, 13 | bitri 275 |
1
โข (๐ โ LinOp โ (๐: โโถ โ โง
โ๐ฅ โ โ
โ๐ฆ โ โ
โ๐ง โ โ
(๐โ((๐ฅ
ยทโ ๐ฆ) +โ ๐ง)) = ((๐ฅ ยทโ (๐โ๐ฆ)) +โ (๐โ๐ง)))) |