Step | Hyp | Ref
| Expression |
1 | | lmhmpropd.a |
. . . . . 6
β’ (π β π΅ = (Baseβπ½)) |
2 | | lmhmpropd.c |
. . . . . 6
β’ (π β π΅ = (BaseβπΏ)) |
3 | | lmhmpropd.e |
. . . . . 6
β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(+gβπ½)π¦) = (π₯(+gβπΏ)π¦)) |
4 | | lmhmpropd.1 |
. . . . . 6
β’ (π β πΉ = (Scalarβπ½)) |
5 | | lmhmpropd.3 |
. . . . . 6
β’ (π β πΉ = (ScalarβπΏ)) |
6 | | lmhmpropd.p |
. . . . . 6
β’ π = (BaseβπΉ) |
7 | | lmhmpropd.g |
. . . . . 6
β’ ((π β§ (π₯ β π β§ π¦ β π΅)) β (π₯( Β·π
βπ½)π¦) = (π₯( Β·π
βπΏ)π¦)) |
8 | 1, 2, 3, 4, 5, 6, 7 | lmodpropd 20400 |
. . . . 5
β’ (π β (π½ β LMod β πΏ β LMod)) |
9 | | lmhmpropd.b |
. . . . . 6
β’ (π β πΆ = (BaseβπΎ)) |
10 | | lmhmpropd.d |
. . . . . 6
β’ (π β πΆ = (Baseβπ)) |
11 | | lmhmpropd.f |
. . . . . 6
β’ ((π β§ (π₯ β πΆ β§ π¦ β πΆ)) β (π₯(+gβπΎ)π¦) = (π₯(+gβπ)π¦)) |
12 | | lmhmpropd.2 |
. . . . . 6
β’ (π β πΊ = (ScalarβπΎ)) |
13 | | lmhmpropd.4 |
. . . . . 6
β’ (π β πΊ = (Scalarβπ)) |
14 | | lmhmpropd.q |
. . . . . 6
β’ π = (BaseβπΊ) |
15 | | lmhmpropd.h |
. . . . . 6
β’ ((π β§ (π₯ β π β§ π¦ β πΆ)) β (π₯( Β·π
βπΎ)π¦) = (π₯( Β·π
βπ)π¦)) |
16 | 9, 10, 11, 12, 13, 14, 15 | lmodpropd 20400 |
. . . . 5
β’ (π β (πΎ β LMod β π β LMod)) |
17 | 8, 16 | anbi12d 632 |
. . . 4
β’ (π β ((π½ β LMod β§ πΎ β LMod) β (πΏ β LMod β§ π β LMod))) |
18 | 7 | oveqrspc2v 7385 |
. . . . . . . . . . 11
β’ ((π β§ (π§ β π β§ π€ β π΅)) β (π§( Β·π
βπ½)π€) = (π§( Β·π
βπΏ)π€)) |
19 | 18 | adantlr 714 |
. . . . . . . . . 10
β’ (((π β§ (π β (π½ GrpHom πΎ) β§ πΊ = πΉ)) β§ (π§ β π β§ π€ β π΅)) β (π§( Β·π
βπ½)π€) = (π§( Β·π
βπΏ)π€)) |
20 | 19 | fveq2d 6847 |
. . . . . . . . 9
β’ (((π β§ (π β (π½ GrpHom πΎ) β§ πΊ = πΉ)) β§ (π§ β π β§ π€ β π΅)) β (πβ(π§( Β·π
βπ½)π€)) = (πβ(π§( Β·π
βπΏ)π€))) |
21 | | simpll 766 |
. . . . . . . . . 10
β’ (((π β§ (π β (π½ GrpHom πΎ) β§ πΊ = πΉ)) β§ (π§ β π β§ π€ β π΅)) β π) |
22 | | simprl 770 |
. . . . . . . . . . 11
β’ (((π β§ (π β (π½ GrpHom πΎ) β§ πΊ = πΉ)) β§ (π§ β π β§ π€ β π΅)) β π§ β π) |
23 | | simplrr 777 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β (π½ GrpHom πΎ) β§ πΊ = πΉ)) β§ (π§ β π β§ π€ β π΅)) β πΊ = πΉ) |
24 | 23 | fveq2d 6847 |
. . . . . . . . . . . 12
β’ (((π β§ (π β (π½ GrpHom πΎ) β§ πΊ = πΉ)) β§ (π§ β π β§ π€ β π΅)) β (BaseβπΊ) = (BaseβπΉ)) |
25 | 24, 14, 6 | 3eqtr4g 2798 |
. . . . . . . . . . 11
β’ (((π β§ (π β (π½ GrpHom πΎ) β§ πΊ = πΉ)) β§ (π§ β π β§ π€ β π΅)) β π = π) |
26 | 22, 25 | eleqtrrd 2837 |
. . . . . . . . . 10
β’ (((π β§ (π β (π½ GrpHom πΎ) β§ πΊ = πΉ)) β§ (π§ β π β§ π€ β π΅)) β π§ β π) |
27 | | simplrl 776 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β (π½ GrpHom πΎ) β§ πΊ = πΉ)) β§ (π§ β π β§ π€ β π΅)) β π β (π½ GrpHom πΎ)) |
28 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
(Baseβπ½) =
(Baseβπ½) |
29 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
(BaseβπΎ) =
(BaseβπΎ) |
30 | 28, 29 | ghmf 19017 |
. . . . . . . . . . . . 13
β’ (π β (π½ GrpHom πΎ) β π:(Baseβπ½)βΆ(BaseβπΎ)) |
31 | 27, 30 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β§ (π β (π½ GrpHom πΎ) β§ πΊ = πΉ)) β§ (π§ β π β§ π€ β π΅)) β π:(Baseβπ½)βΆ(BaseβπΎ)) |
32 | | simprr 772 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β (π½ GrpHom πΎ) β§ πΊ = πΉ)) β§ (π§ β π β§ π€ β π΅)) β π€ β π΅) |
33 | 21, 1 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π β§ (π β (π½ GrpHom πΎ) β§ πΊ = πΉ)) β§ (π§ β π β§ π€ β π΅)) β π΅ = (Baseβπ½)) |
34 | 32, 33 | eleqtrd 2836 |
. . . . . . . . . . . 12
β’ (((π β§ (π β (π½ GrpHom πΎ) β§ πΊ = πΉ)) β§ (π§ β π β§ π€ β π΅)) β π€ β (Baseβπ½)) |
35 | 31, 34 | ffvelcdmd 7037 |
. . . . . . . . . . 11
β’ (((π β§ (π β (π½ GrpHom πΎ) β§ πΊ = πΉ)) β§ (π§ β π β§ π€ β π΅)) β (πβπ€) β (BaseβπΎ)) |
36 | 21, 9 | syl 17 |
. . . . . . . . . . 11
β’ (((π β§ (π β (π½ GrpHom πΎ) β§ πΊ = πΉ)) β§ (π§ β π β§ π€ β π΅)) β πΆ = (BaseβπΎ)) |
37 | 35, 36 | eleqtrrd 2837 |
. . . . . . . . . 10
β’ (((π β§ (π β (π½ GrpHom πΎ) β§ πΊ = πΉ)) β§ (π§ β π β§ π€ β π΅)) β (πβπ€) β πΆ) |
38 | 15 | oveqrspc2v 7385 |
. . . . . . . . . 10
β’ ((π β§ (π§ β π β§ (πβπ€) β πΆ)) β (π§( Β·π
βπΎ)(πβπ€)) = (π§( Β·π
βπ)(πβπ€))) |
39 | 21, 26, 37, 38 | syl12anc 836 |
. . . . . . . . 9
β’ (((π β§ (π β (π½ GrpHom πΎ) β§ πΊ = πΉ)) β§ (π§ β π β§ π€ β π΅)) β (π§( Β·π
βπΎ)(πβπ€)) = (π§( Β·π
βπ)(πβπ€))) |
40 | 20, 39 | eqeq12d 2749 |
. . . . . . . 8
β’ (((π β§ (π β (π½ GrpHom πΎ) β§ πΊ = πΉ)) β§ (π§ β π β§ π€ β π΅)) β ((πβ(π§( Β·π
βπ½)π€)) = (π§( Β·π
βπΎ)(πβπ€)) β (πβ(π§( Β·π
βπΏ)π€)) = (π§( Β·π
βπ)(πβπ€)))) |
41 | 40 | 2ralbidva 3207 |
. . . . . . 7
β’ ((π β§ (π β (π½ GrpHom πΎ) β§ πΊ = πΉ)) β (βπ§ β π βπ€ β π΅ (πβ(π§( Β·π
βπ½)π€)) = (π§( Β·π
βπΎ)(πβπ€)) β βπ§ β π βπ€ β π΅ (πβ(π§( Β·π
βπΏ)π€)) = (π§( Β·π
βπ)(πβπ€)))) |
42 | 41 | pm5.32da 580 |
. . . . . 6
β’ (π β (((π β (π½ GrpHom πΎ) β§ πΊ = πΉ) β§ βπ§ β π βπ€ β π΅ (πβ(π§( Β·π
βπ½)π€)) = (π§( Β·π
βπΎ)(πβπ€))) β ((π β (π½ GrpHom πΎ) β§ πΊ = πΉ) β§ βπ§ β π βπ€ β π΅ (πβ(π§( Β·π
βπΏ)π€)) = (π§( Β·π
βπ)(πβπ€))))) |
43 | | df-3an 1090 |
. . . . . 6
β’ ((π β (π½ GrpHom πΎ) β§ πΊ = πΉ β§ βπ§ β π βπ€ β π΅ (πβ(π§( Β·π
βπ½)π€)) = (π§( Β·π
βπΎ)(πβπ€))) β ((π β (π½ GrpHom πΎ) β§ πΊ = πΉ) β§ βπ§ β π βπ€ β π΅ (πβ(π§( Β·π
βπ½)π€)) = (π§( Β·π
βπΎ)(πβπ€)))) |
44 | | df-3an 1090 |
. . . . . 6
β’ ((π β (π½ GrpHom πΎ) β§ πΊ = πΉ β§ βπ§ β π βπ€ β π΅ (πβ(π§( Β·π
βπΏ)π€)) = (π§( Β·π
βπ)(πβπ€))) β ((π β (π½ GrpHom πΎ) β§ πΊ = πΉ) β§ βπ§ β π βπ€ β π΅ (πβ(π§( Β·π
βπΏ)π€)) = (π§( Β·π
βπ)(πβπ€)))) |
45 | 42, 43, 44 | 3bitr4g 314 |
. . . . 5
β’ (π β ((π β (π½ GrpHom πΎ) β§ πΊ = πΉ β§ βπ§ β π βπ€ β π΅ (πβ(π§( Β·π
βπ½)π€)) = (π§( Β·π
βπΎ)(πβπ€))) β (π β (π½ GrpHom πΎ) β§ πΊ = πΉ β§ βπ§ β π βπ€ β π΅ (πβ(π§( Β·π
βπΏ)π€)) = (π§( Β·π
βπ)(πβπ€))))) |
46 | 12, 4 | eqeq12d 2749 |
. . . . . 6
β’ (π β (πΊ = πΉ β (ScalarβπΎ) = (Scalarβπ½))) |
47 | 4 | fveq2d 6847 |
. . . . . . . 8
β’ (π β (BaseβπΉ) =
(Baseβ(Scalarβπ½))) |
48 | 6, 47 | eqtrid 2785 |
. . . . . . 7
β’ (π β π = (Baseβ(Scalarβπ½))) |
49 | 1 | raleqdv 3312 |
. . . . . . 7
β’ (π β (βπ€ β π΅ (πβ(π§( Β·π
βπ½)π€)) = (π§( Β·π
βπΎ)(πβπ€)) β βπ€ β (Baseβπ½)(πβ(π§( Β·π
βπ½)π€)) = (π§( Β·π
βπΎ)(πβπ€)))) |
50 | 48, 49 | raleqbidv 3318 |
. . . . . 6
β’ (π β (βπ§ β π βπ€ β π΅ (πβ(π§( Β·π
βπ½)π€)) = (π§( Β·π
βπΎ)(πβπ€)) β βπ§ β (Baseβ(Scalarβπ½))βπ€ β (Baseβπ½)(πβ(π§( Β·π
βπ½)π€)) = (π§( Β·π
βπΎ)(πβπ€)))) |
51 | 46, 50 | 3anbi23d 1440 |
. . . . 5
β’ (π β ((π β (π½ GrpHom πΎ) β§ πΊ = πΉ β§ βπ§ β π βπ€ β π΅ (πβ(π§( Β·π
βπ½)π€)) = (π§( Β·π
βπΎ)(πβπ€))) β (π β (π½ GrpHom πΎ) β§ (ScalarβπΎ) = (Scalarβπ½) β§ βπ§ β (Baseβ(Scalarβπ½))βπ€ β (Baseβπ½)(πβ(π§( Β·π
βπ½)π€)) = (π§( Β·π
βπΎ)(πβπ€))))) |
52 | 1, 9, 2, 10, 3, 11 | ghmpropd 19051 |
. . . . . . 7
β’ (π β (π½ GrpHom πΎ) = (πΏ GrpHom π)) |
53 | 52 | eleq2d 2820 |
. . . . . 6
β’ (π β (π β (π½ GrpHom πΎ) β π β (πΏ GrpHom π))) |
54 | 13, 5 | eqeq12d 2749 |
. . . . . 6
β’ (π β (πΊ = πΉ β (Scalarβπ) = (ScalarβπΏ))) |
55 | 5 | fveq2d 6847 |
. . . . . . . 8
β’ (π β (BaseβπΉ) =
(Baseβ(ScalarβπΏ))) |
56 | 6, 55 | eqtrid 2785 |
. . . . . . 7
β’ (π β π = (Baseβ(ScalarβπΏ))) |
57 | 2 | raleqdv 3312 |
. . . . . . 7
β’ (π β (βπ€ β π΅ (πβ(π§( Β·π
βπΏ)π€)) = (π§( Β·π
βπ)(πβπ€)) β βπ€ β (BaseβπΏ)(πβ(π§( Β·π
βπΏ)π€)) = (π§( Β·π
βπ)(πβπ€)))) |
58 | 56, 57 | raleqbidv 3318 |
. . . . . 6
β’ (π β (βπ§ β π βπ€ β π΅ (πβ(π§( Β·π
βπΏ)π€)) = (π§( Β·π
βπ)(πβπ€)) β βπ§ β (Baseβ(ScalarβπΏ))βπ€ β (BaseβπΏ)(πβ(π§( Β·π
βπΏ)π€)) = (π§( Β·π
βπ)(πβπ€)))) |
59 | 53, 54, 58 | 3anbi123d 1437 |
. . . . 5
β’ (π β ((π β (π½ GrpHom πΎ) β§ πΊ = πΉ β§ βπ§ β π βπ€ β π΅ (πβ(π§( Β·π
βπΏ)π€)) = (π§( Β·π
βπ)(πβπ€))) β (π β (πΏ GrpHom π) β§ (Scalarβπ) = (ScalarβπΏ) β§ βπ§ β (Baseβ(ScalarβπΏ))βπ€ β (BaseβπΏ)(πβ(π§( Β·π
βπΏ)π€)) = (π§( Β·π
βπ)(πβπ€))))) |
60 | 45, 51, 59 | 3bitr3d 309 |
. . . 4
β’ (π β ((π β (π½ GrpHom πΎ) β§ (ScalarβπΎ) = (Scalarβπ½) β§ βπ§ β (Baseβ(Scalarβπ½))βπ€ β (Baseβπ½)(πβ(π§( Β·π
βπ½)π€)) = (π§( Β·π
βπΎ)(πβπ€))) β (π β (πΏ GrpHom π) β§ (Scalarβπ) = (ScalarβπΏ) β§ βπ§ β (Baseβ(ScalarβπΏ))βπ€ β (BaseβπΏ)(πβ(π§( Β·π
βπΏ)π€)) = (π§( Β·π
βπ)(πβπ€))))) |
61 | 17, 60 | anbi12d 632 |
. . 3
β’ (π β (((π½ β LMod β§ πΎ β LMod) β§ (π β (π½ GrpHom πΎ) β§ (ScalarβπΎ) = (Scalarβπ½) β§ βπ§ β (Baseβ(Scalarβπ½))βπ€ β (Baseβπ½)(πβ(π§( Β·π
βπ½)π€)) = (π§( Β·π
βπΎ)(πβπ€)))) β ((πΏ β LMod β§ π β LMod) β§ (π β (πΏ GrpHom π) β§ (Scalarβπ) = (ScalarβπΏ) β§ βπ§ β (Baseβ(ScalarβπΏ))βπ€ β (BaseβπΏ)(πβ(π§( Β·π
βπΏ)π€)) = (π§( Β·π
βπ)(πβπ€)))))) |
62 | | eqid 2733 |
. . . 4
β’
(Scalarβπ½) =
(Scalarβπ½) |
63 | | eqid 2733 |
. . . 4
β’
(ScalarβπΎ) =
(ScalarβπΎ) |
64 | | eqid 2733 |
. . . 4
β’
(Baseβ(Scalarβπ½)) = (Baseβ(Scalarβπ½)) |
65 | | eqid 2733 |
. . . 4
β’ (
Β·π βπ½) = ( Β·π
βπ½) |
66 | | eqid 2733 |
. . . 4
β’ (
Β·π βπΎ) = ( Β·π
βπΎ) |
67 | 62, 63, 64, 28, 65, 66 | islmhm 20503 |
. . 3
β’ (π β (π½ LMHom πΎ) β ((π½ β LMod β§ πΎ β LMod) β§ (π β (π½ GrpHom πΎ) β§ (ScalarβπΎ) = (Scalarβπ½) β§ βπ§ β (Baseβ(Scalarβπ½))βπ€ β (Baseβπ½)(πβ(π§( Β·π
βπ½)π€)) = (π§( Β·π
βπΎ)(πβπ€))))) |
68 | | eqid 2733 |
. . . 4
β’
(ScalarβπΏ) =
(ScalarβπΏ) |
69 | | eqid 2733 |
. . . 4
β’
(Scalarβπ) =
(Scalarβπ) |
70 | | eqid 2733 |
. . . 4
β’
(Baseβ(ScalarβπΏ)) = (Baseβ(ScalarβπΏ)) |
71 | | eqid 2733 |
. . . 4
β’
(BaseβπΏ) =
(BaseβπΏ) |
72 | | eqid 2733 |
. . . 4
β’ (
Β·π βπΏ) = ( Β·π
βπΏ) |
73 | | eqid 2733 |
. . . 4
β’ (
Β·π βπ) = ( Β·π
βπ) |
74 | 68, 69, 70, 71, 72, 73 | islmhm 20503 |
. . 3
β’ (π β (πΏ LMHom π) β ((πΏ β LMod β§ π β LMod) β§ (π β (πΏ GrpHom π) β§ (Scalarβπ) = (ScalarβπΏ) β§ βπ§ β (Baseβ(ScalarβπΏ))βπ€ β (BaseβπΏ)(πβ(π§( Β·π
βπΏ)π€)) = (π§( Β·π
βπ)(πβπ€))))) |
75 | 61, 67, 74 | 3bitr4g 314 |
. 2
β’ (π β (π β (π½ LMHom πΎ) β π β (πΏ LMHom π))) |
76 | 75 | eqrdv 2731 |
1
β’ (π β (π½ LMHom πΎ) = (πΏ LMHom π)) |