Step | Hyp | Ref
| Expression |
1 | | phlpropd.1 |
. . . 4
β’ (π β π΅ = (BaseβπΎ)) |
2 | | phlpropd.2 |
. . . 4
β’ (π β π΅ = (BaseβπΏ)) |
3 | | phlpropd.3 |
. . . 4
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(+gβπΎ)π¦) = (π₯(+gβπΏ)π¦)) |
4 | | phlpropd.4 |
. . . 4
β’ (π β πΉ = (ScalarβπΎ)) |
5 | | phlpropd.5 |
. . . 4
β’ (π β πΉ = (ScalarβπΏ)) |
6 | | phlpropd.6 |
. . . 4
β’ π = (BaseβπΉ) |
7 | | phlpropd.7 |
. . . 4
β’ ((π β§ (π₯ β π β§ π¦ β π΅)) β (π₯( Β·π
βπΎ)π¦) = (π₯( Β·π
βπΏ)π¦)) |
8 | 1, 2, 3, 4, 5, 6, 7 | lvecpropd 20673 |
. . 3
β’ (π β (πΎ β LVec β πΏ β LVec)) |
9 | 4, 5 | eqtr3d 2775 |
. . . 4
β’ (π β (ScalarβπΎ) = (ScalarβπΏ)) |
10 | 9 | eleq1d 2819 |
. . 3
β’ (π β ((ScalarβπΎ) β *-Ring β
(ScalarβπΏ) β
*-Ring)) |
11 | | phlpropd.8 |
. . . . . . . . . . 11
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(Β·πβπΎ)π¦) = (π₯(Β·πβπΏ)π¦)) |
12 | 11 | oveqrspc2v 7388 |
. . . . . . . . . 10
β’ ((π β§ (π β π΅ β§ π β π΅)) β (π(Β·πβπΎ)π) = (π(Β·πβπΏ)π)) |
13 | 12 | anass1rs 654 |
. . . . . . . . 9
β’ (((π β§ π β π΅) β§ π β π΅) β (π(Β·πβπΎ)π) = (π(Β·πβπΏ)π)) |
14 | 13 | mpteq2dva 5209 |
. . . . . . . 8
β’ ((π β§ π β π΅) β (π β π΅ β¦ (π(Β·πβπΎ)π)) = (π β π΅ β¦ (π(Β·πβπΏ)π))) |
15 | 1 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β π΅) β π΅ = (BaseβπΎ)) |
16 | 15 | mpteq1d 5204 |
. . . . . . . 8
β’ ((π β§ π β π΅) β (π β π΅ β¦ (π(Β·πβπΎ)π)) = (π β (BaseβπΎ) β¦ (π(Β·πβπΎ)π))) |
17 | 2 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π β π΅) β π΅ = (BaseβπΏ)) |
18 | 17 | mpteq1d 5204 |
. . . . . . . 8
β’ ((π β§ π β π΅) β (π β π΅ β¦ (π(Β·πβπΏ)π)) = (π β (BaseβπΏ) β¦ (π(Β·πβπΏ)π))) |
19 | 14, 16, 18 | 3eqtr3d 2781 |
. . . . . . 7
β’ ((π β§ π β π΅) β (π β (BaseβπΎ) β¦ (π(Β·πβπΎ)π)) = (π β (BaseβπΏ) β¦ (π(Β·πβπΏ)π))) |
20 | | rlmbas 20709 |
. . . . . . . . . . . 12
β’
(BaseβπΉ) =
(Baseβ(ringLModβπΉ)) |
21 | 6, 20 | eqtri 2761 |
. . . . . . . . . . 11
β’ π =
(Baseβ(ringLModβπΉ)) |
22 | 21 | a1i 11 |
. . . . . . . . . 10
β’ (π β π = (Baseβ(ringLModβπΉ))) |
23 | | fvex 6859 |
. . . . . . . . . . . 12
β’
(ScalarβπΎ)
β V |
24 | 4, 23 | eqeltrdi 2842 |
. . . . . . . . . . 11
β’ (π β πΉ β V) |
25 | | rlmsca 20714 |
. . . . . . . . . . 11
β’ (πΉ β V β πΉ =
(Scalarβ(ringLModβπΉ))) |
26 | 24, 25 | syl 17 |
. . . . . . . . . 10
β’ (π β πΉ = (Scalarβ(ringLModβπΉ))) |
27 | | eqidd 2734 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯(+gβ(ringLModβπΉ))π¦) = (π₯(+gβ(ringLModβπΉ))π¦)) |
28 | | eqidd 2734 |
. . . . . . . . . 10
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯( Β·π
β(ringLModβπΉ))π¦) = (π₯( Β·π
β(ringLModβπΉ))π¦)) |
29 | 1, 22, 2, 22, 4, 26, 5, 26, 6, 6, 3, 27,
7, 28 | lmhmpropd 20578 |
. . . . . . . . 9
β’ (π β (πΎ LMHom (ringLModβπΉ)) = (πΏ LMHom (ringLModβπΉ))) |
30 | 4 | fveq2d 6850 |
. . . . . . . . . 10
β’ (π β (ringLModβπΉ) =
(ringLModβ(ScalarβπΎ))) |
31 | 30 | oveq2d 7377 |
. . . . . . . . 9
β’ (π β (πΎ LMHom (ringLModβπΉ)) = (πΎ LMHom (ringLModβ(ScalarβπΎ)))) |
32 | 5 | fveq2d 6850 |
. . . . . . . . . 10
β’ (π β (ringLModβπΉ) =
(ringLModβ(ScalarβπΏ))) |
33 | 32 | oveq2d 7377 |
. . . . . . . . 9
β’ (π β (πΏ LMHom (ringLModβπΉ)) = (πΏ LMHom (ringLModβ(ScalarβπΏ)))) |
34 | 29, 31, 33 | 3eqtr3d 2781 |
. . . . . . . 8
β’ (π β (πΎ LMHom (ringLModβ(ScalarβπΎ))) = (πΏ LMHom (ringLModβ(ScalarβπΏ)))) |
35 | 34 | adantr 482 |
. . . . . . 7
β’ ((π β§ π β π΅) β (πΎ LMHom (ringLModβ(ScalarβπΎ))) = (πΏ LMHom (ringLModβ(ScalarβπΏ)))) |
36 | 19, 35 | eleq12d 2828 |
. . . . . 6
β’ ((π β§ π β π΅) β ((π β (BaseβπΎ) β¦ (π(Β·πβπΎ)π)) β (πΎ LMHom (ringLModβ(ScalarβπΎ))) β (π β (BaseβπΏ) β¦ (π(Β·πβπΏ)π)) β (πΏ LMHom (ringLModβ(ScalarβπΏ))))) |
37 | 11 | oveqrspc2v 7388 |
. . . . . . . . 9
β’ ((π β§ (π β π΅ β§ π β π΅)) β (π(Β·πβπΎ)π) = (π(Β·πβπΏ)π)) |
38 | 37 | anabsan2 673 |
. . . . . . . 8
β’ ((π β§ π β π΅) β (π(Β·πβπΎ)π) = (π(Β·πβπΏ)π)) |
39 | 9 | fveq2d 6850 |
. . . . . . . . 9
β’ (π β
(0gβ(ScalarβπΎ)) =
(0gβ(ScalarβπΏ))) |
40 | 39 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β π΅) β
(0gβ(ScalarβπΎ)) =
(0gβ(ScalarβπΏ))) |
41 | 38, 40 | eqeq12d 2749 |
. . . . . . 7
β’ ((π β§ π β π΅) β ((π(Β·πβπΎ)π) = (0gβ(ScalarβπΎ)) β (π(Β·πβπΏ)π) = (0gβ(ScalarβπΏ)))) |
42 | 1, 2, 3 | grpidpropd 18525 |
. . . . . . . . 9
β’ (π β (0gβπΎ) = (0gβπΏ)) |
43 | 42 | adantr 482 |
. . . . . . . 8
β’ ((π β§ π β π΅) β (0gβπΎ) = (0gβπΏ)) |
44 | 43 | eqeq2d 2744 |
. . . . . . 7
β’ ((π β§ π β π΅) β (π = (0gβπΎ) β π = (0gβπΏ))) |
45 | 41, 44 | imbi12d 345 |
. . . . . 6
β’ ((π β§ π β π΅) β (((π(Β·πβπΎ)π) = (0gβ(ScalarβπΎ)) β π = (0gβπΎ)) β ((π(Β·πβπΏ)π) = (0gβ(ScalarβπΏ)) β π = (0gβπΏ)))) |
46 | 9 | fveq2d 6850 |
. . . . . . . . . . . 12
β’ (π β
(*πβ(ScalarβπΎ)) =
(*πβ(ScalarβπΏ))) |
47 | 46 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ (π β π΅ β§ π β π΅)) β
(*πβ(ScalarβπΎ)) =
(*πβ(ScalarβπΏ))) |
48 | 11 | oveqrspc2v 7388 |
. . . . . . . . . . 11
β’ ((π β§ (π β π΅ β§ π β π΅)) β (π(Β·πβπΎ)π) = (π(Β·πβπΏ)π)) |
49 | 47, 48 | fveq12d 6853 |
. . . . . . . . . 10
β’ ((π β§ (π β π΅ β§ π β π΅)) β
((*πβ(ScalarβπΎ))β(π(Β·πβπΎ)π)) =
((*πβ(ScalarβπΏ))β(π(Β·πβπΏ)π))) |
50 | 49 | anassrs 469 |
. . . . . . . . 9
β’ (((π β§ π β π΅) β§ π β π΅) β
((*πβ(ScalarβπΎ))β(π(Β·πβπΎ)π)) =
((*πβ(ScalarβπΏ))β(π(Β·πβπΏ)π))) |
51 | 50, 13 | eqeq12d 2749 |
. . . . . . . 8
β’ (((π β§ π β π΅) β§ π β π΅) β
(((*πβ(ScalarβπΎ))β(π(Β·πβπΎ)π)) = (π(Β·πβπΎ)π) β
((*πβ(ScalarβπΏ))β(π(Β·πβπΏ)π)) = (π(Β·πβπΏ)π))) |
52 | 51 | ralbidva 3169 |
. . . . . . 7
β’ ((π β§ π β π΅) β (βπ β π΅
((*πβ(ScalarβπΎ))β(π(Β·πβπΎ)π)) = (π(Β·πβπΎ)π) β βπ β π΅
((*πβ(ScalarβπΏ))β(π(Β·πβπΏ)π)) = (π(Β·πβπΏ)π))) |
53 | 15 | raleqdv 3312 |
. . . . . . 7
β’ ((π β§ π β π΅) β (βπ β π΅
((*πβ(ScalarβπΎ))β(π(Β·πβπΎ)π)) = (π(Β·πβπΎ)π) β βπ β (BaseβπΎ)((*πβ(ScalarβπΎ))β(π(Β·πβπΎ)π)) = (π(Β·πβπΎ)π))) |
54 | 17 | raleqdv 3312 |
. . . . . . 7
β’ ((π β§ π β π΅) β (βπ β π΅
((*πβ(ScalarβπΏ))β(π(Β·πβπΏ)π)) = (π(Β·πβπΏ)π) β βπ β (BaseβπΏ)((*πβ(ScalarβπΏ))β(π(Β·πβπΏ)π)) = (π(Β·πβπΏ)π))) |
55 | 52, 53, 54 | 3bitr3d 309 |
. . . . . 6
β’ ((π β§ π β π΅) β (βπ β (BaseβπΎ)((*πβ(ScalarβπΎ))β(π(Β·πβπΎ)π)) = (π(Β·πβπΎ)π) β βπ β (BaseβπΏ)((*πβ(ScalarβπΏ))β(π(Β·πβπΏ)π)) = (π(Β·πβπΏ)π))) |
56 | 36, 45, 55 | 3anbi123d 1437 |
. . . . 5
β’ ((π β§ π β π΅) β (((π β (BaseβπΎ) β¦ (π(Β·πβπΎ)π)) β (πΎ LMHom (ringLModβ(ScalarβπΎ))) β§ ((π(Β·πβπΎ)π) = (0gβ(ScalarβπΎ)) β π = (0gβπΎ)) β§ βπ β (BaseβπΎ)((*πβ(ScalarβπΎ))β(π(Β·πβπΎ)π)) = (π(Β·πβπΎ)π)) β ((π β (BaseβπΏ) β¦ (π(Β·πβπΏ)π)) β (πΏ LMHom (ringLModβ(ScalarβπΏ))) β§ ((π(Β·πβπΏ)π) = (0gβ(ScalarβπΏ)) β π = (0gβπΏ)) β§ βπ β (BaseβπΏ)((*πβ(ScalarβπΏ))β(π(Β·πβπΏ)π)) = (π(Β·πβπΏ)π)))) |
57 | 56 | ralbidva 3169 |
. . . 4
β’ (π β (βπ β π΅ ((π β (BaseβπΎ) β¦ (π(Β·πβπΎ)π)) β (πΎ LMHom (ringLModβ(ScalarβπΎ))) β§ ((π(Β·πβπΎ)π) = (0gβ(ScalarβπΎ)) β π = (0gβπΎ)) β§ βπ β (BaseβπΎ)((*πβ(ScalarβπΎ))β(π(Β·πβπΎ)π)) = (π(Β·πβπΎ)π)) β βπ β π΅ ((π β (BaseβπΏ) β¦ (π(Β·πβπΏ)π)) β (πΏ LMHom (ringLModβ(ScalarβπΏ))) β§ ((π(Β·πβπΏ)π) = (0gβ(ScalarβπΏ)) β π = (0gβπΏ)) β§ βπ β (BaseβπΏ)((*πβ(ScalarβπΏ))β(π(Β·πβπΏ)π)) = (π(Β·πβπΏ)π)))) |
58 | 1 | raleqdv 3312 |
. . . 4
β’ (π β (βπ β π΅ ((π β (BaseβπΎ) β¦ (π(Β·πβπΎ)π)) β (πΎ LMHom (ringLModβ(ScalarβπΎ))) β§ ((π(Β·πβπΎ)π) = (0gβ(ScalarβπΎ)) β π = (0gβπΎ)) β§ βπ β (BaseβπΎ)((*πβ(ScalarβπΎ))β(π(Β·πβπΎ)π)) = (π(Β·πβπΎ)π)) β βπ β (BaseβπΎ)((π β (BaseβπΎ) β¦ (π(Β·πβπΎ)π)) β (πΎ LMHom (ringLModβ(ScalarβπΎ))) β§ ((π(Β·πβπΎ)π) = (0gβ(ScalarβπΎ)) β π = (0gβπΎ)) β§ βπ β (BaseβπΎ)((*πβ(ScalarβπΎ))β(π(Β·πβπΎ)π)) = (π(Β·πβπΎ)π)))) |
59 | 2 | raleqdv 3312 |
. . . 4
β’ (π β (βπ β π΅ ((π β (BaseβπΏ) β¦ (π(Β·πβπΏ)π)) β (πΏ LMHom (ringLModβ(ScalarβπΏ))) β§ ((π(Β·πβπΏ)π) = (0gβ(ScalarβπΏ)) β π = (0gβπΏ)) β§ βπ β (BaseβπΏ)((*πβ(ScalarβπΏ))β(π(Β·πβπΏ)π)) = (π(Β·πβπΏ)π)) β βπ β (BaseβπΏ)((π β (BaseβπΏ) β¦ (π(Β·πβπΏ)π)) β (πΏ LMHom (ringLModβ(ScalarβπΏ))) β§ ((π(Β·πβπΏ)π) = (0gβ(ScalarβπΏ)) β π = (0gβπΏ)) β§ βπ β (BaseβπΏ)((*πβ(ScalarβπΏ))β(π(Β·πβπΏ)π)) = (π(Β·πβπΏ)π)))) |
60 | 57, 58, 59 | 3bitr3d 309 |
. . 3
β’ (π β (βπ β (BaseβπΎ)((π β (BaseβπΎ) β¦ (π(Β·πβπΎ)π)) β (πΎ LMHom (ringLModβ(ScalarβπΎ))) β§ ((π(Β·πβπΎ)π) = (0gβ(ScalarβπΎ)) β π = (0gβπΎ)) β§ βπ β (BaseβπΎ)((*πβ(ScalarβπΎ))β(π(Β·πβπΎ)π)) = (π(Β·πβπΎ)π)) β βπ β (BaseβπΏ)((π β (BaseβπΏ) β¦ (π(Β·πβπΏ)π)) β (πΏ LMHom (ringLModβ(ScalarβπΏ))) β§ ((π(Β·πβπΏ)π) = (0gβ(ScalarβπΏ)) β π = (0gβπΏ)) β§ βπ β (BaseβπΏ)((*πβ(ScalarβπΏ))β(π(Β·πβπΏ)π)) = (π(Β·πβπΏ)π)))) |
61 | 8, 10, 60 | 3anbi123d 1437 |
. 2
β’ (π β ((πΎ β LVec β§ (ScalarβπΎ) β *-Ring β§
βπ β
(BaseβπΎ)((π β (BaseβπΎ) β¦ (π(Β·πβπΎ)π)) β (πΎ LMHom (ringLModβ(ScalarβπΎ))) β§ ((π(Β·πβπΎ)π) = (0gβ(ScalarβπΎ)) β π = (0gβπΎ)) β§ βπ β (BaseβπΎ)((*πβ(ScalarβπΎ))β(π(Β·πβπΎ)π)) = (π(Β·πβπΎ)π))) β (πΏ β LVec β§ (ScalarβπΏ) β *-Ring β§ βπ β (BaseβπΏ)((π β (BaseβπΏ) β¦ (π(Β·πβπΏ)π)) β (πΏ LMHom (ringLModβ(ScalarβπΏ))) β§ ((π(Β·πβπΏ)π) = (0gβ(ScalarβπΏ)) β π = (0gβπΏ)) β§ βπ β (BaseβπΏ)((*πβ(ScalarβπΏ))β(π(Β·πβπΏ)π)) = (π(Β·πβπΏ)π))))) |
62 | | eqid 2733 |
. . 3
β’
(BaseβπΎ) =
(BaseβπΎ) |
63 | | eqid 2733 |
. . 3
β’
(ScalarβπΎ) =
(ScalarβπΎ) |
64 | | eqid 2733 |
. . 3
β’
(Β·πβπΎ) =
(Β·πβπΎ) |
65 | | eqid 2733 |
. . 3
β’
(0gβπΎ) = (0gβπΎ) |
66 | | eqid 2733 |
. . 3
β’
(*πβ(ScalarβπΎ)) =
(*πβ(ScalarβπΎ)) |
67 | | eqid 2733 |
. . 3
β’
(0gβ(ScalarβπΎ)) =
(0gβ(ScalarβπΎ)) |
68 | 62, 63, 64, 65, 66, 67 | isphl 21055 |
. 2
β’ (πΎ β PreHil β (πΎ β LVec β§
(ScalarβπΎ) β
*-Ring β§ βπ
β (BaseβπΎ)((π β (BaseβπΎ) β¦ (π(Β·πβπΎ)π)) β (πΎ LMHom (ringLModβ(ScalarβπΎ))) β§ ((π(Β·πβπΎ)π) = (0gβ(ScalarβπΎ)) β π = (0gβπΎ)) β§ βπ β (BaseβπΎ)((*πβ(ScalarβπΎ))β(π(Β·πβπΎ)π)) = (π(Β·πβπΎ)π)))) |
69 | | eqid 2733 |
. . 3
β’
(BaseβπΏ) =
(BaseβπΏ) |
70 | | eqid 2733 |
. . 3
β’
(ScalarβπΏ) =
(ScalarβπΏ) |
71 | | eqid 2733 |
. . 3
β’
(Β·πβπΏ) =
(Β·πβπΏ) |
72 | | eqid 2733 |
. . 3
β’
(0gβπΏ) = (0gβπΏ) |
73 | | eqid 2733 |
. . 3
β’
(*πβ(ScalarβπΏ)) =
(*πβ(ScalarβπΏ)) |
74 | | eqid 2733 |
. . 3
β’
(0gβ(ScalarβπΏ)) =
(0gβ(ScalarβπΏ)) |
75 | 69, 70, 71, 72, 73, 74 | isphl 21055 |
. 2
β’ (πΏ β PreHil β (πΏ β LVec β§
(ScalarβπΏ) β
*-Ring β§ βπ
β (BaseβπΏ)((π β (BaseβπΏ) β¦ (π(Β·πβπΏ)π)) β (πΏ LMHom (ringLModβ(ScalarβπΏ))) β§ ((π(Β·πβπΏ)π) = (0gβ(ScalarβπΏ)) β π = (0gβπΏ)) β§ βπ β (BaseβπΏ)((*πβ(ScalarβπΏ))β(π(Β·πβπΏ)π)) = (π(Β·πβπΏ)π)))) |
76 | 61, 68, 75 | 3bitr4g 314 |
1
β’ (π β (πΎ β PreHil β πΏ β PreHil)) |