Step | Hyp | Ref
| Expression |
1 | | df-lmhm 20498 |
. . 3
β’ LMHom =
(π β LMod, π‘ β LMod β¦ {π β (π GrpHom π‘) β£ [(Scalarβπ ) / π€]((Scalarβπ‘) = π€ β§ βπ₯ β (Baseβπ€)βπ¦ β (Baseβπ )(πβ(π₯( Β·π
βπ )π¦)) = (π₯( Β·π
βπ‘)(πβπ¦)))}) |
2 | 1 | elmpocl 7596 |
. 2
β’ (πΉ β (π LMHom π) β (π β LMod β§ π β LMod)) |
3 | | oveq12 7367 |
. . . . . 6
β’ ((π = π β§ π‘ = π) β (π GrpHom π‘) = (π GrpHom π)) |
4 | | fvexd 6858 |
. . . . . . 7
β’ ((π = π β§ π‘ = π) β (Scalarβπ ) β V) |
5 | | simplr 768 |
. . . . . . . . . . 11
β’ (((π = π β§ π‘ = π) β§ π€ = (Scalarβπ )) β π‘ = π) |
6 | 5 | fveq2d 6847 |
. . . . . . . . . 10
β’ (((π = π β§ π‘ = π) β§ π€ = (Scalarβπ )) β (Scalarβπ‘) = (Scalarβπ)) |
7 | | islmhm.l |
. . . . . . . . . 10
β’ πΏ = (Scalarβπ) |
8 | 6, 7 | eqtr4di 2791 |
. . . . . . . . 9
β’ (((π = π β§ π‘ = π) β§ π€ = (Scalarβπ )) β (Scalarβπ‘) = πΏ) |
9 | | simpr 486 |
. . . . . . . . . . 11
β’ (((π = π β§ π‘ = π) β§ π€ = (Scalarβπ )) β π€ = (Scalarβπ )) |
10 | | simpll 766 |
. . . . . . . . . . . 12
β’ (((π = π β§ π‘ = π) β§ π€ = (Scalarβπ )) β π = π) |
11 | 10 | fveq2d 6847 |
. . . . . . . . . . 11
β’ (((π = π β§ π‘ = π) β§ π€ = (Scalarβπ )) β (Scalarβπ ) = (Scalarβπ)) |
12 | 9, 11 | eqtrd 2773 |
. . . . . . . . . 10
β’ (((π = π β§ π‘ = π) β§ π€ = (Scalarβπ )) β π€ = (Scalarβπ)) |
13 | | islmhm.k |
. . . . . . . . . 10
β’ πΎ = (Scalarβπ) |
14 | 12, 13 | eqtr4di 2791 |
. . . . . . . . 9
β’ (((π = π β§ π‘ = π) β§ π€ = (Scalarβπ )) β π€ = πΎ) |
15 | 8, 14 | eqeq12d 2749 |
. . . . . . . 8
β’ (((π = π β§ π‘ = π) β§ π€ = (Scalarβπ )) β ((Scalarβπ‘) = π€ β πΏ = πΎ)) |
16 | 14 | fveq2d 6847 |
. . . . . . . . . 10
β’ (((π = π β§ π‘ = π) β§ π€ = (Scalarβπ )) β (Baseβπ€) = (BaseβπΎ)) |
17 | | islmhm.b |
. . . . . . . . . 10
β’ π΅ = (BaseβπΎ) |
18 | 16, 17 | eqtr4di 2791 |
. . . . . . . . 9
β’ (((π = π β§ π‘ = π) β§ π€ = (Scalarβπ )) β (Baseβπ€) = π΅) |
19 | 10 | fveq2d 6847 |
. . . . . . . . . . 11
β’ (((π = π β§ π‘ = π) β§ π€ = (Scalarβπ )) β (Baseβπ ) = (Baseβπ)) |
20 | | islmhm.e |
. . . . . . . . . . 11
β’ πΈ = (Baseβπ) |
21 | 19, 20 | eqtr4di 2791 |
. . . . . . . . . 10
β’ (((π = π β§ π‘ = π) β§ π€ = (Scalarβπ )) β (Baseβπ ) = πΈ) |
22 | 10 | fveq2d 6847 |
. . . . . . . . . . . . . 14
β’ (((π = π β§ π‘ = π) β§ π€ = (Scalarβπ )) β (
Β·π βπ ) = ( Β·π
βπ)) |
23 | | islmhm.m |
. . . . . . . . . . . . . 14
β’ Β· = (
Β·π βπ) |
24 | 22, 23 | eqtr4di 2791 |
. . . . . . . . . . . . 13
β’ (((π = π β§ π‘ = π) β§ π€ = (Scalarβπ )) β (
Β·π βπ ) = Β· ) |
25 | 24 | oveqd 7375 |
. . . . . . . . . . . 12
β’ (((π = π β§ π‘ = π) β§ π€ = (Scalarβπ )) β (π₯( Β·π
βπ )π¦) = (π₯ Β· π¦)) |
26 | 25 | fveq2d 6847 |
. . . . . . . . . . 11
β’ (((π = π β§ π‘ = π) β§ π€ = (Scalarβπ )) β (πβ(π₯( Β·π
βπ )π¦)) = (πβ(π₯ Β· π¦))) |
27 | 5 | fveq2d 6847 |
. . . . . . . . . . . . 13
β’ (((π = π β§ π‘ = π) β§ π€ = (Scalarβπ )) β (
Β·π βπ‘) = ( Β·π
βπ)) |
28 | | islmhm.n |
. . . . . . . . . . . . 13
β’ Γ = (
Β·π βπ) |
29 | 27, 28 | eqtr4di 2791 |
. . . . . . . . . . . 12
β’ (((π = π β§ π‘ = π) β§ π€ = (Scalarβπ )) β (
Β·π βπ‘) = Γ ) |
30 | 29 | oveqd 7375 |
. . . . . . . . . . 11
β’ (((π = π β§ π‘ = π) β§ π€ = (Scalarβπ )) β (π₯( Β·π
βπ‘)(πβπ¦)) = (π₯ Γ (πβπ¦))) |
31 | 26, 30 | eqeq12d 2749 |
. . . . . . . . . 10
β’ (((π = π β§ π‘ = π) β§ π€ = (Scalarβπ )) β ((πβ(π₯( Β·π
βπ )π¦)) = (π₯( Β·π
βπ‘)(πβπ¦)) β (πβ(π₯ Β· π¦)) = (π₯ Γ (πβπ¦)))) |
32 | 21, 31 | raleqbidv 3318 |
. . . . . . . . 9
β’ (((π = π β§ π‘ = π) β§ π€ = (Scalarβπ )) β (βπ¦ β (Baseβπ )(πβ(π₯( Β·π
βπ )π¦)) = (π₯( Β·π
βπ‘)(πβπ¦)) β βπ¦ β πΈ (πβ(π₯ Β· π¦)) = (π₯ Γ (πβπ¦)))) |
33 | 18, 32 | raleqbidv 3318 |
. . . . . . . 8
β’ (((π = π β§ π‘ = π) β§ π€ = (Scalarβπ )) β (βπ₯ β (Baseβπ€)βπ¦ β (Baseβπ )(πβ(π₯( Β·π
βπ )π¦)) = (π₯( Β·π
βπ‘)(πβπ¦)) β βπ₯ β π΅ βπ¦ β πΈ (πβ(π₯ Β· π¦)) = (π₯ Γ (πβπ¦)))) |
34 | 15, 33 | anbi12d 632 |
. . . . . . 7
β’ (((π = π β§ π‘ = π) β§ π€ = (Scalarβπ )) β (((Scalarβπ‘) = π€ β§ βπ₯ β (Baseβπ€)βπ¦ β (Baseβπ )(πβ(π₯( Β·π
βπ )π¦)) = (π₯( Β·π
βπ‘)(πβπ¦))) β (πΏ = πΎ β§ βπ₯ β π΅ βπ¦ β πΈ (πβ(π₯ Β· π¦)) = (π₯ Γ (πβπ¦))))) |
35 | 4, 34 | sbcied 3785 |
. . . . . 6
β’ ((π = π β§ π‘ = π) β ([(Scalarβπ ) / π€]((Scalarβπ‘) = π€ β§ βπ₯ β (Baseβπ€)βπ¦ β (Baseβπ )(πβ(π₯( Β·π
βπ )π¦)) = (π₯( Β·π
βπ‘)(πβπ¦))) β (πΏ = πΎ β§ βπ₯ β π΅ βπ¦ β πΈ (πβ(π₯ Β· π¦)) = (π₯ Γ (πβπ¦))))) |
36 | 3, 35 | rabeqbidv 3423 |
. . . . 5
β’ ((π = π β§ π‘ = π) β {π β (π GrpHom π‘) β£ [(Scalarβπ ) / π€]((Scalarβπ‘) = π€ β§ βπ₯ β (Baseβπ€)βπ¦ β (Baseβπ )(πβ(π₯( Β·π
βπ )π¦)) = (π₯( Β·π
βπ‘)(πβπ¦)))} = {π β (π GrpHom π) β£ (πΏ = πΎ β§ βπ₯ β π΅ βπ¦ β πΈ (πβ(π₯ Β· π¦)) = (π₯ Γ (πβπ¦)))}) |
37 | | ovex 7391 |
. . . . . 6
β’ (π GrpHom π) β V |
38 | 37 | rabex 5290 |
. . . . 5
β’ {π β (π GrpHom π) β£ (πΏ = πΎ β§ βπ₯ β π΅ βπ¦ β πΈ (πβ(π₯ Β· π¦)) = (π₯ Γ (πβπ¦)))} β V |
39 | 36, 1, 38 | ovmpoa 7511 |
. . . 4
β’ ((π β LMod β§ π β LMod) β (π LMHom π) = {π β (π GrpHom π) β£ (πΏ = πΎ β§ βπ₯ β π΅ βπ¦ β πΈ (πβ(π₯ Β· π¦)) = (π₯ Γ (πβπ¦)))}) |
40 | 39 | eleq2d 2820 |
. . 3
β’ ((π β LMod β§ π β LMod) β (πΉ β (π LMHom π) β πΉ β {π β (π GrpHom π) β£ (πΏ = πΎ β§ βπ₯ β π΅ βπ¦ β πΈ (πβ(π₯ Β· π¦)) = (π₯ Γ (πβπ¦)))})) |
41 | | fveq1 6842 |
. . . . . . . 8
β’ (π = πΉ β (πβ(π₯ Β· π¦)) = (πΉβ(π₯ Β· π¦))) |
42 | | fveq1 6842 |
. . . . . . . . 9
β’ (π = πΉ β (πβπ¦) = (πΉβπ¦)) |
43 | 42 | oveq2d 7374 |
. . . . . . . 8
β’ (π = πΉ β (π₯ Γ (πβπ¦)) = (π₯ Γ (πΉβπ¦))) |
44 | 41, 43 | eqeq12d 2749 |
. . . . . . 7
β’ (π = πΉ β ((πβ(π₯ Β· π¦)) = (π₯ Γ (πβπ¦)) β (πΉβ(π₯ Β· π¦)) = (π₯ Γ (πΉβπ¦)))) |
45 | 44 | 2ralbidv 3209 |
. . . . . 6
β’ (π = πΉ β (βπ₯ β π΅ βπ¦ β πΈ (πβ(π₯ Β· π¦)) = (π₯ Γ (πβπ¦)) β βπ₯ β π΅ βπ¦ β πΈ (πΉβ(π₯ Β· π¦)) = (π₯ Γ (πΉβπ¦)))) |
46 | 45 | anbi2d 630 |
. . . . 5
β’ (π = πΉ β ((πΏ = πΎ β§ βπ₯ β π΅ βπ¦ β πΈ (πβ(π₯ Β· π¦)) = (π₯ Γ (πβπ¦))) β (πΏ = πΎ β§ βπ₯ β π΅ βπ¦ β πΈ (πΉβ(π₯ Β· π¦)) = (π₯ Γ (πΉβπ¦))))) |
47 | 46 | elrab 3646 |
. . . 4
β’ (πΉ β {π β (π GrpHom π) β£ (πΏ = πΎ β§ βπ₯ β π΅ βπ¦ β πΈ (πβ(π₯ Β· π¦)) = (π₯ Γ (πβπ¦)))} β (πΉ β (π GrpHom π) β§ (πΏ = πΎ β§ βπ₯ β π΅ βπ¦ β πΈ (πΉβ(π₯ Β· π¦)) = (π₯ Γ (πΉβπ¦))))) |
48 | | 3anass 1096 |
. . . 4
β’ ((πΉ β (π GrpHom π) β§ πΏ = πΎ β§ βπ₯ β π΅ βπ¦ β πΈ (πΉβ(π₯ Β· π¦)) = (π₯ Γ (πΉβπ¦))) β (πΉ β (π GrpHom π) β§ (πΏ = πΎ β§ βπ₯ β π΅ βπ¦ β πΈ (πΉβ(π₯ Β· π¦)) = (π₯ Γ (πΉβπ¦))))) |
49 | 47, 48 | bitr4i 278 |
. . 3
β’ (πΉ β {π β (π GrpHom π) β£ (πΏ = πΎ β§ βπ₯ β π΅ βπ¦ β πΈ (πβ(π₯ Β· π¦)) = (π₯ Γ (πβπ¦)))} β (πΉ β (π GrpHom π) β§ πΏ = πΎ β§ βπ₯ β π΅ βπ¦ β πΈ (πΉβ(π₯ Β· π¦)) = (π₯ Γ (πΉβπ¦)))) |
50 | 40, 49 | bitrdi 287 |
. 2
β’ ((π β LMod β§ π β LMod) β (πΉ β (π LMHom π) β (πΉ β (π GrpHom π) β§ πΏ = πΎ β§ βπ₯ β π΅ βπ¦ β πΈ (πΉβ(π₯ Β· π¦)) = (π₯ Γ (πΉβπ¦))))) |
51 | 2, 50 | biadanii 821 |
1
β’ (πΉ β (π LMHom π) β ((π β LMod β§ π β LMod) β§ (πΉ β (π GrpHom π) β§ πΏ = πΎ β§ βπ₯ β π΅ βπ¦ β πΈ (πΉβ(π₯ Β· π¦)) = (π₯ Γ (πΉβπ¦))))) |