Step | Hyp | Ref
| Expression |
1 | | lmhmf1o.y |
. . 3
β’ π = (Baseβπ) |
2 | | eqid 2733 |
. . 3
β’ (
Β·π βπ) = ( Β·π
βπ) |
3 | | eqid 2733 |
. . 3
β’ (
Β·π βπ) = ( Β·π
βπ) |
4 | | eqid 2733 |
. . 3
β’
(Scalarβπ) =
(Scalarβπ) |
5 | | eqid 2733 |
. . 3
β’
(Scalarβπ) =
(Scalarβπ) |
6 | | eqid 2733 |
. . 3
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
7 | | lmhmlmod2 20508 |
. . . 4
β’ (πΉ β (π LMHom π) β π β LMod) |
8 | 7 | adantr 482 |
. . 3
β’ ((πΉ β (π LMHom π) β§ πΉ:πβ1-1-ontoβπ) β π β LMod) |
9 | | lmhmlmod1 20509 |
. . . 4
β’ (πΉ β (π LMHom π) β π β LMod) |
10 | 9 | adantr 482 |
. . 3
β’ ((πΉ β (π LMHom π) β§ πΉ:πβ1-1-ontoβπ) β π β LMod) |
11 | 5, 4 | lmhmsca 20506 |
. . . . 5
β’ (πΉ β (π LMHom π) β (Scalarβπ) = (Scalarβπ)) |
12 | 11 | eqcomd 2739 |
. . . 4
β’ (πΉ β (π LMHom π) β (Scalarβπ) = (Scalarβπ)) |
13 | 12 | adantr 482 |
. . 3
β’ ((πΉ β (π LMHom π) β§ πΉ:πβ1-1-ontoβπ) β (Scalarβπ) = (Scalarβπ)) |
14 | | lmghm 20507 |
. . . . 5
β’ (πΉ β (π LMHom π) β πΉ β (π GrpHom π)) |
15 | | lmhmf1o.x |
. . . . . 6
β’ π = (Baseβπ) |
16 | 15, 1 | ghmf1o 19043 |
. . . . 5
β’ (πΉ β (π GrpHom π) β (πΉ:πβ1-1-ontoβπ β β‘πΉ β (π GrpHom π))) |
17 | 14, 16 | syl 17 |
. . . 4
β’ (πΉ β (π LMHom π) β (πΉ:πβ1-1-ontoβπ β β‘πΉ β (π GrpHom π))) |
18 | 17 | biimpa 478 |
. . 3
β’ ((πΉ β (π LMHom π) β§ πΉ:πβ1-1-ontoβπ) β β‘πΉ β (π GrpHom π)) |
19 | | simpll 766 |
. . . . . 6
β’ (((πΉ β (π LMHom π) β§ πΉ:πβ1-1-ontoβπ) β§ (π β (Baseβ(Scalarβπ)) β§ π β π)) β πΉ β (π LMHom π)) |
20 | 13 | fveq2d 6847 |
. . . . . . . . 9
β’ ((πΉ β (π LMHom π) β§ πΉ:πβ1-1-ontoβπ) β
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ))) |
21 | 20 | eleq2d 2820 |
. . . . . . . 8
β’ ((πΉ β (π LMHom π) β§ πΉ:πβ1-1-ontoβπ) β (π β (Baseβ(Scalarβπ)) β π β (Baseβ(Scalarβπ)))) |
22 | 21 | biimpar 479 |
. . . . . . 7
β’ (((πΉ β (π LMHom π) β§ πΉ:πβ1-1-ontoβπ) β§ π β (Baseβ(Scalarβπ))) β π β (Baseβ(Scalarβπ))) |
23 | 22 | adantrr 716 |
. . . . . 6
β’ (((πΉ β (π LMHom π) β§ πΉ:πβ1-1-ontoβπ) β§ (π β (Baseβ(Scalarβπ)) β§ π β π)) β π β (Baseβ(Scalarβπ))) |
24 | | f1ocnv 6797 |
. . . . . . . . . 10
β’ (πΉ:πβ1-1-ontoβπ β β‘πΉ:πβ1-1-ontoβπ) |
25 | | f1of 6785 |
. . . . . . . . . 10
β’ (β‘πΉ:πβ1-1-ontoβπ β β‘πΉ:πβΆπ) |
26 | 24, 25 | syl 17 |
. . . . . . . . 9
β’ (πΉ:πβ1-1-ontoβπ β β‘πΉ:πβΆπ) |
27 | 26 | adantl 483 |
. . . . . . . 8
β’ ((πΉ β (π LMHom π) β§ πΉ:πβ1-1-ontoβπ) β β‘πΉ:πβΆπ) |
28 | 27 | ffvelcdmda 7036 |
. . . . . . 7
β’ (((πΉ β (π LMHom π) β§ πΉ:πβ1-1-ontoβπ) β§ π β π) β (β‘πΉβπ) β π) |
29 | 28 | adantrl 715 |
. . . . . 6
β’ (((πΉ β (π LMHom π) β§ πΉ:πβ1-1-ontoβπ) β§ (π β (Baseβ(Scalarβπ)) β§ π β π)) β (β‘πΉβπ) β π) |
30 | | eqid 2733 |
. . . . . . 7
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
31 | 5, 30, 15, 3, 2 | lmhmlin 20511 |
. . . . . 6
β’ ((πΉ β (π LMHom π) β§ π β (Baseβ(Scalarβπ)) β§ (β‘πΉβπ) β π) β (πΉβ(π( Β·π
βπ)(β‘πΉβπ))) = (π( Β·π
βπ)(πΉβ(β‘πΉβπ)))) |
32 | 19, 23, 29, 31 | syl3anc 1372 |
. . . . 5
β’ (((πΉ β (π LMHom π) β§ πΉ:πβ1-1-ontoβπ) β§ (π β (Baseβ(Scalarβπ)) β§ π β π)) β (πΉβ(π( Β·π
βπ)(β‘πΉβπ))) = (π( Β·π
βπ)(πΉβ(β‘πΉβπ)))) |
33 | | f1ocnvfv2 7224 |
. . . . . . 7
β’ ((πΉ:πβ1-1-ontoβπ β§ π β π) β (πΉβ(β‘πΉβπ)) = π) |
34 | 33 | ad2ant2l 745 |
. . . . . 6
β’ (((πΉ β (π LMHom π) β§ πΉ:πβ1-1-ontoβπ) β§ (π β (Baseβ(Scalarβπ)) β§ π β π)) β (πΉβ(β‘πΉβπ)) = π) |
35 | 34 | oveq2d 7374 |
. . . . 5
β’ (((πΉ β (π LMHom π) β§ πΉ:πβ1-1-ontoβπ) β§ (π β (Baseβ(Scalarβπ)) β§ π β π)) β (π( Β·π
βπ)(πΉβ(β‘πΉβπ))) = (π( Β·π
βπ)π)) |
36 | 32, 35 | eqtrd 2773 |
. . . 4
β’ (((πΉ β (π LMHom π) β§ πΉ:πβ1-1-ontoβπ) β§ (π β (Baseβ(Scalarβπ)) β§ π β π)) β (πΉβ(π( Β·π
βπ)(β‘πΉβπ))) = (π( Β·π
βπ)π)) |
37 | | simplr 768 |
. . . . 5
β’ (((πΉ β (π LMHom π) β§ πΉ:πβ1-1-ontoβπ) β§ (π β (Baseβ(Scalarβπ)) β§ π β π)) β πΉ:πβ1-1-ontoβπ) |
38 | 10 | adantr 482 |
. . . . . 6
β’ (((πΉ β (π LMHom π) β§ πΉ:πβ1-1-ontoβπ) β§ (π β (Baseβ(Scalarβπ)) β§ π β π)) β π β LMod) |
39 | 15, 5, 3, 30 | lmodvscl 20354 |
. . . . . 6
β’ ((π β LMod β§ π β
(Baseβ(Scalarβπ)) β§ (β‘πΉβπ) β π) β (π( Β·π
βπ)(β‘πΉβπ)) β π) |
40 | 38, 23, 29, 39 | syl3anc 1372 |
. . . . 5
β’ (((πΉ β (π LMHom π) β§ πΉ:πβ1-1-ontoβπ) β§ (π β (Baseβ(Scalarβπ)) β§ π β π)) β (π( Β·π
βπ)(β‘πΉβπ)) β π) |
41 | | f1ocnvfv 7225 |
. . . . 5
β’ ((πΉ:πβ1-1-ontoβπ β§ (π( Β·π
βπ)(β‘πΉβπ)) β π) β ((πΉβ(π( Β·π
βπ)(β‘πΉβπ))) = (π( Β·π
βπ)π) β (β‘πΉβ(π( Β·π
βπ)π)) = (π( Β·π
βπ)(β‘πΉβπ)))) |
42 | 37, 40, 41 | syl2anc 585 |
. . . 4
β’ (((πΉ β (π LMHom π) β§ πΉ:πβ1-1-ontoβπ) β§ (π β (Baseβ(Scalarβπ)) β§ π β π)) β ((πΉβ(π( Β·π
βπ)(β‘πΉβπ))) = (π( Β·π
βπ)π) β (β‘πΉβ(π( Β·π
βπ)π)) = (π( Β·π
βπ)(β‘πΉβπ)))) |
43 | 36, 42 | mpd 15 |
. . 3
β’ (((πΉ β (π LMHom π) β§ πΉ:πβ1-1-ontoβπ) β§ (π β (Baseβ(Scalarβπ)) β§ π β π)) β (β‘πΉβ(π( Β·π
βπ)π)) = (π( Β·π
βπ)(β‘πΉβπ))) |
44 | 1, 2, 3, 4, 5, 6, 8, 10, 13, 18, 43 | islmhmd 20515 |
. 2
β’ ((πΉ β (π LMHom π) β§ πΉ:πβ1-1-ontoβπ) β β‘πΉ β (π LMHom π)) |
45 | 15, 1 | lmhmf 20510 |
. . . . 5
β’ (πΉ β (π LMHom π) β πΉ:πβΆπ) |
46 | 45 | ffnd 6670 |
. . . 4
β’ (πΉ β (π LMHom π) β πΉ Fn π) |
47 | 46 | adantr 482 |
. . 3
β’ ((πΉ β (π LMHom π) β§ β‘πΉ β (π LMHom π)) β πΉ Fn π) |
48 | 1, 15 | lmhmf 20510 |
. . . . 5
β’ (β‘πΉ β (π LMHom π) β β‘πΉ:πβΆπ) |
49 | 48 | adantl 483 |
. . . 4
β’ ((πΉ β (π LMHom π) β§ β‘πΉ β (π LMHom π)) β β‘πΉ:πβΆπ) |
50 | 49 | ffnd 6670 |
. . 3
β’ ((πΉ β (π LMHom π) β§ β‘πΉ β (π LMHom π)) β β‘πΉ Fn π) |
51 | | dff1o4 6793 |
. . 3
β’ (πΉ:πβ1-1-ontoβπ β (πΉ Fn π β§ β‘πΉ Fn π)) |
52 | 47, 50, 51 | sylanbrc 584 |
. 2
β’ ((πΉ β (π LMHom π) β§ β‘πΉ β (π LMHom π)) β πΉ:πβ1-1-ontoβπ) |
53 | 44, 52 | impbida 800 |
1
β’ (πΉ β (π LMHom π) β (πΉ:πβ1-1-ontoβπ β β‘πΉ β (π LMHom π))) |