Step | Hyp | Ref
| Expression |
1 | | inss1 4192 |
. . . 4
β’ (π β© π) β π |
2 | | mapdin.h |
. . . . 5
β’ π» = (LHypβπΎ) |
3 | | mapdin.u |
. . . . 5
β’ π = ((DVecHβπΎ)βπ) |
4 | | mapdin.s |
. . . . 5
β’ π = (LSubSpβπ) |
5 | | mapdin.m |
. . . . 5
β’ π = ((mapdβπΎ)βπ) |
6 | | mapdin.k |
. . . . 5
β’ (π β (πΎ β HL β§ π β π»)) |
7 | 2, 3, 6 | dvhlmod 39623 |
. . . . . 6
β’ (π β π β LMod) |
8 | | mapdin.x |
. . . . . 6
β’ (π β π β π) |
9 | | mapdin.y |
. . . . . 6
β’ (π β π β π) |
10 | 4 | lssincl 20470 |
. . . . . 6
β’ ((π β LMod β§ π β π β§ π β π) β (π β© π) β π) |
11 | 7, 8, 9, 10 | syl3anc 1372 |
. . . . 5
β’ (π β (π β© π) β π) |
12 | 2, 3, 4, 5, 6, 11,
8 | mapdord 40151 |
. . . 4
β’ (π β ((πβ(π β© π)) β (πβπ) β (π β© π) β π)) |
13 | 1, 12 | mpbiri 258 |
. . 3
β’ (π β (πβ(π β© π)) β (πβπ)) |
14 | | inss2 4193 |
. . . 4
β’ (π β© π) β π |
15 | 2, 3, 4, 5, 6, 11,
9 | mapdord 40151 |
. . . 4
β’ (π β ((πβ(π β© π)) β (πβπ) β (π β© π) β π)) |
16 | 14, 15 | mpbiri 258 |
. . 3
β’ (π β (πβ(π β© π)) β (πβπ)) |
17 | 13, 16 | ssind 4196 |
. 2
β’ (π β (πβ(π β© π)) β ((πβπ) β© (πβπ))) |
18 | | eqid 2733 |
. . . . 5
β’
((LCDualβπΎ)βπ) = ((LCDualβπΎ)βπ) |
19 | | eqid 2733 |
. . . . . . 7
β’
(LSubSpβ((LCDualβπΎ)βπ)) = (LSubSpβ((LCDualβπΎ)βπ)) |
20 | 2, 5, 3, 4, 18, 19, 6, 8 | mapdcl2 40169 |
. . . . . 6
β’ (π β (πβπ) β (LSubSpβ((LCDualβπΎ)βπ))) |
21 | 2, 5, 18, 19, 6 | mapdrn2 40164 |
. . . . . 6
β’ (π β ran π = (LSubSpβ((LCDualβπΎ)βπ))) |
22 | 20, 21 | eleqtrrd 2837 |
. . . . 5
β’ (π β (πβπ) β ran π) |
23 | 2, 5, 3, 4, 18, 19, 6, 9 | mapdcl2 40169 |
. . . . . 6
β’ (π β (πβπ) β (LSubSpβ((LCDualβπΎ)βπ))) |
24 | 23, 21 | eleqtrrd 2837 |
. . . . 5
β’ (π β (πβπ) β ran π) |
25 | 2, 5, 3, 18, 6, 22, 24 | mapdincl 40174 |
. . . 4
β’ (π β ((πβπ) β© (πβπ)) β ran π) |
26 | 2, 5, 6, 25 | mapdcnvid2 40170 |
. . 3
β’ (π β (πβ(β‘πβ((πβπ) β© (πβπ)))) = ((πβπ) β© (πβπ))) |
27 | | inss1 4192 |
. . . . . . 7
β’ ((πβπ) β© (πβπ)) β (πβπ) |
28 | 26, 27 | eqsstrdi 4002 |
. . . . . 6
β’ (π β (πβ(β‘πβ((πβπ) β© (πβπ)))) β (πβπ)) |
29 | 2, 18, 6 | lcdlmod 40105 |
. . . . . . . . . 10
β’ (π β ((LCDualβπΎ)βπ) β LMod) |
30 | 19 | lssincl 20470 |
. . . . . . . . . 10
β’
((((LCDualβπΎ)βπ) β LMod β§ (πβπ) β (LSubSpβ((LCDualβπΎ)βπ)) β§ (πβπ) β (LSubSpβ((LCDualβπΎ)βπ))) β ((πβπ) β© (πβπ)) β (LSubSpβ((LCDualβπΎ)βπ))) |
31 | 29, 20, 23, 30 | syl3anc 1372 |
. . . . . . . . 9
β’ (π β ((πβπ) β© (πβπ)) β (LSubSpβ((LCDualβπΎ)βπ))) |
32 | 31, 21 | eleqtrrd 2837 |
. . . . . . . 8
β’ (π β ((πβπ) β© (πβπ)) β ran π) |
33 | 2, 5, 3, 4, 6, 32 | mapdcnvcl 40165 |
. . . . . . 7
β’ (π β (β‘πβ((πβπ) β© (πβπ))) β π) |
34 | 2, 3, 4, 5, 6, 33,
8 | mapdord 40151 |
. . . . . 6
β’ (π β ((πβ(β‘πβ((πβπ) β© (πβπ)))) β (πβπ) β (β‘πβ((πβπ) β© (πβπ))) β π)) |
35 | 28, 34 | mpbid 231 |
. . . . 5
β’ (π β (β‘πβ((πβπ) β© (πβπ))) β π) |
36 | 2, 5, 6, 32 | mapdcnvid2 40170 |
. . . . . . 7
β’ (π β (πβ(β‘πβ((πβπ) β© (πβπ)))) = ((πβπ) β© (πβπ))) |
37 | | inss2 4193 |
. . . . . . 7
β’ ((πβπ) β© (πβπ)) β (πβπ) |
38 | 36, 37 | eqsstrdi 4002 |
. . . . . 6
β’ (π β (πβ(β‘πβ((πβπ) β© (πβπ)))) β (πβπ)) |
39 | 2, 3, 4, 5, 6, 33,
9 | mapdord 40151 |
. . . . . 6
β’ (π β ((πβ(β‘πβ((πβπ) β© (πβπ)))) β (πβπ) β (β‘πβ((πβπ) β© (πβπ))) β π)) |
40 | 38, 39 | mpbid 231 |
. . . . 5
β’ (π β (β‘πβ((πβπ) β© (πβπ))) β π) |
41 | 35, 40 | ssind 4196 |
. . . 4
β’ (π β (β‘πβ((πβπ) β© (πβπ))) β (π β© π)) |
42 | 2, 3, 4, 5, 6, 33,
11 | mapdord 40151 |
. . . 4
β’ (π β ((πβ(β‘πβ((πβπ) β© (πβπ)))) β (πβ(π β© π)) β (β‘πβ((πβπ) β© (πβπ))) β (π β© π))) |
43 | 41, 42 | mpbird 257 |
. . 3
β’ (π β (πβ(β‘πβ((πβπ) β© (πβπ)))) β (πβ(π β© π))) |
44 | 26, 43 | eqsstrrd 3987 |
. 2
β’ (π β ((πβπ) β© (πβπ)) β (πβ(π β© π))) |
45 | 17, 44 | eqssd 3965 |
1
β’ (π β (πβ(π β© π)) = ((πβπ) β© (πβπ))) |