Step | Hyp | Ref
| Expression |
1 | | lmhmlin.k |
. . . . . 6
β’ πΎ = (Scalarβπ) |
2 | | eqid 2733 |
. . . . . 6
β’
(Scalarβπ) =
(Scalarβπ) |
3 | | lmhmlin.b |
. . . . . 6
β’ π΅ = (BaseβπΎ) |
4 | | lmhmlin.e |
. . . . . 6
β’ πΈ = (Baseβπ) |
5 | | lmhmlin.m |
. . . . . 6
β’ Β· = (
Β·π βπ) |
6 | | lmhmlin.n |
. . . . . 6
β’ Γ = (
Β·π βπ) |
7 | 1, 2, 3, 4, 5, 6 | islmhm 20503 |
. . . . 5
β’ (πΉ β (π LMHom π) β ((π β LMod β§ π β LMod) β§ (πΉ β (π GrpHom π) β§ (Scalarβπ) = πΎ β§ βπ β π΅ βπ β πΈ (πΉβ(π Β· π)) = (π Γ (πΉβπ))))) |
8 | 7 | simprbi 498 |
. . . 4
β’ (πΉ β (π LMHom π) β (πΉ β (π GrpHom π) β§ (Scalarβπ) = πΎ β§ βπ β π΅ βπ β πΈ (πΉβ(π Β· π)) = (π Γ (πΉβπ)))) |
9 | 8 | simp3d 1145 |
. . 3
β’ (πΉ β (π LMHom π) β βπ β π΅ βπ β πΈ (πΉβ(π Β· π)) = (π Γ (πΉβπ))) |
10 | | fvoveq1 7381 |
. . . . 5
β’ (π = π β (πΉβ(π Β· π)) = (πΉβ(π Β· π))) |
11 | | oveq1 7365 |
. . . . 5
β’ (π = π β (π Γ (πΉβπ)) = (π Γ (πΉβπ))) |
12 | 10, 11 | eqeq12d 2749 |
. . . 4
β’ (π = π β ((πΉβ(π Β· π)) = (π Γ (πΉβπ)) β (πΉβ(π Β· π)) = (π Γ (πΉβπ)))) |
13 | | oveq2 7366 |
. . . . . 6
β’ (π = π β (π Β· π) = (π Β· π)) |
14 | 13 | fveq2d 6847 |
. . . . 5
β’ (π = π β (πΉβ(π Β· π)) = (πΉβ(π Β· π))) |
15 | | fveq2 6843 |
. . . . . 6
β’ (π = π β (πΉβπ) = (πΉβπ)) |
16 | 15 | oveq2d 7374 |
. . . . 5
β’ (π = π β (π Γ (πΉβπ)) = (π Γ (πΉβπ))) |
17 | 14, 16 | eqeq12d 2749 |
. . . 4
β’ (π = π β ((πΉβ(π Β· π)) = (π Γ (πΉβπ)) β (πΉβ(π Β· π)) = (π Γ (πΉβπ)))) |
18 | 12, 17 | rspc2v 3589 |
. . 3
β’ ((π β π΅ β§ π β πΈ) β (βπ β π΅ βπ β πΈ (πΉβ(π Β· π)) = (π Γ (πΉβπ)) β (πΉβ(π Β· π)) = (π Γ (πΉβπ)))) |
19 | 9, 18 | syl5com 31 |
. 2
β’ (πΉ β (π LMHom π) β ((π β π΅ β§ π β πΈ) β (πΉβ(π Β· π)) = (π Γ (πΉβπ)))) |
20 | 19 | 3impib 1117 |
1
β’ ((πΉ β (π LMHom π) β§ π β π΅ β§ π β πΈ) β (πΉβ(π Β· π)) = (π Γ (πΉβπ))) |