Step | Hyp | Ref
| Expression |
1 | | lshpkrlem.v |
. . 3
β’ π = (Baseβπ) |
2 | | lshpkrlem.a |
. . 3
β’ + =
(+gβπ) |
3 | | lshpkrlem.n |
. . 3
β’ π = (LSpanβπ) |
4 | | lshpkrlem.p |
. . 3
β’ β =
(LSSumβπ) |
5 | | lshpkrlem.h |
. . 3
β’ π» = (LSHypβπ) |
6 | | lshpkrlem.w |
. . . 4
β’ (π β π β LVec) |
7 | 6 | adantr 482 |
. . 3
β’ ((π β§ (π β πΎ β§ π’ β π β§ π£ β π)) β π β LVec) |
8 | | lshpkrlem.u |
. . . 4
β’ (π β π β π») |
9 | 8 | adantr 482 |
. . 3
β’ ((π β§ (π β πΎ β§ π’ β π β§ π£ β π)) β π β π») |
10 | | lshpkrlem.z |
. . . 4
β’ (π β π β π) |
11 | 10 | adantr 482 |
. . 3
β’ ((π β§ (π β πΎ β§ π’ β π β§ π£ β π)) β π β π) |
12 | | simpr2 1196 |
. . 3
β’ ((π β§ (π β πΎ β§ π’ β π β§ π£ β π)) β π’ β π) |
13 | | lshpkrlem.e |
. . . 4
β’ (π β (π β (πβ{π})) = π) |
14 | 13 | adantr 482 |
. . 3
β’ ((π β§ (π β πΎ β§ π’ β π β§ π£ β π)) β (π β (πβ{π})) = π) |
15 | | lshpkrlem.d |
. . 3
β’ π· = (Scalarβπ) |
16 | | lshpkrlem.k |
. . 3
β’ πΎ = (Baseβπ·) |
17 | | lshpkrlem.t |
. . 3
β’ Β· = (
Β·π βπ) |
18 | | lshpkrlem.o |
. . 3
β’ 0 =
(0gβπ·) |
19 | | lshpkrlem.g |
. . 3
β’ πΊ = (π₯ β π β¦ (β©π β πΎ βπ¦ β π π₯ = (π¦ + (π Β· π)))) |
20 | 1, 2, 3, 4, 5, 7, 9, 11, 12, 14, 15, 16, 17, 18, 19 | lshpkrlem3 37620 |
. 2
β’ ((π β§ (π β πΎ β§ π’ β π β§ π£ β π)) β βπ β π π’ = (π + ((πΊβπ’) Β· π))) |
21 | | simpr3 1197 |
. . 3
β’ ((π β§ (π β πΎ β§ π’ β π β§ π£ β π)) β π£ β π) |
22 | 1, 2, 3, 4, 5, 7, 9, 11, 21, 14, 15, 16, 17, 18, 19 | lshpkrlem3 37620 |
. 2
β’ ((π β§ (π β πΎ β§ π’ β π β§ π£ β π)) β βπ β π π£ = (π + ((πΊβπ£) Β· π))) |
23 | | lveclmod 20582 |
. . . . 5
β’ (π β LVec β π β LMod) |
24 | 7, 23 | syl 17 |
. . . 4
β’ ((π β§ (π β πΎ β§ π’ β π β§ π£ β π)) β π β LMod) |
25 | | simpr1 1195 |
. . . . 5
β’ ((π β§ (π β πΎ β§ π’ β π β§ π£ β π)) β π β πΎ) |
26 | 1, 15, 17, 16 | lmodvscl 20354 |
. . . . 5
β’ ((π β LMod β§ π β πΎ β§ π’ β π) β (π Β· π’) β π) |
27 | 24, 25, 12, 26 | syl3anc 1372 |
. . . 4
β’ ((π β§ (π β πΎ β§ π’ β π β§ π£ β π)) β (π Β· π’) β π) |
28 | 1, 2 | lmodvacl 20351 |
. . . 4
β’ ((π β LMod β§ (π Β· π’) β π β§ π£ β π) β ((π Β· π’) + π£) β π) |
29 | 24, 27, 21, 28 | syl3anc 1372 |
. . 3
β’ ((π β§ (π β πΎ β§ π’ β π β§ π£ β π)) β ((π Β· π’) + π£) β π) |
30 | 1, 2, 3, 4, 5, 7, 9, 11, 29, 14, 15, 16, 17, 18, 19 | lshpkrlem3 37620 |
. 2
β’ ((π β§ (π β πΎ β§ π’ β π β§ π£ β π)) β βπ§ β π ((π Β· π’) + π£) = (π§ + ((πΊβ((π Β· π’) + π£)) Β· π))) |
31 | | 3reeanv 3217 |
. . 3
β’
(βπ β
π βπ β π βπ§ β π (π’ = (π + ((πΊβπ’) Β· π)) β§ π£ = (π + ((πΊβπ£) Β· π)) β§ ((π Β· π’) + π£) = (π§ + ((πΊβ((π Β· π’) + π£)) Β· π))) β (βπ β π π’ = (π + ((πΊβπ’) Β· π)) β§ βπ β π π£ = (π + ((πΊβπ£) Β· π)) β§ βπ§ β π ((π Β· π’) + π£) = (π§ + ((πΊβ((π Β· π’) + π£)) Β· π)))) |
32 | | simp1l 1198 |
. . . . . . . 8
β’ (((π β§ (π β πΎ β§ π’ β π β§ π£ β π)) β§ ((π β π β§ π β π) β§ π§ β π) β§ (π’ = (π + ((πΊβπ’) Β· π)) β§ π£ = (π + ((πΊβπ£) Β· π)) β§ ((π Β· π’) + π£) = (π§ + ((πΊβ((π Β· π’) + π£)) Β· π)))) β π) |
33 | | simp1r1 1270 |
. . . . . . . 8
β’ (((π β§ (π β πΎ β§ π’ β π β§ π£ β π)) β§ ((π β π β§ π β π) β§ π§ β π) β§ (π’ = (π + ((πΊβπ’) Β· π)) β§ π£ = (π + ((πΊβπ£) Β· π)) β§ ((π Β· π’) + π£) = (π§ + ((πΊβ((π Β· π’) + π£)) Β· π)))) β π β πΎ) |
34 | | simp1r2 1271 |
. . . . . . . 8
β’ (((π β§ (π β πΎ β§ π’ β π β§ π£ β π)) β§ ((π β π β§ π β π) β§ π§ β π) β§ (π’ = (π + ((πΊβπ’) Β· π)) β§ π£ = (π + ((πΊβπ£) Β· π)) β§ ((π Β· π’) + π£) = (π§ + ((πΊβ((π Β· π’) + π£)) Β· π)))) β π’ β π) |
35 | | simp1r3 1272 |
. . . . . . . 8
β’ (((π β§ (π β πΎ β§ π’ β π β§ π£ β π)) β§ ((π β π β§ π β π) β§ π§ β π) β§ (π’ = (π + ((πΊβπ’) Β· π)) β§ π£ = (π + ((πΊβπ£) Β· π)) β§ ((π Β· π’) + π£) = (π§ + ((πΊβ((π Β· π’) + π£)) Β· π)))) β π£ β π) |
36 | | simp2ll 1241 |
. . . . . . . 8
β’ (((π β§ (π β πΎ β§ π’ β π β§ π£ β π)) β§ ((π β π β§ π β π) β§ π§ β π) β§ (π’ = (π + ((πΊβπ’) Β· π)) β§ π£ = (π + ((πΊβπ£) Β· π)) β§ ((π Β· π’) + π£) = (π§ + ((πΊβ((π Β· π’) + π£)) Β· π)))) β π β π) |
37 | | simp2lr 1242 |
. . . . . . . . 9
β’ (((π β§ (π β πΎ β§ π’ β π β§ π£ β π)) β§ ((π β π β§ π β π) β§ π§ β π) β§ (π’ = (π + ((πΊβπ’) Β· π)) β§ π£ = (π + ((πΊβπ£) Β· π)) β§ ((π Β· π’) + π£) = (π§ + ((πΊβ((π Β· π’) + π£)) Β· π)))) β π β π) |
38 | | simp2r 1201 |
. . . . . . . . 9
β’ (((π β§ (π β πΎ β§ π’ β π β§ π£ β π)) β§ ((π β π β§ π β π) β§ π§ β π) β§ (π’ = (π + ((πΊβπ’) Β· π)) β§ π£ = (π + ((πΊβπ£) Β· π)) β§ ((π Β· π’) + π£) = (π§ + ((πΊβ((π Β· π’) + π£)) Β· π)))) β π§ β π) |
39 | 37, 38 | jca 513 |
. . . . . . . 8
β’ (((π β§ (π β πΎ β§ π’ β π β§ π£ β π)) β§ ((π β π β§ π β π) β§ π§ β π) β§ (π’ = (π + ((πΊβπ’) Β· π)) β§ π£ = (π + ((πΊβπ£) Β· π)) β§ ((π Β· π’) + π£) = (π§ + ((πΊβ((π Β· π’) + π£)) Β· π)))) β (π β π β§ π§ β π)) |
40 | | simp31 1210 |
. . . . . . . 8
β’ (((π β§ (π β πΎ β§ π’ β π β§ π£ β π)) β§ ((π β π β§ π β π) β§ π§ β π) β§ (π’ = (π + ((πΊβπ’) Β· π)) β§ π£ = (π + ((πΊβπ£) Β· π)) β§ ((π Β· π’) + π£) = (π§ + ((πΊβ((π Β· π’) + π£)) Β· π)))) β π’ = (π + ((πΊβπ’) Β· π))) |
41 | | simp32 1211 |
. . . . . . . 8
β’ (((π β§ (π β πΎ β§ π’ β π β§ π£ β π)) β§ ((π β π β§ π β π) β§ π§ β π) β§ (π’ = (π + ((πΊβπ’) Β· π)) β§ π£ = (π + ((πΊβπ£) Β· π)) β§ ((π Β· π’) + π£) = (π§ + ((πΊβ((π Β· π’) + π£)) Β· π)))) β π£ = (π + ((πΊβπ£) Β· π))) |
42 | | simp33 1212 |
. . . . . . . 8
β’ (((π β§ (π β πΎ β§ π’ β π β§ π£ β π)) β§ ((π β π β§ π β π) β§ π§ β π) β§ (π’ = (π + ((πΊβπ’) Β· π)) β§ π£ = (π + ((πΊβπ£) Β· π)) β§ ((π Β· π’) + π£) = (π§ + ((πΊβ((π Β· π’) + π£)) Β· π)))) β ((π Β· π’) + π£) = (π§ + ((πΊβ((π Β· π’) + π£)) Β· π))) |
43 | 1, 2, 3, 4, 5, 6, 8, 10, 10, 13, 15, 16, 17, 18, 19 | lshpkrlem5 37622 |
. . . . . . . 8
β’ (((π β§ π β πΎ β§ π’ β π) β§ (π£ β π β§ π β π β§ (π β π β§ π§ β π)) β§ (π’ = (π + ((πΊβπ’) Β· π)) β§ π£ = (π + ((πΊβπ£) Β· π)) β§ ((π Β· π’) + π£) = (π§ + ((πΊβ((π Β· π’) + π£)) Β· π)))) β (πΊβ((π Β· π’) + π£)) = ((π(.rβπ·)(πΊβπ’))(+gβπ·)(πΊβπ£))) |
44 | 32, 33, 34, 35, 36, 39, 40, 41, 42, 43 | syl333anc 1403 |
. . . . . . 7
β’ (((π β§ (π β πΎ β§ π’ β π β§ π£ β π)) β§ ((π β π β§ π β π) β§ π§ β π) β§ (π’ = (π + ((πΊβπ’) Β· π)) β§ π£ = (π + ((πΊβπ£) Β· π)) β§ ((π Β· π’) + π£) = (π§ + ((πΊβ((π Β· π’) + π£)) Β· π)))) β (πΊβ((π Β· π’) + π£)) = ((π(.rβπ·)(πΊβπ’))(+gβπ·)(πΊβπ£))) |
45 | 44 | 3exp 1120 |
. . . . . 6
β’ ((π β§ (π β πΎ β§ π’ β π β§ π£ β π)) β (((π β π β§ π β π) β§ π§ β π) β ((π’ = (π + ((πΊβπ’) Β· π)) β§ π£ = (π + ((πΊβπ£) Β· π)) β§ ((π Β· π’) + π£) = (π§ + ((πΊβ((π Β· π’) + π£)) Β· π))) β (πΊβ((π Β· π’) + π£)) = ((π(.rβπ·)(πΊβπ’))(+gβπ·)(πΊβπ£))))) |
46 | 45 | expdimp 454 |
. . . . 5
β’ (((π β§ (π β πΎ β§ π’ β π β§ π£ β π)) β§ (π β π β§ π β π)) β (π§ β π β ((π’ = (π + ((πΊβπ’) Β· π)) β§ π£ = (π + ((πΊβπ£) Β· π)) β§ ((π Β· π’) + π£) = (π§ + ((πΊβ((π Β· π’) + π£)) Β· π))) β (πΊβ((π Β· π’) + π£)) = ((π(.rβπ·)(πΊβπ’))(+gβπ·)(πΊβπ£))))) |
47 | 46 | rexlimdv 3147 |
. . . 4
β’ (((π β§ (π β πΎ β§ π’ β π β§ π£ β π)) β§ (π β π β§ π β π)) β (βπ§ β π (π’ = (π + ((πΊβπ’) Β· π)) β§ π£ = (π + ((πΊβπ£) Β· π)) β§ ((π Β· π’) + π£) = (π§ + ((πΊβ((π Β· π’) + π£)) Β· π))) β (πΊβ((π Β· π’) + π£)) = ((π(.rβπ·)(πΊβπ’))(+gβπ·)(πΊβπ£)))) |
48 | 47 | rexlimdvva 3202 |
. . 3
β’ ((π β§ (π β πΎ β§ π’ β π β§ π£ β π)) β (βπ β π βπ β π βπ§ β π (π’ = (π + ((πΊβπ’) Β· π)) β§ π£ = (π + ((πΊβπ£) Β· π)) β§ ((π Β· π’) + π£) = (π§ + ((πΊβ((π Β· π’) + π£)) Β· π))) β (πΊβ((π Β· π’) + π£)) = ((π(.rβπ·)(πΊβπ’))(+gβπ·)(πΊβπ£)))) |
49 | 31, 48 | biimtrrid 242 |
. 2
β’ ((π β§ (π β πΎ β§ π’ β π β§ π£ β π)) β ((βπ β π π’ = (π + ((πΊβπ’) Β· π)) β§ βπ β π π£ = (π + ((πΊβπ£) Β· π)) β§ βπ§ β π ((π Β· π’) + π£) = (π§ + ((πΊβ((π Β· π’) + π£)) Β· π))) β (πΊβ((π Β· π’) + π£)) = ((π(.rβπ·)(πΊβπ’))(+gβπ·)(πΊβπ£)))) |
50 | 20, 22, 30, 49 | mp3and 1465 |
1
β’ ((π β§ (π β πΎ β§ π’ β π β§ π£ β π)) β (πΊβ((π Β· π’) + π£)) = ((π(.rβπ·)(πΊβπ’))(+gβπ·)(πΊβπ£))) |