Step | Hyp | Ref
| Expression |
1 | | eqtr3 2758 |
. . . 4
β’ (((π βΎ π) = πΉ β§ (β βΎ π) = πΉ) β (π βΎ π) = (β βΎ π)) |
2 | | inss1 4228 |
. . . . . . . . 9
β’ (π β© β) β π |
3 | | dmss 5902 |
. . . . . . . . 9
β’ ((π β© β) β π β dom (π β© β) β dom π) |
4 | 2, 3 | ax-mp 5 |
. . . . . . . 8
β’ dom
(π β© β) β dom π |
5 | | lspextmo.b |
. . . . . . . . . . . . 13
β’ π΅ = (Baseβπ) |
6 | | eqid 2732 |
. . . . . . . . . . . . 13
β’
(Baseβπ) =
(Baseβπ) |
7 | 5, 6 | lmhmf 20644 |
. . . . . . . . . . . 12
β’ (π β (π LMHom π) β π:π΅βΆ(Baseβπ)) |
8 | 7 | ad2antrl 726 |
. . . . . . . . . . 11
β’ (((π β π΅ β§ (πΎβπ) = π΅) β§ (π β (π LMHom π) β§ β β (π LMHom π))) β π:π΅βΆ(Baseβπ)) |
9 | 8 | ffnd 6718 |
. . . . . . . . . 10
β’ (((π β π΅ β§ (πΎβπ) = π΅) β§ (π β (π LMHom π) β§ β β (π LMHom π))) β π Fn π΅) |
10 | 9 | adantrr 715 |
. . . . . . . . 9
β’ (((π β π΅ β§ (πΎβπ) = π΅) β§ ((π β (π LMHom π) β§ β β (π LMHom π)) β§ π β dom (π β© β))) β π Fn π΅) |
11 | 10 | fndmd 6654 |
. . . . . . . 8
β’ (((π β π΅ β§ (πΎβπ) = π΅) β§ ((π β (π LMHom π) β§ β β (π LMHom π)) β§ π β dom (π β© β))) β dom π = π΅) |
12 | 4, 11 | sseqtrid 4034 |
. . . . . . 7
β’ (((π β π΅ β§ (πΎβπ) = π΅) β§ ((π β (π LMHom π) β§ β β (π LMHom π)) β§ π β dom (π β© β))) β dom (π β© β) β π΅) |
13 | | simplr 767 |
. . . . . . . 8
β’ (((π β π΅ β§ (πΎβπ) = π΅) β§ ((π β (π LMHom π) β§ β β (π LMHom π)) β§ π β dom (π β© β))) β (πΎβπ) = π΅) |
14 | | lmhmlmod1 20643 |
. . . . . . . . . . 11
β’ (π β (π LMHom π) β π β LMod) |
15 | 14 | adantr 481 |
. . . . . . . . . 10
β’ ((π β (π LMHom π) β§ β β (π LMHom π)) β π β LMod) |
16 | 15 | ad2antrl 726 |
. . . . . . . . 9
β’ (((π β π΅ β§ (πΎβπ) = π΅) β§ ((π β (π LMHom π) β§ β β (π LMHom π)) β§ π β dom (π β© β))) β π β LMod) |
17 | | eqid 2732 |
. . . . . . . . . . 11
β’
(LSubSpβπ) =
(LSubSpβπ) |
18 | 17 | lmhmeql 20665 |
. . . . . . . . . 10
β’ ((π β (π LMHom π) β§ β β (π LMHom π)) β dom (π β© β) β (LSubSpβπ)) |
19 | 18 | ad2antrl 726 |
. . . . . . . . 9
β’ (((π β π΅ β§ (πΎβπ) = π΅) β§ ((π β (π LMHom π) β§ β β (π LMHom π)) β§ π β dom (π β© β))) β dom (π β© β) β (LSubSpβπ)) |
20 | | simprr 771 |
. . . . . . . . 9
β’ (((π β π΅ β§ (πΎβπ) = π΅) β§ ((π β (π LMHom π) β§ β β (π LMHom π)) β§ π β dom (π β© β))) β π β dom (π β© β)) |
21 | | lspextmo.k |
. . . . . . . . . 10
β’ πΎ = (LSpanβπ) |
22 | 17, 21 | lspssp 20598 |
. . . . . . . . 9
β’ ((π β LMod β§ dom (π β© β) β (LSubSpβπ) β§ π β dom (π β© β)) β (πΎβπ) β dom (π β© β)) |
23 | 16, 19, 20, 22 | syl3anc 1371 |
. . . . . . . 8
β’ (((π β π΅ β§ (πΎβπ) = π΅) β§ ((π β (π LMHom π) β§ β β (π LMHom π)) β§ π β dom (π β© β))) β (πΎβπ) β dom (π β© β)) |
24 | 13, 23 | eqsstrrd 4021 |
. . . . . . 7
β’ (((π β π΅ β§ (πΎβπ) = π΅) β§ ((π β (π LMHom π) β§ β β (π LMHom π)) β§ π β dom (π β© β))) β π΅ β dom (π β© β)) |
25 | 12, 24 | eqssd 3999 |
. . . . . 6
β’ (((π β π΅ β§ (πΎβπ) = π΅) β§ ((π β (π LMHom π) β§ β β (π LMHom π)) β§ π β dom (π β© β))) β dom (π β© β) = π΅) |
26 | 25 | expr 457 |
. . . . 5
β’ (((π β π΅ β§ (πΎβπ) = π΅) β§ (π β (π LMHom π) β§ β β (π LMHom π))) β (π β dom (π β© β) β dom (π β© β) = π΅)) |
27 | | simprr 771 |
. . . . . . 7
β’ (((π β π΅ β§ (πΎβπ) = π΅) β§ (π β (π LMHom π) β§ β β (π LMHom π))) β β β (π LMHom π)) |
28 | 5, 6 | lmhmf 20644 |
. . . . . . 7
β’ (β β (π LMHom π) β β:π΅βΆ(Baseβπ)) |
29 | | ffn 6717 |
. . . . . . 7
β’ (β:π΅βΆ(Baseβπ) β β Fn π΅) |
30 | 27, 28, 29 | 3syl 18 |
. . . . . 6
β’ (((π β π΅ β§ (πΎβπ) = π΅) β§ (π β (π LMHom π) β§ β β (π LMHom π))) β β Fn π΅) |
31 | | simpll 765 |
. . . . . 6
β’ (((π β π΅ β§ (πΎβπ) = π΅) β§ (π β (π LMHom π) β§ β β (π LMHom π))) β π β π΅) |
32 | | fnreseql 7049 |
. . . . . 6
β’ ((π Fn π΅ β§ β Fn π΅ β§ π β π΅) β ((π βΎ π) = (β βΎ π) β π β dom (π β© β))) |
33 | 9, 30, 31, 32 | syl3anc 1371 |
. . . . 5
β’ (((π β π΅ β§ (πΎβπ) = π΅) β§ (π β (π LMHom π) β§ β β (π LMHom π))) β ((π βΎ π) = (β βΎ π) β π β dom (π β© β))) |
34 | | fneqeql 7047 |
. . . . . 6
β’ ((π Fn π΅ β§ β Fn π΅) β (π = β β dom (π β© β) = π΅)) |
35 | 9, 30, 34 | syl2anc 584 |
. . . . 5
β’ (((π β π΅ β§ (πΎβπ) = π΅) β§ (π β (π LMHom π) β§ β β (π LMHom π))) β (π = β β dom (π β© β) = π΅)) |
36 | 26, 33, 35 | 3imtr4d 293 |
. . . 4
β’ (((π β π΅ β§ (πΎβπ) = π΅) β§ (π β (π LMHom π) β§ β β (π LMHom π))) β ((π βΎ π) = (β βΎ π) β π = β)) |
37 | 1, 36 | syl5 34 |
. . 3
β’ (((π β π΅ β§ (πΎβπ) = π΅) β§ (π β (π LMHom π) β§ β β (π LMHom π))) β (((π βΎ π) = πΉ β§ (β βΎ π) = πΉ) β π = β)) |
38 | 37 | ralrimivva 3200 |
. 2
β’ ((π β π΅ β§ (πΎβπ) = π΅) β βπ β (π LMHom π)ββ β (π LMHom π)(((π βΎ π) = πΉ β§ (β βΎ π) = πΉ) β π = β)) |
39 | | reseq1 5975 |
. . . 4
β’ (π = β β (π βΎ π) = (β βΎ π)) |
40 | 39 | eqeq1d 2734 |
. . 3
β’ (π = β β ((π βΎ π) = πΉ β (β βΎ π) = πΉ)) |
41 | 40 | rmo4 3726 |
. 2
β’
(β*π β
(π LMHom π)(π βΎ π) = πΉ β βπ β (π LMHom π)ββ β (π LMHom π)(((π βΎ π) = πΉ β§ (β βΎ π) = πΉ) β π = β)) |
42 | 38, 41 | sylibr 233 |
1
β’ ((π β π΅ β§ (πΎβπ) = π΅) β β*π β (π LMHom π)(π βΎ π) = πΉ) |