Step | Hyp | Ref
| Expression |
1 | | lmghm 20508 |
. . 3
β’ (πΉ β (π LMHom π) β πΉ β (π GrpHom π)) |
2 | | lmghm 20508 |
. . 3
β’ (πΊ β (π LMHom π) β πΊ β (π GrpHom π)) |
3 | | ghmeql 19038 |
. . 3
β’ ((πΉ β (π GrpHom π) β§ πΊ β (π GrpHom π)) β dom (πΉ β© πΊ) β (SubGrpβπ)) |
4 | 1, 2, 3 | syl2an 597 |
. 2
β’ ((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β dom (πΉ β© πΊ) β (SubGrpβπ)) |
5 | | fveq2 6847 |
. . . . . . . 8
β’ (π§ = (π₯( Β·π
βπ)π¦) β (πΉβπ§) = (πΉβ(π₯( Β·π
βπ)π¦))) |
6 | | fveq2 6847 |
. . . . . . . 8
β’ (π§ = (π₯( Β·π
βπ)π¦) β (πΊβπ§) = (πΊβ(π₯( Β·π
βπ)π¦))) |
7 | 5, 6 | eqeq12d 2753 |
. . . . . . 7
β’ (π§ = (π₯( Β·π
βπ)π¦) β ((πΉβπ§) = (πΊβπ§) β (πΉβ(π₯( Β·π
βπ)π¦)) = (πΊβ(π₯( Β·π
βπ)π¦)))) |
8 | | lmhmlmod1 20510 |
. . . . . . . . . 10
β’ (πΉ β (π LMHom π) β π β LMod) |
9 | 8 | adantr 482 |
. . . . . . . . 9
β’ ((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β π β LMod) |
10 | 9 | ad2antrr 725 |
. . . . . . . 8
β’ ((((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ π₯ β (Baseβ(Scalarβπ))) β§ (π¦ β (Baseβπ) β§ (πΉβπ¦) = (πΊβπ¦))) β π β LMod) |
11 | | simplr 768 |
. . . . . . . 8
β’ ((((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ π₯ β (Baseβ(Scalarβπ))) β§ (π¦ β (Baseβπ) β§ (πΉβπ¦) = (πΊβπ¦))) β π₯ β (Baseβ(Scalarβπ))) |
12 | | simprl 770 |
. . . . . . . 8
β’ ((((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ π₯ β (Baseβ(Scalarβπ))) β§ (π¦ β (Baseβπ) β§ (πΉβπ¦) = (πΊβπ¦))) β π¦ β (Baseβπ)) |
13 | | eqid 2737 |
. . . . . . . . 9
β’
(Baseβπ) =
(Baseβπ) |
14 | | eqid 2737 |
. . . . . . . . 9
β’
(Scalarβπ) =
(Scalarβπ) |
15 | | eqid 2737 |
. . . . . . . . 9
β’ (
Β·π βπ) = ( Β·π
βπ) |
16 | | eqid 2737 |
. . . . . . . . 9
β’
(Baseβ(Scalarβπ)) = (Baseβ(Scalarβπ)) |
17 | 13, 14, 15, 16 | lmodvscl 20355 |
. . . . . . . 8
β’ ((π β LMod β§ π₯ β
(Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ)) β (π₯( Β·π
βπ)π¦) β (Baseβπ)) |
18 | 10, 11, 12, 17 | syl3anc 1372 |
. . . . . . 7
β’ ((((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ π₯ β (Baseβ(Scalarβπ))) β§ (π¦ β (Baseβπ) β§ (πΉβπ¦) = (πΊβπ¦))) β (π₯( Β·π
βπ)π¦) β (Baseβπ)) |
19 | | oveq2 7370 |
. . . . . . . . 9
β’ ((πΉβπ¦) = (πΊβπ¦) β (π₯( Β·π
βπ)(πΉβπ¦)) = (π₯( Β·π
βπ)(πΊβπ¦))) |
20 | 19 | ad2antll 728 |
. . . . . . . 8
β’ ((((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ π₯ β (Baseβ(Scalarβπ))) β§ (π¦ β (Baseβπ) β§ (πΉβπ¦) = (πΊβπ¦))) β (π₯( Β·π
βπ)(πΉβπ¦)) = (π₯( Β·π
βπ)(πΊβπ¦))) |
21 | | simplll 774 |
. . . . . . . . 9
β’ ((((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ π₯ β (Baseβ(Scalarβπ))) β§ (π¦ β (Baseβπ) β§ (πΉβπ¦) = (πΊβπ¦))) β πΉ β (π LMHom π)) |
22 | | eqid 2737 |
. . . . . . . . . 10
β’ (
Β·π βπ) = ( Β·π
βπ) |
23 | 14, 16, 13, 15, 22 | lmhmlin 20512 |
. . . . . . . . 9
β’ ((πΉ β (π LMHom π) β§ π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ)) β (πΉβ(π₯( Β·π
βπ)π¦)) = (π₯( Β·π
βπ)(πΉβπ¦))) |
24 | 21, 11, 12, 23 | syl3anc 1372 |
. . . . . . . 8
β’ ((((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ π₯ β (Baseβ(Scalarβπ))) β§ (π¦ β (Baseβπ) β§ (πΉβπ¦) = (πΊβπ¦))) β (πΉβ(π₯( Β·π
βπ)π¦)) = (π₯( Β·π
βπ)(πΉβπ¦))) |
25 | | simpllr 775 |
. . . . . . . . 9
β’ ((((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ π₯ β (Baseβ(Scalarβπ))) β§ (π¦ β (Baseβπ) β§ (πΉβπ¦) = (πΊβπ¦))) β πΊ β (π LMHom π)) |
26 | 14, 16, 13, 15, 22 | lmhmlin 20512 |
. . . . . . . . 9
β’ ((πΊ β (π LMHom π) β§ π₯ β (Baseβ(Scalarβπ)) β§ π¦ β (Baseβπ)) β (πΊβ(π₯( Β·π
βπ)π¦)) = (π₯( Β·π
βπ)(πΊβπ¦))) |
27 | 25, 11, 12, 26 | syl3anc 1372 |
. . . . . . . 8
β’ ((((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ π₯ β (Baseβ(Scalarβπ))) β§ (π¦ β (Baseβπ) β§ (πΉβπ¦) = (πΊβπ¦))) β (πΊβ(π₯( Β·π
βπ)π¦)) = (π₯( Β·π
βπ)(πΊβπ¦))) |
28 | 20, 24, 27 | 3eqtr4d 2787 |
. . . . . . 7
β’ ((((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ π₯ β (Baseβ(Scalarβπ))) β§ (π¦ β (Baseβπ) β§ (πΉβπ¦) = (πΊβπ¦))) β (πΉβ(π₯( Β·π
βπ)π¦)) = (πΊβ(π₯( Β·π
βπ)π¦))) |
29 | 7, 18, 28 | elrabd 3652 |
. . . . . 6
β’ ((((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ π₯ β (Baseβ(Scalarβπ))) β§ (π¦ β (Baseβπ) β§ (πΉβπ¦) = (πΊβπ¦))) β (π₯( Β·π
βπ)π¦) β {π§ β (Baseβπ) β£ (πΉβπ§) = (πΊβπ§)}) |
30 | 29 | expr 458 |
. . . . 5
β’ ((((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ π₯ β (Baseβ(Scalarβπ))) β§ π¦ β (Baseβπ)) β ((πΉβπ¦) = (πΊβπ¦) β (π₯( Β·π
βπ)π¦) β {π§ β (Baseβπ) β£ (πΉβπ§) = (πΊβπ§)})) |
31 | 30 | ralrimiva 3144 |
. . . 4
β’ (((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ π₯ β (Baseβ(Scalarβπ))) β βπ¦ β (Baseβπ)((πΉβπ¦) = (πΊβπ¦) β (π₯( Β·π
βπ)π¦) β {π§ β (Baseβπ) β£ (πΉβπ§) = (πΊβπ§)})) |
32 | | eqid 2737 |
. . . . . . . . 9
β’
(Baseβπ) =
(Baseβπ) |
33 | 13, 32 | lmhmf 20511 |
. . . . . . . 8
β’ (πΉ β (π LMHom π) β πΉ:(Baseβπ)βΆ(Baseβπ)) |
34 | 33 | ffnd 6674 |
. . . . . . 7
β’ (πΉ β (π LMHom π) β πΉ Fn (Baseβπ)) |
35 | 13, 32 | lmhmf 20511 |
. . . . . . . 8
β’ (πΊ β (π LMHom π) β πΊ:(Baseβπ)βΆ(Baseβπ)) |
36 | 35 | ffnd 6674 |
. . . . . . 7
β’ (πΊ β (π LMHom π) β πΊ Fn (Baseβπ)) |
37 | | fndmin 7000 |
. . . . . . 7
β’ ((πΉ Fn (Baseβπ) β§ πΊ Fn (Baseβπ)) β dom (πΉ β© πΊ) = {π§ β (Baseβπ) β£ (πΉβπ§) = (πΊβπ§)}) |
38 | 34, 36, 37 | syl2an 597 |
. . . . . 6
β’ ((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β dom (πΉ β© πΊ) = {π§ β (Baseβπ) β£ (πΉβπ§) = (πΊβπ§)}) |
39 | 38 | adantr 482 |
. . . . 5
β’ (((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ π₯ β (Baseβ(Scalarβπ))) β dom (πΉ β© πΊ) = {π§ β (Baseβπ) β£ (πΉβπ§) = (πΊβπ§)}) |
40 | | eleq2 2827 |
. . . . . . 7
β’ (dom
(πΉ β© πΊ) = {π§ β (Baseβπ) β£ (πΉβπ§) = (πΊβπ§)} β ((π₯( Β·π
βπ)π¦) β dom (πΉ β© πΊ) β (π₯( Β·π
βπ)π¦) β {π§ β (Baseβπ) β£ (πΉβπ§) = (πΊβπ§)})) |
41 | 40 | raleqbi1dv 3310 |
. . . . . 6
β’ (dom
(πΉ β© πΊ) = {π§ β (Baseβπ) β£ (πΉβπ§) = (πΊβπ§)} β (βπ¦ β dom (πΉ β© πΊ)(π₯( Β·π
βπ)π¦) β dom (πΉ β© πΊ) β βπ¦ β {π§ β (Baseβπ) β£ (πΉβπ§) = (πΊβπ§)} (π₯( Β·π
βπ)π¦) β {π§ β (Baseβπ) β£ (πΉβπ§) = (πΊβπ§)})) |
42 | | fveq2 6847 |
. . . . . . . 8
β’ (π§ = π¦ β (πΉβπ§) = (πΉβπ¦)) |
43 | | fveq2 6847 |
. . . . . . . 8
β’ (π§ = π¦ β (πΊβπ§) = (πΊβπ¦)) |
44 | 42, 43 | eqeq12d 2753 |
. . . . . . 7
β’ (π§ = π¦ β ((πΉβπ§) = (πΊβπ§) β (πΉβπ¦) = (πΊβπ¦))) |
45 | 44 | ralrab 3656 |
. . . . . 6
β’
(βπ¦ β
{π§ β (Baseβπ) β£ (πΉβπ§) = (πΊβπ§)} (π₯( Β·π
βπ)π¦) β {π§ β (Baseβπ) β£ (πΉβπ§) = (πΊβπ§)} β βπ¦ β (Baseβπ)((πΉβπ¦) = (πΊβπ¦) β (π₯( Β·π
βπ)π¦) β {π§ β (Baseβπ) β£ (πΉβπ§) = (πΊβπ§)})) |
46 | 41, 45 | bitrdi 287 |
. . . . 5
β’ (dom
(πΉ β© πΊ) = {π§ β (Baseβπ) β£ (πΉβπ§) = (πΊβπ§)} β (βπ¦ β dom (πΉ β© πΊ)(π₯( Β·π
βπ)π¦) β dom (πΉ β© πΊ) β βπ¦ β (Baseβπ)((πΉβπ¦) = (πΊβπ¦) β (π₯( Β·π
βπ)π¦) β {π§ β (Baseβπ) β£ (πΉβπ§) = (πΊβπ§)}))) |
47 | 39, 46 | syl 17 |
. . . 4
β’ (((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ π₯ β (Baseβ(Scalarβπ))) β (βπ¦ β dom (πΉ β© πΊ)(π₯( Β·π
βπ)π¦) β dom (πΉ β© πΊ) β βπ¦ β (Baseβπ)((πΉβπ¦) = (πΊβπ¦) β (π₯( Β·π
βπ)π¦) β {π§ β (Baseβπ) β£ (πΉβπ§) = (πΊβπ§)}))) |
48 | 31, 47 | mpbird 257 |
. . 3
β’ (((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β§ π₯ β (Baseβ(Scalarβπ))) β βπ¦ β dom (πΉ β© πΊ)(π₯( Β·π
βπ)π¦) β dom (πΉ β© πΊ)) |
49 | 48 | ralrimiva 3144 |
. 2
β’ ((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β βπ₯ β (Baseβ(Scalarβπ))βπ¦ β dom (πΉ β© πΊ)(π₯( Β·π
βπ)π¦) β dom (πΉ β© πΊ)) |
50 | | lmhmeql.u |
. . . 4
β’ π = (LSubSpβπ) |
51 | 14, 16, 13, 15, 50 | islss4 20439 |
. . 3
β’ (π β LMod β (dom (πΉ β© πΊ) β π β (dom (πΉ β© πΊ) β (SubGrpβπ) β§ βπ₯ β (Baseβ(Scalarβπ))βπ¦ β dom (πΉ β© πΊ)(π₯( Β·π
βπ)π¦) β dom (πΉ β© πΊ)))) |
52 | 9, 51 | syl 17 |
. 2
β’ ((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β (dom (πΉ β© πΊ) β π β (dom (πΉ β© πΊ) β (SubGrpβπ) β§ βπ₯ β (Baseβ(Scalarβπ))βπ¦ β dom (πΉ β© πΊ)(π₯( Β·π
βπ)π¦) β dom (πΉ β© πΊ)))) |
53 | 4, 49, 52 | mpbir2and 712 |
1
β’ ((πΉ β (π LMHom π) β§ πΊ β (π LMHom π)) β dom (πΉ β© πΊ) β π) |