Step | Hyp | Ref
| Expression |
1 | | ellnfn 31136 |
. . . . . 6
β’ (π β LinFn β (π: ββΆβ β§
βπ₯ β β
βπ¦ β β
βπ§ β β
(πβ((π₯
Β·β π¦) +β π§)) = ((π₯ Β· (πβπ¦)) + (πβπ§)))) |
2 | 1 | simprbi 498 |
. . . . 5
β’ (π β LinFn β
βπ₯ β β
βπ¦ β β
βπ§ β β
(πβ((π₯
Β·β π¦) +β π§)) = ((π₯ Β· (πβπ¦)) + (πβπ§))) |
3 | | oveq1 7416 |
. . . . . . . 8
β’ (π₯ = π΄ β (π₯ Β·β π¦) = (π΄ Β·β π¦)) |
4 | 3 | fvoveq1d 7431 |
. . . . . . 7
β’ (π₯ = π΄ β (πβ((π₯ Β·β π¦) +β π§)) = (πβ((π΄ Β·β π¦) +β π§))) |
5 | | oveq1 7416 |
. . . . . . . 8
β’ (π₯ = π΄ β (π₯ Β· (πβπ¦)) = (π΄ Β· (πβπ¦))) |
6 | 5 | oveq1d 7424 |
. . . . . . 7
β’ (π₯ = π΄ β ((π₯ Β· (πβπ¦)) + (πβπ§)) = ((π΄ Β· (πβπ¦)) + (πβπ§))) |
7 | 4, 6 | eqeq12d 2749 |
. . . . . 6
β’ (π₯ = π΄ β ((πβ((π₯ Β·β π¦) +β π§)) = ((π₯ Β· (πβπ¦)) + (πβπ§)) β (πβ((π΄ Β·β π¦) +β π§)) = ((π΄ Β· (πβπ¦)) + (πβπ§)))) |
8 | | oveq2 7417 |
. . . . . . . 8
β’ (π¦ = π΅ β (π΄ Β·β π¦) = (π΄ Β·β π΅)) |
9 | 8 | fvoveq1d 7431 |
. . . . . . 7
β’ (π¦ = π΅ β (πβ((π΄ Β·β π¦) +β π§)) = (πβ((π΄ Β·β π΅) +β π§))) |
10 | | fveq2 6892 |
. . . . . . . . 9
β’ (π¦ = π΅ β (πβπ¦) = (πβπ΅)) |
11 | 10 | oveq2d 7425 |
. . . . . . . 8
β’ (π¦ = π΅ β (π΄ Β· (πβπ¦)) = (π΄ Β· (πβπ΅))) |
12 | 11 | oveq1d 7424 |
. . . . . . 7
β’ (π¦ = π΅ β ((π΄ Β· (πβπ¦)) + (πβπ§)) = ((π΄ Β· (πβπ΅)) + (πβπ§))) |
13 | 9, 12 | eqeq12d 2749 |
. . . . . 6
β’ (π¦ = π΅ β ((πβ((π΄ Β·β π¦) +β π§)) = ((π΄ Β· (πβπ¦)) + (πβπ§)) β (πβ((π΄ Β·β π΅) +β π§)) = ((π΄ Β· (πβπ΅)) + (πβπ§)))) |
14 | | oveq2 7417 |
. . . . . . . 8
β’ (π§ = πΆ β ((π΄ Β·β π΅) +β π§) = ((π΄ Β·β π΅) +β πΆ)) |
15 | 14 | fveq2d 6896 |
. . . . . . 7
β’ (π§ = πΆ β (πβ((π΄ Β·β π΅) +β π§)) = (πβ((π΄ Β·β π΅) +β πΆ))) |
16 | | fveq2 6892 |
. . . . . . . 8
β’ (π§ = πΆ β (πβπ§) = (πβπΆ)) |
17 | 16 | oveq2d 7425 |
. . . . . . 7
β’ (π§ = πΆ β ((π΄ Β· (πβπ΅)) + (πβπ§)) = ((π΄ Β· (πβπ΅)) + (πβπΆ))) |
18 | 15, 17 | eqeq12d 2749 |
. . . . . 6
β’ (π§ = πΆ β ((πβ((π΄ Β·β π΅) +β π§)) = ((π΄ Β· (πβπ΅)) + (πβπ§)) β (πβ((π΄ Β·β π΅) +β πΆ)) = ((π΄ Β· (πβπ΅)) + (πβπΆ)))) |
19 | 7, 13, 18 | rspc3v 3628 |
. . . . 5
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β
(βπ₯ β β
βπ¦ β β
βπ§ β β
(πβ((π₯
Β·β π¦) +β π§)) = ((π₯ Β· (πβπ¦)) + (πβπ§)) β (πβ((π΄ Β·β π΅) +β πΆ)) = ((π΄ Β· (πβπ΅)) + (πβπΆ)))) |
20 | 2, 19 | syl5 34 |
. . . 4
β’ ((π΄ β β β§ π΅ β β β§ πΆ β β) β (π β LinFn β (πβ((π΄ Β·β π΅) +β πΆ)) = ((π΄ Β· (πβπ΅)) + (πβπΆ)))) |
21 | 20 | 3expb 1121 |
. . 3
β’ ((π΄ β β β§ (π΅ β β β§ πΆ β β)) β (π β LinFn β (πβ((π΄ Β·β π΅) +β πΆ)) = ((π΄ Β· (πβπ΅)) + (πβπΆ)))) |
22 | 21 | impcom 409 |
. 2
β’ ((π β LinFn β§ (π΄ β β β§ (π΅ β β β§ πΆ β β))) β (πβ((π΄ Β·β π΅) +β πΆ)) = ((π΄ Β· (πβπ΅)) + (πβπΆ))) |
23 | 22 | anassrs 469 |
1
β’ (((π β LinFn β§ π΄ β β) β§ (π΅ β β β§ πΆ β β)) β (πβ((π΄ Β·β π΅) +β πΆ)) = ((π΄ Β· (πβπ΅)) + (πβπΆ))) |