Step | Hyp | Ref
| Expression |
1 | | eqgvscpbl.v |
. . . 4
β’ π΅ = (Baseβπ) |
2 | | eqid 2733 |
. . . 4
β’ (π ~QG πΊ) = (π ~QG πΊ) |
3 | | eqgvscpbl.s |
. . . 4
β’ π =
(Baseβ(Scalarβπ)) |
4 | | eqgvscpbl.p |
. . . 4
β’ Β· = (
Β·π βπ) |
5 | | eqgvscpbl.m |
. . . 4
β’ (π β π β LMod) |
6 | | eqgvscpbl.g |
. . . 4
β’ (π β πΊ β (LSubSpβπ)) |
7 | | eqgvscpbl.k |
. . . 4
β’ (π β πΎ β π) |
8 | 1, 2, 3, 4, 5, 6, 7 | eqgvscpbl 32189 |
. . 3
β’ (π β (π(π ~QG πΊ)π β (πΎ Β· π)(π ~QG πΊ)(πΎ Β· π))) |
9 | | eqid 2733 |
. . . . . . 7
β’
(LSubSpβπ) =
(LSubSpβπ) |
10 | 9 | lsssubg 20433 |
. . . . . 6
β’ ((π β LMod β§ πΊ β (LSubSpβπ)) β πΊ β (SubGrpβπ)) |
11 | 5, 6, 10 | syl2anc 585 |
. . . . 5
β’ (π β πΊ β (SubGrpβπ)) |
12 | 1, 2 | eqger 18985 |
. . . . 5
β’ (πΊ β (SubGrpβπ) β (π ~QG πΊ) Er π΅) |
13 | 11, 12 | syl 17 |
. . . 4
β’ (π β (π ~QG πΊ) Er π΅) |
14 | | qusvscpbl.u |
. . . 4
β’ (π β π β π΅) |
15 | 13, 14 | erth 8700 |
. . 3
β’ (π β (π(π ~QG πΊ)π β [π](π ~QG πΊ) = [π](π ~QG πΊ))) |
16 | | eqid 2733 |
. . . . . 6
β’
(Scalarβπ) =
(Scalarβπ) |
17 | 1, 16, 4, 3 | lmodvscl 20354 |
. . . . 5
β’ ((π β LMod β§ πΎ β π β§ π β π΅) β (πΎ Β· π) β π΅) |
18 | 5, 7, 14, 17 | syl3anc 1372 |
. . . 4
β’ (π β (πΎ Β· π) β π΅) |
19 | 13, 18 | erth 8700 |
. . 3
β’ (π β ((πΎ Β· π)(π ~QG πΊ)(πΎ Β· π) β [(πΎ Β· π)](π ~QG πΊ) = [(πΎ Β· π)](π ~QG πΊ))) |
20 | 8, 15, 19 | 3imtr3d 293 |
. 2
β’ (π β ([π](π ~QG πΊ) = [π](π ~QG πΊ) β [(πΎ Β· π)](π ~QG πΊ) = [(πΎ Β· π)](π ~QG πΊ))) |
21 | | eceq1 8689 |
. . . . 5
β’ (π₯ = π β [π₯](π ~QG πΊ) = [π](π ~QG πΊ)) |
22 | | qusvscpbl.f |
. . . . 5
β’ πΉ = (π₯ β π΅ β¦ [π₯](π ~QG πΊ)) |
23 | | ovex 7391 |
. . . . . 6
β’ (π ~QG πΊ) β V |
24 | | ecexg 8655 |
. . . . . 6
β’ ((π ~QG πΊ) β V β [π](π ~QG πΊ) β V) |
25 | 23, 24 | ax-mp 5 |
. . . . 5
β’ [π](π ~QG πΊ) β V |
26 | 21, 22, 25 | fvmpt 6949 |
. . . 4
β’ (π β π΅ β (πΉβπ) = [π](π ~QG πΊ)) |
27 | 14, 26 | syl 17 |
. . 3
β’ (π β (πΉβπ) = [π](π ~QG πΊ)) |
28 | | qusvscpbl.v |
. . . 4
β’ (π β π β π΅) |
29 | | eceq1 8689 |
. . . . 5
β’ (π₯ = π β [π₯](π ~QG πΊ) = [π](π ~QG πΊ)) |
30 | | ecexg 8655 |
. . . . . 6
β’ ((π ~QG πΊ) β V β [π](π ~QG πΊ) β V) |
31 | 23, 30 | ax-mp 5 |
. . . . 5
β’ [π](π ~QG πΊ) β V |
32 | 29, 22, 31 | fvmpt 6949 |
. . . 4
β’ (π β π΅ β (πΉβπ) = [π](π ~QG πΊ)) |
33 | 28, 32 | syl 17 |
. . 3
β’ (π β (πΉβπ) = [π](π ~QG πΊ)) |
34 | 27, 33 | eqeq12d 2749 |
. 2
β’ (π β ((πΉβπ) = (πΉβπ) β [π](π ~QG πΊ) = [π](π ~QG πΊ))) |
35 | | eceq1 8689 |
. . . . 5
β’ (π₯ = (πΎ Β· π) β [π₯](π ~QG πΊ) = [(πΎ Β· π)](π ~QG πΊ)) |
36 | | ecexg 8655 |
. . . . . 6
β’ ((π ~QG πΊ) β V β [(πΎ Β· π)](π ~QG πΊ) β V) |
37 | 23, 36 | ax-mp 5 |
. . . . 5
β’ [(πΎ Β· π)](π ~QG πΊ) β V |
38 | 35, 22, 37 | fvmpt 6949 |
. . . 4
β’ ((πΎ Β· π) β π΅ β (πΉβ(πΎ Β· π)) = [(πΎ Β· π)](π ~QG πΊ)) |
39 | 18, 38 | syl 17 |
. . 3
β’ (π β (πΉβ(πΎ Β· π)) = [(πΎ Β· π)](π ~QG πΊ)) |
40 | 1, 16, 4, 3 | lmodvscl 20354 |
. . . . 5
β’ ((π β LMod β§ πΎ β π β§ π β π΅) β (πΎ Β· π) β π΅) |
41 | 5, 7, 28, 40 | syl3anc 1372 |
. . . 4
β’ (π β (πΎ Β· π) β π΅) |
42 | | eceq1 8689 |
. . . . 5
β’ (π₯ = (πΎ Β· π) β [π₯](π ~QG πΊ) = [(πΎ Β· π)](π ~QG πΊ)) |
43 | | ecexg 8655 |
. . . . . 6
β’ ((π ~QG πΊ) β V β [(πΎ Β· π)](π ~QG πΊ) β V) |
44 | 23, 43 | ax-mp 5 |
. . . . 5
β’ [(πΎ Β· π)](π ~QG πΊ) β V |
45 | 42, 22, 44 | fvmpt 6949 |
. . . 4
β’ ((πΎ Β· π) β π΅ β (πΉβ(πΎ Β· π)) = [(πΎ Β· π)](π ~QG πΊ)) |
46 | 41, 45 | syl 17 |
. . 3
β’ (π β (πΉβ(πΎ Β· π)) = [(πΎ Β· π)](π ~QG πΊ)) |
47 | 39, 46 | eqeq12d 2749 |
. 2
β’ (π β ((πΉβ(πΎ Β· π)) = (πΉβ(πΎ Β· π)) β [(πΎ Β· π)](π ~QG πΊ) = [(πΎ Β· π)](π ~QG πΊ))) |
48 | 20, 34, 47 | 3imtr4d 294 |
1
β’ (π β ((πΉβπ) = (πΉβπ) β (πΉβ(πΎ Β· π)) = (πΉβ(πΎ Β· π)))) |