Step | Hyp | Ref
| Expression |
1 | | lsslsp.x |
. . . . 5
β’ π = (π βΎs π) |
2 | | lsslsp.l |
. . . . 5
β’ πΏ = (LSubSpβπ) |
3 | 1, 2 | lsslmod 13505 |
. . . 4
β’ ((π β LMod β§ π β πΏ) β π β LMod) |
4 | 3 | 3adant3 1017 |
. . 3
β’ ((π β LMod β§ π β πΏ β§ πΊ β π) β π β LMod) |
5 | | simp1 997 |
. . . . 5
β’ ((π β LMod β§ π β πΏ β§ πΊ β π) β π β LMod) |
6 | | simp3 999 |
. . . . . 6
β’ ((π β LMod β§ π β πΏ β§ πΊ β π) β πΊ β π) |
7 | | eqid 2177 |
. . . . . . . 8
β’
(Baseβπ) =
(Baseβπ) |
8 | 7, 2 | lssssg 13485 |
. . . . . . 7
β’ ((π β LMod β§ π β πΏ) β π β (Baseβπ)) |
9 | 8 | 3adant3 1017 |
. . . . . 6
β’ ((π β LMod β§ π β πΏ β§ πΊ β π) β π β (Baseβπ)) |
10 | 6, 9 | sstrd 3167 |
. . . . 5
β’ ((π β LMod β§ π β πΏ β§ πΊ β π) β πΊ β (Baseβπ)) |
11 | | lsslsp.m |
. . . . . 6
β’ π = (LSpanβπ) |
12 | 7, 2, 11 | lspcl 13516 |
. . . . 5
β’ ((π β LMod β§ πΊ β (Baseβπ)) β (πβπΊ) β πΏ) |
13 | 5, 10, 12 | syl2anc 411 |
. . . 4
β’ ((π β LMod β§ π β πΏ β§ πΊ β π) β (πβπΊ) β πΏ) |
14 | 2, 11 | lspssp 13528 |
. . . 4
β’ ((π β LMod β§ π β πΏ β§ πΊ β π) β (πβπΊ) β π) |
15 | | eqid 2177 |
. . . . . 6
β’
(LSubSpβπ) =
(LSubSpβπ) |
16 | 1, 2, 15 | lsslss 13506 |
. . . . 5
β’ ((π β LMod β§ π β πΏ) β ((πβπΊ) β (LSubSpβπ) β ((πβπΊ) β πΏ β§ (πβπΊ) β π))) |
17 | 16 | 3adant3 1017 |
. . . 4
β’ ((π β LMod β§ π β πΏ β§ πΊ β π) β ((πβπΊ) β (LSubSpβπ) β ((πβπΊ) β πΏ β§ (πβπΊ) β π))) |
18 | 13, 14, 17 | mpbir2and 944 |
. . 3
β’ ((π β LMod β§ π β πΏ β§ πΊ β π) β (πβπΊ) β (LSubSpβπ)) |
19 | 7, 11 | lspssid 13525 |
. . . 4
β’ ((π β LMod β§ πΊ β (Baseβπ)) β πΊ β (πβπΊ)) |
20 | 5, 10, 19 | syl2anc 411 |
. . 3
β’ ((π β LMod β§ π β πΏ β§ πΊ β π) β πΊ β (πβπΊ)) |
21 | | lsslsp.n |
. . . 4
β’ π = (LSpanβπ) |
22 | 15, 21 | lspssp 13528 |
. . 3
β’ ((π β LMod β§ (πβπΊ) β (LSubSpβπ) β§ πΊ β (πβπΊ)) β (πβπΊ) β (πβπΊ)) |
23 | 4, 18, 20, 22 | syl3anc 1238 |
. 2
β’ ((π β LMod β§ π β πΏ β§ πΊ β π) β (πβπΊ) β (πβπΊ)) |
24 | 1 | a1i 9 |
. . . . . . . 8
β’ ((π β LMod β§ π β πΏ β§ πΊ β π) β π = (π βΎs π)) |
25 | | eqidd 2178 |
. . . . . . . 8
β’ ((π β LMod β§ π β πΏ β§ πΊ β π) β (Baseβπ) = (Baseβπ)) |
26 | 24, 25, 5, 9 | ressbas2d 12531 |
. . . . . . 7
β’ ((π β LMod β§ π β πΏ β§ πΊ β π) β π = (Baseβπ)) |
27 | 6, 26 | sseqtrd 3195 |
. . . . . 6
β’ ((π β LMod β§ π β πΏ β§ πΊ β π) β πΊ β (Baseβπ)) |
28 | | eqid 2177 |
. . . . . . 7
β’
(Baseβπ) =
(Baseβπ) |
29 | 28, 15, 21 | lspcl 13516 |
. . . . . 6
β’ ((π β LMod β§ πΊ β (Baseβπ)) β (πβπΊ) β (LSubSpβπ)) |
30 | 4, 27, 29 | syl2anc 411 |
. . . . 5
β’ ((π β LMod β§ π β πΏ β§ πΊ β π) β (πβπΊ) β (LSubSpβπ)) |
31 | 1, 2, 15 | lsslss 13506 |
. . . . . 6
β’ ((π β LMod β§ π β πΏ) β ((πβπΊ) β (LSubSpβπ) β ((πβπΊ) β πΏ β§ (πβπΊ) β π))) |
32 | 31 | 3adant3 1017 |
. . . . 5
β’ ((π β LMod β§ π β πΏ β§ πΊ β π) β ((πβπΊ) β (LSubSpβπ) β ((πβπΊ) β πΏ β§ (πβπΊ) β π))) |
33 | 30, 32 | mpbid 147 |
. . . 4
β’ ((π β LMod β§ π β πΏ β§ πΊ β π) β ((πβπΊ) β πΏ β§ (πβπΊ) β π)) |
34 | 33 | simpld 112 |
. . 3
β’ ((π β LMod β§ π β πΏ β§ πΊ β π) β (πβπΊ) β πΏ) |
35 | 28, 21 | lspssid 13525 |
. . . 4
β’ ((π β LMod β§ πΊ β (Baseβπ)) β πΊ β (πβπΊ)) |
36 | 4, 27, 35 | syl2anc 411 |
. . 3
β’ ((π β LMod β§ π β πΏ β§ πΊ β π) β πΊ β (πβπΊ)) |
37 | 2, 11 | lspssp 13528 |
. . 3
β’ ((π β LMod β§ (πβπΊ) β πΏ β§ πΊ β (πβπΊ)) β (πβπΊ) β (πβπΊ)) |
38 | 5, 34, 36, 37 | syl3anc 1238 |
. 2
β’ ((π β LMod β§ π β πΏ β§ πΊ β π) β (πβπΊ) β (πβπΊ)) |
39 | 23, 38 | eqssd 3174 |
1
β’ ((π β LMod β§ π β πΏ β§ πΊ β π) β (πβπΊ) = (πβπΊ)) |