Step | Hyp | Ref
| Expression |
1 | | phllmhm.v |
. . . . 5
β’ π = (Baseβπ) |
2 | | phlsrng.f |
. . . . 5
β’ πΉ = (Scalarβπ) |
3 | | phllmhm.h |
. . . . 5
β’ , =
(Β·πβπ) |
4 | | eqid 2733 |
. . . . 5
β’
(0gβπ) = (0gβπ) |
5 | | eqid 2733 |
. . . . 5
β’
(*πβπΉ) = (*πβπΉ) |
6 | | eqid 2733 |
. . . . 5
β’
(0gβπΉ) = (0gβπΉ) |
7 | 1, 2, 3, 4, 5, 6 | isphl 21055 |
. . . 4
β’ (π β PreHil β (π β LVec β§ πΉ β *-Ring β§
βπ¦ β π ((π₯ β π β¦ (π₯ , π¦)) β (π LMHom (ringLModβπΉ)) β§ ((π¦ , π¦) = (0gβπΉ) β π¦ = (0gβπ)) β§ βπ₯ β π ((*πβπΉ)β(π¦ , π₯)) = (π₯ , π¦)))) |
8 | 7 | simp3bi 1148 |
. . 3
β’ (π β PreHil β
βπ¦ β π ((π₯ β π β¦ (π₯ , π¦)) β (π LMHom (ringLModβπΉ)) β§ ((π¦ , π¦) = (0gβπΉ) β π¦ = (0gβπ)) β§ βπ₯ β π ((*πβπΉ)β(π¦ , π₯)) = (π₯ , π¦))) |
9 | | simp1 1137 |
. . . 4
β’ (((π₯ β π β¦ (π₯ , π¦)) β (π LMHom (ringLModβπΉ)) β§ ((π¦ , π¦) = (0gβπΉ) β π¦ = (0gβπ)) β§ βπ₯ β π ((*πβπΉ)β(π¦ , π₯)) = (π₯ , π¦)) β (π₯ β π β¦ (π₯ , π¦)) β (π LMHom (ringLModβπΉ))) |
10 | 9 | ralimi 3083 |
. . 3
β’
(βπ¦ β
π ((π₯ β π β¦ (π₯ , π¦)) β (π LMHom (ringLModβπΉ)) β§ ((π¦ , π¦) = (0gβπΉ) β π¦ = (0gβπ)) β§ βπ₯ β π ((*πβπΉ)β(π¦ , π₯)) = (π₯ , π¦)) β βπ¦ β π (π₯ β π β¦ (π₯ , π¦)) β (π LMHom (ringLModβπΉ))) |
11 | 8, 10 | syl 17 |
. 2
β’ (π β PreHil β
βπ¦ β π (π₯ β π β¦ (π₯ , π¦)) β (π LMHom (ringLModβπΉ))) |
12 | | oveq2 7369 |
. . . . . 6
β’ (π¦ = π΄ β (π₯ , π¦) = (π₯ , π΄)) |
13 | 12 | mpteq2dv 5211 |
. . . . 5
β’ (π¦ = π΄ β (π₯ β π β¦ (π₯ , π¦)) = (π₯ β π β¦ (π₯ , π΄))) |
14 | | phllmhm.g |
. . . . 5
β’ πΊ = (π₯ β π β¦ (π₯ , π΄)) |
15 | 13, 14 | eqtr4di 2791 |
. . . 4
β’ (π¦ = π΄ β (π₯ β π β¦ (π₯ , π¦)) = πΊ) |
16 | 15 | eleq1d 2819 |
. . 3
β’ (π¦ = π΄ β ((π₯ β π β¦ (π₯ , π¦)) β (π LMHom (ringLModβπΉ)) β πΊ β (π LMHom (ringLModβπΉ)))) |
17 | 16 | rspccva 3582 |
. 2
β’
((βπ¦ β
π (π₯ β π β¦ (π₯ , π¦)) β (π LMHom (ringLModβπΉ)) β§ π΄ β π) β πΊ β (π LMHom (ringLModβπΉ))) |
18 | 11, 17 | sylan 581 |
1
β’ ((π β PreHil β§ π΄ β π) β πΊ β (π LMHom (ringLModβπΉ))) |