Step | Hyp | Ref
| Expression |
1 | | lsslsp.x |
. . . . 5
β’ π = (π βΎs π) |
2 | | lsslsp.l |
. . . . 5
β’ πΏ = (LSubSpβπ) |
3 | 1, 2 | lsslmod 20805 |
. . . 4
β’ ((π β LMod β§ π β πΏ) β π β LMod) |
4 | 3 | 3adant3 1129 |
. . 3
β’ ((π β LMod β§ π β πΏ β§ πΊ β π) β π β LMod) |
5 | | simp1 1133 |
. . . . 5
β’ ((π β LMod β§ π β πΏ β§ πΊ β π) β π β LMod) |
6 | | simp3 1135 |
. . . . . 6
β’ ((π β LMod β§ π β πΏ β§ πΊ β π) β πΊ β π) |
7 | | eqid 2726 |
. . . . . . . 8
β’
(Baseβπ) =
(Baseβπ) |
8 | 7, 2 | lssss 20781 |
. . . . . . 7
β’ (π β πΏ β π β (Baseβπ)) |
9 | 8 | 3ad2ant2 1131 |
. . . . . 6
β’ ((π β LMod β§ π β πΏ β§ πΊ β π) β π β (Baseβπ)) |
10 | 6, 9 | sstrd 3987 |
. . . . 5
β’ ((π β LMod β§ π β πΏ β§ πΊ β π) β πΊ β (Baseβπ)) |
11 | | lsslsp.m |
. . . . . 6
β’ π = (LSpanβπ) |
12 | 7, 2, 11 | lspcl 20821 |
. . . . 5
β’ ((π β LMod β§ πΊ β (Baseβπ)) β (πβπΊ) β πΏ) |
13 | 5, 10, 12 | syl2anc 583 |
. . . 4
β’ ((π β LMod β§ π β πΏ β§ πΊ β π) β (πβπΊ) β πΏ) |
14 | 2, 11 | lspssp 20833 |
. . . 4
β’ ((π β LMod β§ π β πΏ β§ πΊ β π) β (πβπΊ) β π) |
15 | | eqid 2726 |
. . . . . 6
β’
(LSubSpβπ) =
(LSubSpβπ) |
16 | 1, 2, 15 | lsslss 20806 |
. . . . 5
β’ ((π β LMod β§ π β πΏ) β ((πβπΊ) β (LSubSpβπ) β ((πβπΊ) β πΏ β§ (πβπΊ) β π))) |
17 | 16 | 3adant3 1129 |
. . . 4
β’ ((π β LMod β§ π β πΏ β§ πΊ β π) β ((πβπΊ) β (LSubSpβπ) β ((πβπΊ) β πΏ β§ (πβπΊ) β π))) |
18 | 13, 14, 17 | mpbir2and 710 |
. . 3
β’ ((π β LMod β§ π β πΏ β§ πΊ β π) β (πβπΊ) β (LSubSpβπ)) |
19 | 7, 11 | lspssid 20830 |
. . . 4
β’ ((π β LMod β§ πΊ β (Baseβπ)) β πΊ β (πβπΊ)) |
20 | 5, 10, 19 | syl2anc 583 |
. . 3
β’ ((π β LMod β§ π β πΏ β§ πΊ β π) β πΊ β (πβπΊ)) |
21 | | lsslsp.n |
. . . 4
β’ π = (LSpanβπ) |
22 | 15, 21 | lspssp 20833 |
. . 3
β’ ((π β LMod β§ (πβπΊ) β (LSubSpβπ) β§ πΊ β (πβπΊ)) β (πβπΊ) β (πβπΊ)) |
23 | 4, 18, 20, 22 | syl3anc 1368 |
. 2
β’ ((π β LMod β§ π β πΏ β§ πΊ β π) β (πβπΊ) β (πβπΊ)) |
24 | 1, 7 | ressbas2 17189 |
. . . . . . . 8
β’ (π β (Baseβπ) β π = (Baseβπ)) |
25 | 9, 24 | syl 17 |
. . . . . . 7
β’ ((π β LMod β§ π β πΏ β§ πΊ β π) β π = (Baseβπ)) |
26 | 6, 25 | sseqtrd 4017 |
. . . . . 6
β’ ((π β LMod β§ π β πΏ β§ πΊ β π) β πΊ β (Baseβπ)) |
27 | | eqid 2726 |
. . . . . . 7
β’
(Baseβπ) =
(Baseβπ) |
28 | 27, 15, 21 | lspcl 20821 |
. . . . . 6
β’ ((π β LMod β§ πΊ β (Baseβπ)) β (πβπΊ) β (LSubSpβπ)) |
29 | 4, 26, 28 | syl2anc 583 |
. . . . 5
β’ ((π β LMod β§ π β πΏ β§ πΊ β π) β (πβπΊ) β (LSubSpβπ)) |
30 | 1, 2, 15 | lsslss 20806 |
. . . . . 6
β’ ((π β LMod β§ π β πΏ) β ((πβπΊ) β (LSubSpβπ) β ((πβπΊ) β πΏ β§ (πβπΊ) β π))) |
31 | 30 | 3adant3 1129 |
. . . . 5
β’ ((π β LMod β§ π β πΏ β§ πΊ β π) β ((πβπΊ) β (LSubSpβπ) β ((πβπΊ) β πΏ β§ (πβπΊ) β π))) |
32 | 29, 31 | mpbid 231 |
. . . 4
β’ ((π β LMod β§ π β πΏ β§ πΊ β π) β ((πβπΊ) β πΏ β§ (πβπΊ) β π)) |
33 | 32 | simpld 494 |
. . 3
β’ ((π β LMod β§ π β πΏ β§ πΊ β π) β (πβπΊ) β πΏ) |
34 | 27, 21 | lspssid 20830 |
. . . 4
β’ ((π β LMod β§ πΊ β (Baseβπ)) β πΊ β (πβπΊ)) |
35 | 4, 26, 34 | syl2anc 583 |
. . 3
β’ ((π β LMod β§ π β πΏ β§ πΊ β π) β πΊ β (πβπΊ)) |
36 | 2, 11 | lspssp 20833 |
. . 3
β’ ((π β LMod β§ (πβπΊ) β πΏ β§ πΊ β (πβπΊ)) β (πβπΊ) β (πβπΊ)) |
37 | 5, 33, 35, 36 | syl3anc 1368 |
. 2
β’ ((π β LMod β§ π β πΏ β§ πΊ β π) β (πβπΊ) β (πβπΊ)) |
38 | 23, 37 | eqssd 3994 |
1
β’ ((π β LMod β§ π β πΏ β§ πΊ β π) β (πβπΊ) = (πβπΊ)) |