Step | Hyp | Ref
| Expression |
1 | | mapdpglem3.te |
. . . 4
β’ (π β π‘ β ((πβ(πβ{π})) β (πβ(πβ{π})))) |
2 | | mapdpglem3.e |
. . . . 5
β’ (π β (πβ(πβ{π})) = (π½β{πΊ})) |
3 | 2 | oveq1d 7376 |
. . . 4
β’ (π β ((πβ(πβ{π})) β (πβ(πβ{π}))) = ((π½β{πΊ}) β (πβ(πβ{π})))) |
4 | 1, 3 | eleqtrd 2836 |
. . 3
β’ (π β π‘ β ((π½β{πΊ}) β (πβ(πβ{π})))) |
5 | | r19.41v 3182 |
. . . . . . 7
β’
(βπ β
π΅ (π€ = (π Β· πΊ) β§ βπ§ β (πβ(πβ{π}))π‘ = (π€π
π§)) β (βπ β π΅ π€ = (π Β· πΊ) β§ βπ§ β (πβ(πβ{π}))π‘ = (π€π
π§))) |
6 | | mapdpglem.h |
. . . . . . . . . . 11
β’ π» = (LHypβπΎ) |
7 | | mapdpglem.c |
. . . . . . . . . . 11
β’ πΆ = ((LCDualβπΎ)βπ) |
8 | | mapdpglem.k |
. . . . . . . . . . 11
β’ (π β (πΎ β HL β§ π β π»)) |
9 | 6, 7, 8 | lcdlmod 40105 |
. . . . . . . . . 10
β’ (π β πΆ β LMod) |
10 | | mapdpglem3.g |
. . . . . . . . . 10
β’ (π β πΊ β πΉ) |
11 | | eqid 2733 |
. . . . . . . . . . 11
β’
(ScalarβπΆ) =
(ScalarβπΆ) |
12 | | eqid 2733 |
. . . . . . . . . . 11
β’
(Baseβ(ScalarβπΆ)) = (Baseβ(ScalarβπΆ)) |
13 | | mapdpglem3.f |
. . . . . . . . . . 11
β’ πΉ = (BaseβπΆ) |
14 | | mapdpglem3.t |
. . . . . . . . . . 11
β’ Β· = (
Β·π βπΆ) |
15 | | mapdpglem2.j |
. . . . . . . . . . 11
β’ π½ = (LSpanβπΆ) |
16 | 11, 12, 13, 14, 15 | lspsnel 20508 |
. . . . . . . . . 10
β’ ((πΆ β LMod β§ πΊ β πΉ) β (π€ β (π½β{πΊ}) β βπ β (Baseβ(ScalarβπΆ))π€ = (π Β· πΊ))) |
17 | 9, 10, 16 | syl2anc 585 |
. . . . . . . . 9
β’ (π β (π€ β (π½β{πΊ}) β βπ β (Baseβ(ScalarβπΆ))π€ = (π Β· πΊ))) |
18 | | mapdpglem.u |
. . . . . . . . . . 11
β’ π = ((DVecHβπΎ)βπ) |
19 | | mapdpglem3.a |
. . . . . . . . . . 11
β’ π΄ = (Scalarβπ) |
20 | | mapdpglem3.b |
. . . . . . . . . . 11
β’ π΅ = (Baseβπ΄) |
21 | 6, 18, 19, 20, 7, 11, 12, 8 | lcdsbase 40113 |
. . . . . . . . . 10
β’ (π β
(Baseβ(ScalarβπΆ)) = π΅) |
22 | 21 | rexeqdv 3313 |
. . . . . . . . 9
β’ (π β (βπ β (Baseβ(ScalarβπΆ))π€ = (π Β· πΊ) β βπ β π΅ π€ = (π Β· πΊ))) |
23 | 17, 22 | bitrd 279 |
. . . . . . . 8
β’ (π β (π€ β (π½β{πΊ}) β βπ β π΅ π€ = (π Β· πΊ))) |
24 | 23 | anbi1d 631 |
. . . . . . 7
β’ (π β ((π€ β (π½β{πΊ}) β§ βπ§ β (πβ(πβ{π}))π‘ = (π€π
π§)) β (βπ β π΅ π€ = (π Β· πΊ) β§ βπ§ β (πβ(πβ{π}))π‘ = (π€π
π§)))) |
25 | 5, 24 | bitr4id 290 |
. . . . . 6
β’ (π β (βπ β π΅ (π€ = (π Β· πΊ) β§ βπ§ β (πβ(πβ{π}))π‘ = (π€π
π§)) β (π€ β (π½β{πΊ}) β§ βπ§ β (πβ(πβ{π}))π‘ = (π€π
π§)))) |
26 | 25 | exbidv 1925 |
. . . . 5
β’ (π β (βπ€βπ β π΅ (π€ = (π Β· πΊ) β§ βπ§ β (πβ(πβ{π}))π‘ = (π€π
π§)) β βπ€(π€ β (π½β{πΊ}) β§ βπ§ β (πβ(πβ{π}))π‘ = (π€π
π§)))) |
27 | | df-rex 3071 |
. . . . 5
β’
(βπ€ β
(π½β{πΊ})βπ§ β (πβ(πβ{π}))π‘ = (π€π
π§) β βπ€(π€ β (π½β{πΊ}) β§ βπ§ β (πβ(πβ{π}))π‘ = (π€π
π§))) |
28 | 26, 27 | bitr4di 289 |
. . . 4
β’ (π β (βπ€βπ β π΅ (π€ = (π Β· πΊ) β§ βπ§ β (πβ(πβ{π}))π‘ = (π€π
π§)) β βπ€ β (π½β{πΊ})βπ§ β (πβ(πβ{π}))π‘ = (π€π
π§))) |
29 | | mapdpglem3.r |
. . . . 5
β’ π
= (-gβπΆ) |
30 | | mapdpglem1.p |
. . . . 5
β’ β =
(LSSumβπΆ) |
31 | | eqid 2733 |
. . . . . . . 8
β’
(LSubSpβπΆ) =
(LSubSpβπΆ) |
32 | 31 | lsssssubg 20463 |
. . . . . . 7
β’ (πΆ β LMod β
(LSubSpβπΆ) β
(SubGrpβπΆ)) |
33 | 9, 32 | syl 17 |
. . . . . 6
β’ (π β (LSubSpβπΆ) β (SubGrpβπΆ)) |
34 | 13, 31, 15 | lspsncl 20482 |
. . . . . . 7
β’ ((πΆ β LMod β§ πΊ β πΉ) β (π½β{πΊ}) β (LSubSpβπΆ)) |
35 | 9, 10, 34 | syl2anc 585 |
. . . . . 6
β’ (π β (π½β{πΊ}) β (LSubSpβπΆ)) |
36 | 33, 35 | sseldd 3949 |
. . . . 5
β’ (π β (π½β{πΊ}) β (SubGrpβπΆ)) |
37 | | mapdpglem.m |
. . . . . . 7
β’ π = ((mapdβπΎ)βπ) |
38 | | eqid 2733 |
. . . . . . 7
β’
(LSubSpβπ) =
(LSubSpβπ) |
39 | 6, 18, 8 | dvhlmod 39623 |
. . . . . . . 8
β’ (π β π β LMod) |
40 | | mapdpglem.y |
. . . . . . . 8
β’ (π β π β π) |
41 | | mapdpglem.v |
. . . . . . . . 9
β’ π = (Baseβπ) |
42 | | mapdpglem.n |
. . . . . . . . 9
β’ π = (LSpanβπ) |
43 | 41, 38, 42 | lspsncl 20482 |
. . . . . . . 8
β’ ((π β LMod β§ π β π) β (πβ{π}) β (LSubSpβπ)) |
44 | 39, 40, 43 | syl2anc 585 |
. . . . . . 7
β’ (π β (πβ{π}) β (LSubSpβπ)) |
45 | 6, 37, 18, 38, 7, 31, 8, 44 | mapdcl2 40169 |
. . . . . 6
β’ (π β (πβ(πβ{π})) β (LSubSpβπΆ)) |
46 | 33, 45 | sseldd 3949 |
. . . . 5
β’ (π β (πβ(πβ{π})) β (SubGrpβπΆ)) |
47 | 29, 30, 36, 46 | lsmelvalm 19441 |
. . . 4
β’ (π β (π‘ β ((π½β{πΊ}) β (πβ(πβ{π}))) β βπ€ β (π½β{πΊ})βπ§ β (πβ(πβ{π}))π‘ = (π€π
π§))) |
48 | 28, 47 | bitr4d 282 |
. . 3
β’ (π β (βπ€βπ β π΅ (π€ = (π Β· πΊ) β§ βπ§ β (πβ(πβ{π}))π‘ = (π€π
π§)) β π‘ β ((π½β{πΊ}) β (πβ(πβ{π}))))) |
49 | 4, 48 | mpbird 257 |
. 2
β’ (π β βπ€βπ β π΅ (π€ = (π Β· πΊ) β§ βπ§ β (πβ(πβ{π}))π‘ = (π€π
π§))) |
50 | | ovex 7394 |
. . . . 5
β’ (π Β· πΊ) β V |
51 | | oveq1 7368 |
. . . . . . 7
β’ (π€ = (π Β· πΊ) β (π€π
π§) = ((π Β· πΊ)π
π§)) |
52 | 51 | eqeq2d 2744 |
. . . . . 6
β’ (π€ = (π Β· πΊ) β (π‘ = (π€π
π§) β π‘ = ((π Β· πΊ)π
π§))) |
53 | 52 | rexbidv 3172 |
. . . . 5
β’ (π€ = (π Β· πΊ) β (βπ§ β (πβ(πβ{π}))π‘ = (π€π
π§) β βπ§ β (πβ(πβ{π}))π‘ = ((π Β· πΊ)π
π§))) |
54 | 50, 53 | ceqsexv 3496 |
. . . 4
β’
(βπ€(π€ = (π Β· πΊ) β§ βπ§ β (πβ(πβ{π}))π‘ = (π€π
π§)) β βπ§ β (πβ(πβ{π}))π‘ = ((π Β· πΊ)π
π§)) |
55 | 54 | rexbii 3094 |
. . 3
β’
(βπ β
π΅ βπ€(π€ = (π Β· πΊ) β§ βπ§ β (πβ(πβ{π}))π‘ = (π€π
π§)) β βπ β π΅ βπ§ β (πβ(πβ{π}))π‘ = ((π Β· πΊ)π
π§)) |
56 | | rexcom4 3270 |
. . 3
β’
(βπ β
π΅ βπ€(π€ = (π Β· πΊ) β§ βπ§ β (πβ(πβ{π}))π‘ = (π€π
π§)) β βπ€βπ β π΅ (π€ = (π Β· πΊ) β§ βπ§ β (πβ(πβ{π}))π‘ = (π€π
π§))) |
57 | 55, 56 | bitr3i 277 |
. 2
β’
(βπ β
π΅ βπ§ β (πβ(πβ{π}))π‘ = ((π Β· πΊ)π
π§) β βπ€βπ β π΅ (π€ = (π Β· πΊ) β§ βπ§ β (πβ(πβ{π}))π‘ = (π€π
π§))) |
58 | 49, 57 | sylibr 233 |
1
β’ (π β βπ β π΅ βπ§ β (πβ(πβ{π}))π‘ = ((π Β· πΊ)π
π§)) |