Step | Hyp | Ref
| Expression |
1 | | fvexd 6861 |
. . . 4
β’ (π = π β (Baseβπ) β V) |
2 | | fvexd 6861 |
. . . . 5
β’ ((π = π β§ π£ = (Baseβπ)) β
(Β·πβπ) β V) |
3 | | fvexd 6861 |
. . . . . 6
β’ (((π = π β§ π£ = (Baseβπ)) β§ β =
(Β·πβπ)) β (Scalarβπ) β V) |
4 | | id 22 |
. . . . . . . . 9
β’ (π = (Scalarβπ) β π = (Scalarβπ)) |
5 | | simpll 766 |
. . . . . . . . . . 11
β’ (((π = π β§ π£ = (Baseβπ)) β§ β =
(Β·πβπ)) β π = π) |
6 | 5 | fveq2d 6850 |
. . . . . . . . . 10
β’ (((π = π β§ π£ = (Baseβπ)) β§ β =
(Β·πβπ)) β (Scalarβπ) = (Scalarβπ)) |
7 | | isphl.f |
. . . . . . . . . 10
β’ πΉ = (Scalarβπ) |
8 | 6, 7 | eqtr4di 2791 |
. . . . . . . . 9
β’ (((π = π β§ π£ = (Baseβπ)) β§ β =
(Β·πβπ)) β (Scalarβπ) = πΉ) |
9 | 4, 8 | sylan9eqr 2795 |
. . . . . . . 8
β’ ((((π = π β§ π£ = (Baseβπ)) β§ β =
(Β·πβπ)) β§ π = (Scalarβπ)) β π = πΉ) |
10 | 9 | eleq1d 2819 |
. . . . . . 7
β’ ((((π = π β§ π£ = (Baseβπ)) β§ β =
(Β·πβπ)) β§ π = (Scalarβπ)) β (π β *-Ring β πΉ β *-Ring)) |
11 | | simpllr 775 |
. . . . . . . . 9
β’ ((((π = π β§ π£ = (Baseβπ)) β§ β =
(Β·πβπ)) β§ π = (Scalarβπ)) β π£ = (Baseβπ)) |
12 | | simplll 774 |
. . . . . . . . . . 11
β’ ((((π = π β§ π£ = (Baseβπ)) β§ β =
(Β·πβπ)) β§ π = (Scalarβπ)) β π = π) |
13 | 12 | fveq2d 6850 |
. . . . . . . . . 10
β’ ((((π = π β§ π£ = (Baseβπ)) β§ β =
(Β·πβπ)) β§ π = (Scalarβπ)) β (Baseβπ) = (Baseβπ)) |
14 | | isphl.v |
. . . . . . . . . 10
β’ π = (Baseβπ) |
15 | 13, 14 | eqtr4di 2791 |
. . . . . . . . 9
β’ ((((π = π β§ π£ = (Baseβπ)) β§ β =
(Β·πβπ)) β§ π = (Scalarβπ)) β (Baseβπ) = π) |
16 | 11, 15 | eqtrd 2773 |
. . . . . . . 8
β’ ((((π = π β§ π£ = (Baseβπ)) β§ β =
(Β·πβπ)) β§ π = (Scalarβπ)) β π£ = π) |
17 | | simplr 768 |
. . . . . . . . . . . . 13
β’ ((((π = π β§ π£ = (Baseβπ)) β§ β =
(Β·πβπ)) β§ π = (Scalarβπ)) β β =
(Β·πβπ)) |
18 | 12 | fveq2d 6850 |
. . . . . . . . . . . . . 14
β’ ((((π = π β§ π£ = (Baseβπ)) β§ β =
(Β·πβπ)) β§ π = (Scalarβπ)) β
(Β·πβπ) =
(Β·πβπ)) |
19 | | isphl.h |
. . . . . . . . . . . . . 14
β’ , =
(Β·πβπ) |
20 | 18, 19 | eqtr4di 2791 |
. . . . . . . . . . . . 13
β’ ((((π = π β§ π£ = (Baseβπ)) β§ β =
(Β·πβπ)) β§ π = (Scalarβπ)) β
(Β·πβπ) = , ) |
21 | 17, 20 | eqtrd 2773 |
. . . . . . . . . . . 12
β’ ((((π = π β§ π£ = (Baseβπ)) β§ β =
(Β·πβπ)) β§ π = (Scalarβπ)) β β = , ) |
22 | 21 | oveqd 7378 |
. . . . . . . . . . 11
β’ ((((π = π β§ π£ = (Baseβπ)) β§ β =
(Β·πβπ)) β§ π = (Scalarβπ)) β (π¦βπ₯) = (π¦ , π₯)) |
23 | 16, 22 | mpteq12dv 5200 |
. . . . . . . . . 10
β’ ((((π = π β§ π£ = (Baseβπ)) β§ β =
(Β·πβπ)) β§ π = (Scalarβπ)) β (π¦ β π£ β¦ (π¦βπ₯)) = (π¦ β π β¦ (π¦ , π₯))) |
24 | 9 | fveq2d 6850 |
. . . . . . . . . . 11
β’ ((((π = π β§ π£ = (Baseβπ)) β§ β =
(Β·πβπ)) β§ π = (Scalarβπ)) β (ringLModβπ) = (ringLModβπΉ)) |
25 | 12, 24 | oveq12d 7379 |
. . . . . . . . . 10
β’ ((((π = π β§ π£ = (Baseβπ)) β§ β =
(Β·πβπ)) β§ π = (Scalarβπ)) β (π LMHom (ringLModβπ)) = (π LMHom (ringLModβπΉ))) |
26 | 23, 25 | eleq12d 2828 |
. . . . . . . . 9
β’ ((((π = π β§ π£ = (Baseβπ)) β§ β =
(Β·πβπ)) β§ π = (Scalarβπ)) β ((π¦ β π£ β¦ (π¦βπ₯)) β (π LMHom (ringLModβπ)) β (π¦ β π β¦ (π¦ , π₯)) β (π LMHom (ringLModβπΉ)))) |
27 | 21 | oveqd 7378 |
. . . . . . . . . . 11
β’ ((((π = π β§ π£ = (Baseβπ)) β§ β =
(Β·πβπ)) β§ π = (Scalarβπ)) β (π₯βπ₯) = (π₯ , π₯)) |
28 | 9 | fveq2d 6850 |
. . . . . . . . . . . 12
β’ ((((π = π β§ π£ = (Baseβπ)) β§ β =
(Β·πβπ)) β§ π = (Scalarβπ)) β (0gβπ) = (0gβπΉ)) |
29 | | isphl.z |
. . . . . . . . . . . 12
β’ π = (0gβπΉ) |
30 | 28, 29 | eqtr4di 2791 |
. . . . . . . . . . 11
β’ ((((π = π β§ π£ = (Baseβπ)) β§ β =
(Β·πβπ)) β§ π = (Scalarβπ)) β (0gβπ) = π) |
31 | 27, 30 | eqeq12d 2749 |
. . . . . . . . . 10
β’ ((((π = π β§ π£ = (Baseβπ)) β§ β =
(Β·πβπ)) β§ π = (Scalarβπ)) β ((π₯βπ₯) = (0gβπ) β (π₯ , π₯) = π)) |
32 | 12 | fveq2d 6850 |
. . . . . . . . . . . 12
β’ ((((π = π β§ π£ = (Baseβπ)) β§ β =
(Β·πβπ)) β§ π = (Scalarβπ)) β (0gβπ) = (0gβπ)) |
33 | | isphl.o |
. . . . . . . . . . . 12
β’ 0 =
(0gβπ) |
34 | 32, 33 | eqtr4di 2791 |
. . . . . . . . . . 11
β’ ((((π = π β§ π£ = (Baseβπ)) β§ β =
(Β·πβπ)) β§ π = (Scalarβπ)) β (0gβπ) = 0 ) |
35 | 34 | eqeq2d 2744 |
. . . . . . . . . 10
β’ ((((π = π β§ π£ = (Baseβπ)) β§ β =
(Β·πβπ)) β§ π = (Scalarβπ)) β (π₯ = (0gβπ) β π₯ = 0 )) |
36 | 31, 35 | imbi12d 345 |
. . . . . . . . 9
β’ ((((π = π β§ π£ = (Baseβπ)) β§ β =
(Β·πβπ)) β§ π = (Scalarβπ)) β (((π₯βπ₯) = (0gβπ) β π₯ = (0gβπ)) β ((π₯ , π₯) = π β π₯ = 0 ))) |
37 | 9 | fveq2d 6850 |
. . . . . . . . . . . . 13
β’ ((((π = π β§ π£ = (Baseβπ)) β§ β =
(Β·πβπ)) β§ π = (Scalarβπ)) β (*πβπ) =
(*πβπΉ)) |
38 | | isphl.i |
. . . . . . . . . . . . 13
β’ β =
(*πβπΉ) |
39 | 37, 38 | eqtr4di 2791 |
. . . . . . . . . . . 12
β’ ((((π = π β§ π£ = (Baseβπ)) β§ β =
(Β·πβπ)) β§ π = (Scalarβπ)) β (*πβπ) = β ) |
40 | 21 | oveqd 7378 |
. . . . . . . . . . . 12
β’ ((((π = π β§ π£ = (Baseβπ)) β§ β =
(Β·πβπ)) β§ π = (Scalarβπ)) β (π₯βπ¦) = (π₯ , π¦)) |
41 | 39, 40 | fveq12d 6853 |
. . . . . . . . . . 11
β’ ((((π = π β§ π£ = (Baseβπ)) β§ β =
(Β·πβπ)) β§ π = (Scalarβπ)) β ((*πβπ)β(π₯βπ¦)) = ( β β(π₯ , π¦))) |
42 | 41, 22 | eqeq12d 2749 |
. . . . . . . . . 10
β’ ((((π = π β§ π£ = (Baseβπ)) β§ β =
(Β·πβπ)) β§ π = (Scalarβπ)) β
(((*πβπ)β(π₯βπ¦)) = (π¦βπ₯) β ( β β(π₯ , π¦)) = (π¦ , π₯))) |
43 | 16, 42 | raleqbidv 3318 |
. . . . . . . . 9
β’ ((((π = π β§ π£ = (Baseβπ)) β§ β =
(Β·πβπ)) β§ π = (Scalarβπ)) β (βπ¦ β π£ ((*πβπ)β(π₯βπ¦)) = (π¦βπ₯) β βπ¦ β π ( β β(π₯ , π¦)) = (π¦ , π₯))) |
44 | 26, 36, 43 | 3anbi123d 1437 |
. . . . . . . 8
β’ ((((π = π β§ π£ = (Baseβπ)) β§ β =
(Β·πβπ)) β§ π = (Scalarβπ)) β (((π¦ β π£ β¦ (π¦βπ₯)) β (π LMHom (ringLModβπ)) β§ ((π₯βπ₯) = (0gβπ) β π₯ = (0gβπ)) β§ βπ¦ β π£ ((*πβπ)β(π₯βπ¦)) = (π¦βπ₯)) β ((π¦ β π β¦ (π¦ , π₯)) β (π LMHom (ringLModβπΉ)) β§ ((π₯ , π₯) = π β π₯ = 0 ) β§ βπ¦ β π ( β β(π₯ , π¦)) = (π¦ , π₯)))) |
45 | 16, 44 | raleqbidv 3318 |
. . . . . . 7
β’ ((((π = π β§ π£ = (Baseβπ)) β§ β =
(Β·πβπ)) β§ π = (Scalarβπ)) β (βπ₯ β π£ ((π¦ β π£ β¦ (π¦βπ₯)) β (π LMHom (ringLModβπ)) β§ ((π₯βπ₯) = (0gβπ) β π₯ = (0gβπ)) β§ βπ¦ β π£ ((*πβπ)β(π₯βπ¦)) = (π¦βπ₯)) β βπ₯ β π ((π¦ β π β¦ (π¦ , π₯)) β (π LMHom (ringLModβπΉ)) β§ ((π₯ , π₯) = π β π₯ = 0 ) β§ βπ¦ β π ( β β(π₯ , π¦)) = (π¦ , π₯)))) |
46 | 10, 45 | anbi12d 632 |
. . . . . 6
β’ ((((π = π β§ π£ = (Baseβπ)) β§ β =
(Β·πβπ)) β§ π = (Scalarβπ)) β ((π β *-Ring β§ βπ₯ β π£ ((π¦ β π£ β¦ (π¦βπ₯)) β (π LMHom (ringLModβπ)) β§ ((π₯βπ₯) = (0gβπ) β π₯ = (0gβπ)) β§ βπ¦ β π£ ((*πβπ)β(π₯βπ¦)) = (π¦βπ₯))) β (πΉ β *-Ring β§ βπ₯ β π ((π¦ β π β¦ (π¦ , π₯)) β (π LMHom (ringLModβπΉ)) β§ ((π₯ , π₯) = π β π₯ = 0 ) β§ βπ¦ β π ( β β(π₯ , π¦)) = (π¦ , π₯))))) |
47 | 3, 46 | sbcied 3788 |
. . . . 5
β’ (((π = π β§ π£ = (Baseβπ)) β§ β =
(Β·πβπ)) β ([(Scalarβπ) / π](π β *-Ring β§ βπ₯ β π£ ((π¦ β π£ β¦ (π¦βπ₯)) β (π LMHom (ringLModβπ)) β§ ((π₯βπ₯) = (0gβπ) β π₯ = (0gβπ)) β§ βπ¦ β π£ ((*πβπ)β(π₯βπ¦)) = (π¦βπ₯))) β (πΉ β *-Ring β§ βπ₯ β π ((π¦ β π β¦ (π¦ , π₯)) β (π LMHom (ringLModβπΉ)) β§ ((π₯ , π₯) = π β π₯ = 0 ) β§ βπ¦ β π ( β β(π₯ , π¦)) = (π¦ , π₯))))) |
48 | 2, 47 | sbcied 3788 |
. . . 4
β’ ((π = π β§ π£ = (Baseβπ)) β
([(Β·πβπ) / β][(Scalarβπ) / π](π β *-Ring β§ βπ₯ β π£ ((π¦ β π£ β¦ (π¦βπ₯)) β (π LMHom (ringLModβπ)) β§ ((π₯βπ₯) = (0gβπ) β π₯ = (0gβπ)) β§ βπ¦ β π£ ((*πβπ)β(π₯βπ¦)) = (π¦βπ₯))) β (πΉ β *-Ring β§ βπ₯ β π ((π¦ β π β¦ (π¦ , π₯)) β (π LMHom (ringLModβπΉ)) β§ ((π₯ , π₯) = π β π₯ = 0 ) β§ βπ¦ β π ( β β(π₯ , π¦)) = (π¦ , π₯))))) |
49 | 1, 48 | sbcied 3788 |
. . 3
β’ (π = π β ([(Baseβπ) / π£][(Β·πβπ) / β][(Scalarβπ) / π](π
β *-Ring β§ βπ₯ β π£ ((π¦ β π£
β¦ (π¦βπ₯)) β
(π LMHom (ringLModβπ)) β§ ((π₯βπ₯) = (0gβπ) β π₯ =
(0gβπ)) β§ βπ¦ β π£ ((*πβπ)β(π₯βπ¦)) = (π¦βπ₯))) β (πΉ β *-Ring β§ βπ₯ β π
((π¦ β π β¦ (π¦
, π₯)) β (π
LMHom (ringLModβπΉ)) β§ ((π₯ , π₯) = π β
π₯ = 0 ) β§ βπ¦ β π (
β β(π₯ , π¦)) = (π¦
, π₯))))) |
50 | | df-phl 21053 |
. . 3
β’ PreHil =
{π β LVec β£
[(Baseβπ) /
π£][(Β·πβπ) / β][(Scalarβπ) / π](π
β *-Ring β§ βπ₯ β π£ ((π¦ β π£
β¦ (π¦βπ₯)) β
(π LMHom (ringLModβπ)) β§ ((π₯βπ₯) = (0gβπ) β π₯ =
(0gβπ)) β§ βπ¦ β π£ ((*πβπ)β(π₯βπ¦)) = (π¦βπ₯)))} |
51 | 49, 50 | elrab2 3652 |
. 2
β’ (π β PreHil β (π β LVec β§ (πΉ β *-Ring β§
βπ₯ β π ((π¦ β π β¦ (π¦ , π₯)) β (π LMHom (ringLModβπΉ)) β§ ((π₯ , π₯) = π β π₯ = 0 ) β§ βπ¦ β π ( β β(π₯ , π¦)) = (π¦ , π₯))))) |
52 | | 3anass 1096 |
. 2
β’ ((π β LVec β§ πΉ β *-Ring β§
βπ₯ β π ((π¦ β π β¦ (π¦ , π₯)) β (π LMHom (ringLModβπΉ)) β§ ((π₯ , π₯) = π β π₯ = 0 ) β§ βπ¦ β π ( β β(π₯ , π¦)) = (π¦ , π₯))) β (π β LVec β§ (πΉ β *-Ring β§ βπ₯ β π ((π¦ β π β¦ (π¦ , π₯)) β (π LMHom (ringLModβπΉ)) β§ ((π₯ , π₯) = π β π₯ = 0 ) β§ βπ¦ β π ( β β(π₯ , π¦)) = (π¦ , π₯))))) |
53 | 51, 52 | bitr4i 278 |
1
β’ (π β PreHil β (π β LVec β§ πΉ β *-Ring β§
βπ₯ β π ((π¦ β π β¦ (π¦ , π₯)) β (π LMHom (ringLModβπΉ)) β§ ((π₯ , π₯) = π β π₯ = 0 ) β§ βπ¦ β π ( β β(π₯ , π¦)) = (π¦ , π₯)))) |