Step | Hyp | Ref
| Expression |
1 | | lss1d.f |
. . 3
β’ πΉ = (Scalarβπ) |
2 | 1 | a1i 11 |
. 2
β’ ((π β LMod β§ π β π) β πΉ = (Scalarβπ)) |
3 | | lss1d.k |
. . 3
β’ πΎ = (BaseβπΉ) |
4 | 3 | a1i 11 |
. 2
β’ ((π β LMod β§ π β π) β πΎ = (BaseβπΉ)) |
5 | | lss1d.v |
. . 3
β’ π = (Baseβπ) |
6 | 5 | a1i 11 |
. 2
β’ ((π β LMod β§ π β π) β π = (Baseβπ)) |
7 | | eqidd 2734 |
. 2
β’ ((π β LMod β§ π β π) β (+gβπ) = (+gβπ)) |
8 | | lss1d.t |
. . 3
β’ Β· = (
Β·π βπ) |
9 | 8 | a1i 11 |
. 2
β’ ((π β LMod β§ π β π) β Β· = (
Β·π βπ)) |
10 | | lss1d.s |
. . 3
β’ π = (LSubSpβπ) |
11 | 10 | a1i 11 |
. 2
β’ ((π β LMod β§ π β π) β π = (LSubSpβπ)) |
12 | 5, 1, 8, 3 | lmodvscl 20354 |
. . . . . . 7
β’ ((π β LMod β§ π β πΎ β§ π β π) β (π Β· π) β π) |
13 | 12 | 3expa 1119 |
. . . . . 6
β’ (((π β LMod β§ π β πΎ) β§ π β π) β (π Β· π) β π) |
14 | 13 | an32s 651 |
. . . . 5
β’ (((π β LMod β§ π β π) β§ π β πΎ) β (π Β· π) β π) |
15 | | eleq1a 2829 |
. . . . 5
β’ ((π Β· π) β π β (π£ = (π Β· π) β π£ β π)) |
16 | 14, 15 | syl 17 |
. . . 4
β’ (((π β LMod β§ π β π) β§ π β πΎ) β (π£ = (π Β· π) β π£ β π)) |
17 | 16 | rexlimdva 3149 |
. . 3
β’ ((π β LMod β§ π β π) β (βπ β πΎ π£ = (π Β· π) β π£ β π)) |
18 | 17 | abssdv 4026 |
. 2
β’ ((π β LMod β§ π β π) β {π£ β£ βπ β πΎ π£ = (π Β· π)} β π) |
19 | | eqid 2733 |
. . . . 5
β’
(0gβπΉ) = (0gβπΉ) |
20 | 1, 3, 19 | lmod0cl 20363 |
. . . 4
β’ (π β LMod β
(0gβπΉ)
β πΎ) |
21 | 20 | adantr 482 |
. . 3
β’ ((π β LMod β§ π β π) β (0gβπΉ) β πΎ) |
22 | | nfcv 2904 |
. . . 4
β’
β²π(0gβπΉ) |
23 | | nfre1 3267 |
. . . . . 6
β’
β²πβπ β πΎ π£ = (π Β· π) |
24 | 23 | nfab 2910 |
. . . . 5
β’
β²π{π£ β£ βπ β πΎ π£ = (π Β· π)} |
25 | | nfcv 2904 |
. . . . 5
β’
β²πβ
|
26 | 24, 25 | nfne 3042 |
. . . 4
β’
β²π{π£ β£ βπ β πΎ π£ = (π Β· π)} β β
|
27 | | biidd 262 |
. . . 4
β’ (π = (0gβπΉ) β ({π£ β£ βπ β πΎ π£ = (π Β· π)} β β
β {π£ β£ βπ β πΎ π£ = (π Β· π)} β β
)) |
28 | | ovex 7391 |
. . . . . 6
β’ (π Β· π) β V |
29 | 28 | elabrex 7191 |
. . . . 5
β’ (π β πΎ β (π Β· π) β {π£ β£ βπ β πΎ π£ = (π Β· π)}) |
30 | 29 | ne0d 4296 |
. . . 4
β’ (π β πΎ β {π£ β£ βπ β πΎ π£ = (π Β· π)} β β
) |
31 | 22, 26, 27, 30 | vtoclgaf 3532 |
. . 3
β’
((0gβπΉ) β πΎ β {π£ β£ βπ β πΎ π£ = (π Β· π)} β β
) |
32 | 21, 31 | syl 17 |
. 2
β’ ((π β LMod β§ π β π) β {π£ β£ βπ β πΎ π£ = (π Β· π)} β β
) |
33 | | vex 3448 |
. . . . . . . . . . 11
β’ π β V |
34 | | eqeq1 2737 |
. . . . . . . . . . . 12
β’ (π£ = π β (π£ = (π Β· π) β π = (π Β· π))) |
35 | 34 | rexbidv 3172 |
. . . . . . . . . . 11
β’ (π£ = π β (βπ β πΎ π£ = (π Β· π) β βπ β πΎ π = (π Β· π))) |
36 | 33, 35 | elab 3631 |
. . . . . . . . . 10
β’ (π β {π£ β£ βπ β πΎ π£ = (π Β· π)} β βπ β πΎ π = (π Β· π)) |
37 | | oveq1 7365 |
. . . . . . . . . . . 12
β’ (π = π¦ β (π Β· π) = (π¦ Β· π)) |
38 | 37 | eqeq2d 2744 |
. . . . . . . . . . 11
β’ (π = π¦ β (π = (π Β· π) β π = (π¦ Β· π))) |
39 | 38 | cbvrexvw 3225 |
. . . . . . . . . 10
β’
(βπ β
πΎ π = (π Β· π) β βπ¦ β πΎ π = (π¦ Β· π)) |
40 | 36, 39 | bitri 275 |
. . . . . . . . 9
β’ (π β {π£ β£ βπ β πΎ π£ = (π Β· π)} β βπ¦ β πΎ π = (π¦ Β· π)) |
41 | | vex 3448 |
. . . . . . . . . . 11
β’ π β V |
42 | | eqeq1 2737 |
. . . . . . . . . . . 12
β’ (π£ = π β (π£ = (π Β· π) β π = (π Β· π))) |
43 | 42 | rexbidv 3172 |
. . . . . . . . . . 11
β’ (π£ = π β (βπ β πΎ π£ = (π Β· π) β βπ β πΎ π = (π Β· π))) |
44 | 41, 43 | elab 3631 |
. . . . . . . . . 10
β’ (π β {π£ β£ βπ β πΎ π£ = (π Β· π)} β βπ β πΎ π = (π Β· π)) |
45 | | oveq1 7365 |
. . . . . . . . . . . 12
β’ (π = π§ β (π Β· π) = (π§ Β· π)) |
46 | 45 | eqeq2d 2744 |
. . . . . . . . . . 11
β’ (π = π§ β (π = (π Β· π) β π = (π§ Β· π))) |
47 | 46 | cbvrexvw 3225 |
. . . . . . . . . 10
β’
(βπ β
πΎ π = (π Β· π) β βπ§ β πΎ π = (π§ Β· π)) |
48 | 44, 47 | bitri 275 |
. . . . . . . . 9
β’ (π β {π£ β£ βπ β πΎ π£ = (π Β· π)} β βπ§ β πΎ π = (π§ Β· π)) |
49 | 40, 48 | anbi12i 628 |
. . . . . . . 8
β’ ((π β {π£ β£ βπ β πΎ π£ = (π Β· π)} β§ π β {π£ β£ βπ β πΎ π£ = (π Β· π)}) β (βπ¦ β πΎ π = (π¦ Β· π) β§ βπ§ β πΎ π = (π§ Β· π))) |
50 | | reeanv 3216 |
. . . . . . . 8
β’
(βπ¦ β
πΎ βπ§ β πΎ (π = (π¦ Β· π) β§ π = (π§ Β· π)) β (βπ¦ β πΎ π = (π¦ Β· π) β§ βπ§ β πΎ π = (π§ Β· π))) |
51 | 49, 50 | bitr4i 278 |
. . . . . . 7
β’ ((π β {π£ β£ βπ β πΎ π£ = (π Β· π)} β§ π β {π£ β£ βπ β πΎ π£ = (π Β· π)}) β βπ¦ β πΎ βπ§ β πΎ (π = (π¦ Β· π) β§ π = (π§ Β· π))) |
52 | | simpll 766 |
. . . . . . . . . . . . 13
β’ (((π β LMod β§ π β π) β§ ((π¦ β πΎ β§ π§ β πΎ) β§ π₯ β πΎ)) β π β LMod) |
53 | | simprr 772 |
. . . . . . . . . . . . . 14
β’ (((π β LMod β§ π β π) β§ ((π¦ β πΎ β§ π§ β πΎ) β§ π₯ β πΎ)) β π₯ β πΎ) |
54 | | simprll 778 |
. . . . . . . . . . . . . 14
β’ (((π β LMod β§ π β π) β§ ((π¦ β πΎ β§ π§ β πΎ) β§ π₯ β πΎ)) β π¦ β πΎ) |
55 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’
(.rβπΉ) = (.rβπΉ) |
56 | 1, 3, 55 | lmodmcl 20349 |
. . . . . . . . . . . . . 14
β’ ((π β LMod β§ π₯ β πΎ β§ π¦ β πΎ) β (π₯(.rβπΉ)π¦) β πΎ) |
57 | 52, 53, 54, 56 | syl3anc 1372 |
. . . . . . . . . . . . 13
β’ (((π β LMod β§ π β π) β§ ((π¦ β πΎ β§ π§ β πΎ) β§ π₯ β πΎ)) β (π₯(.rβπΉ)π¦) β πΎ) |
58 | | simprlr 779 |
. . . . . . . . . . . . 13
β’ (((π β LMod β§ π β π) β§ ((π¦ β πΎ β§ π§ β πΎ) β§ π₯ β πΎ)) β π§ β πΎ) |
59 | | eqid 2733 |
. . . . . . . . . . . . . 14
β’
(+gβπΉ) = (+gβπΉ) |
60 | 1, 3, 59 | lmodacl 20348 |
. . . . . . . . . . . . 13
β’ ((π β LMod β§ (π₯(.rβπΉ)π¦) β πΎ β§ π§ β πΎ) β ((π₯(.rβπΉ)π¦)(+gβπΉ)π§) β πΎ) |
61 | 52, 57, 58, 60 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ (((π β LMod β§ π β π) β§ ((π¦ β πΎ β§ π§ β πΎ) β§ π₯ β πΎ)) β ((π₯(.rβπΉ)π¦)(+gβπΉ)π§) β πΎ) |
62 | | simplr 768 |
. . . . . . . . . . . . . 14
β’ (((π β LMod β§ π β π) β§ ((π¦ β πΎ β§ π§ β πΎ) β§ π₯ β πΎ)) β π β π) |
63 | | eqid 2733 |
. . . . . . . . . . . . . . 15
β’
(+gβπ) = (+gβπ) |
64 | 5, 63, 1, 8, 3, 59 | lmodvsdir 20361 |
. . . . . . . . . . . . . 14
β’ ((π β LMod β§ ((π₯(.rβπΉ)π¦) β πΎ β§ π§ β πΎ β§ π β π)) β (((π₯(.rβπΉ)π¦)(+gβπΉ)π§) Β· π) = (((π₯(.rβπΉ)π¦) Β· π)(+gβπ)(π§ Β· π))) |
65 | 52, 57, 58, 62, 64 | syl13anc 1373 |
. . . . . . . . . . . . 13
β’ (((π β LMod β§ π β π) β§ ((π¦ β πΎ β§ π§ β πΎ) β§ π₯ β πΎ)) β (((π₯(.rβπΉ)π¦)(+gβπΉ)π§) Β· π) = (((π₯(.rβπΉ)π¦) Β· π)(+gβπ)(π§ Β· π))) |
66 | 5, 1, 8, 3, 55 | lmodvsass 20362 |
. . . . . . . . . . . . . . 15
β’ ((π β LMod β§ (π₯ β πΎ β§ π¦ β πΎ β§ π β π)) β ((π₯(.rβπΉ)π¦) Β· π) = (π₯ Β· (π¦ Β· π))) |
67 | 52, 53, 54, 62, 66 | syl13anc 1373 |
. . . . . . . . . . . . . 14
β’ (((π β LMod β§ π β π) β§ ((π¦ β πΎ β§ π§ β πΎ) β§ π₯ β πΎ)) β ((π₯(.rβπΉ)π¦) Β· π) = (π₯ Β· (π¦ Β· π))) |
68 | 67 | oveq1d 7373 |
. . . . . . . . . . . . 13
β’ (((π β LMod β§ π β π) β§ ((π¦ β πΎ β§ π§ β πΎ) β§ π₯ β πΎ)) β (((π₯(.rβπΉ)π¦) Β· π)(+gβπ)(π§ Β· π)) = ((π₯ Β· (π¦ Β· π))(+gβπ)(π§ Β· π))) |
69 | 65, 68 | eqtr2d 2774 |
. . . . . . . . . . . 12
β’ (((π β LMod β§ π β π) β§ ((π¦ β πΎ β§ π§ β πΎ) β§ π₯ β πΎ)) β ((π₯ Β· (π¦ Β· π))(+gβπ)(π§ Β· π)) = (((π₯(.rβπΉ)π¦)(+gβπΉ)π§) Β· π)) |
70 | | oveq1 7365 |
. . . . . . . . . . . . 13
β’ (π = ((π₯(.rβπΉ)π¦)(+gβπΉ)π§) β (π Β· π) = (((π₯(.rβπΉ)π¦)(+gβπΉ)π§) Β· π)) |
71 | 70 | rspceeqv 3596 |
. . . . . . . . . . . 12
β’ ((((π₯(.rβπΉ)π¦)(+gβπΉ)π§) β πΎ β§ ((π₯ Β· (π¦ Β· π))(+gβπ)(π§ Β· π)) = (((π₯(.rβπΉ)π¦)(+gβπΉ)π§) Β· π)) β βπ β πΎ ((π₯ Β· (π¦ Β· π))(+gβπ)(π§ Β· π)) = (π Β· π)) |
72 | 61, 69, 71 | syl2anc 585 |
. . . . . . . . . . 11
β’ (((π β LMod β§ π β π) β§ ((π¦ β πΎ β§ π§ β πΎ) β§ π₯ β πΎ)) β βπ β πΎ ((π₯ Β· (π¦ Β· π))(+gβπ)(π§ Β· π)) = (π Β· π)) |
73 | | oveq2 7366 |
. . . . . . . . . . . . . 14
β’ (π = (π¦ Β· π) β (π₯ Β· π) = (π₯ Β· (π¦ Β· π))) |
74 | | oveq12 7367 |
. . . . . . . . . . . . . 14
β’ (((π₯ Β· π) = (π₯ Β· (π¦ Β· π)) β§ π = (π§ Β· π)) β ((π₯ Β· π)(+gβπ)π) = ((π₯ Β· (π¦ Β· π))(+gβπ)(π§ Β· π))) |
75 | 73, 74 | sylan 581 |
. . . . . . . . . . . . 13
β’ ((π = (π¦ Β· π) β§ π = (π§ Β· π)) β ((π₯ Β· π)(+gβπ)π) = ((π₯ Β· (π¦ Β· π))(+gβπ)(π§ Β· π))) |
76 | 75 | eqeq1d 2735 |
. . . . . . . . . . . 12
β’ ((π = (π¦ Β· π) β§ π = (π§ Β· π)) β (((π₯ Β· π)(+gβπ)π) = (π Β· π) β ((π₯ Β· (π¦ Β· π))(+gβπ)(π§ Β· π)) = (π Β· π))) |
77 | 76 | rexbidv 3172 |
. . . . . . . . . . 11
β’ ((π = (π¦ Β· π) β§ π = (π§ Β· π)) β (βπ β πΎ ((π₯ Β· π)(+gβπ)π) = (π Β· π) β βπ β πΎ ((π₯ Β· (π¦ Β· π))(+gβπ)(π§ Β· π)) = (π Β· π))) |
78 | 72, 77 | syl5ibrcom 247 |
. . . . . . . . . 10
β’ (((π β LMod β§ π β π) β§ ((π¦ β πΎ β§ π§ β πΎ) β§ π₯ β πΎ)) β ((π = (π¦ Β· π) β§ π = (π§ Β· π)) β βπ β πΎ ((π₯ Β· π)(+gβπ)π) = (π Β· π))) |
79 | 78 | expr 458 |
. . . . . . . . 9
β’ (((π β LMod β§ π β π) β§ (π¦ β πΎ β§ π§ β πΎ)) β (π₯ β πΎ β ((π = (π¦ Β· π) β§ π = (π§ Β· π)) β βπ β πΎ ((π₯ Β· π)(+gβπ)π) = (π Β· π)))) |
80 | 79 | com23 86 |
. . . . . . . 8
β’ (((π β LMod β§ π β π) β§ (π¦ β πΎ β§ π§ β πΎ)) β ((π = (π¦ Β· π) β§ π = (π§ Β· π)) β (π₯ β πΎ β βπ β πΎ ((π₯ Β· π)(+gβπ)π) = (π Β· π)))) |
81 | 80 | rexlimdvva 3202 |
. . . . . . 7
β’ ((π β LMod β§ π β π) β (βπ¦ β πΎ βπ§ β πΎ (π = (π¦ Β· π) β§ π = (π§ Β· π)) β (π₯ β πΎ β βπ β πΎ ((π₯ Β· π)(+gβπ)π) = (π Β· π)))) |
82 | 51, 81 | biimtrid 241 |
. . . . . 6
β’ ((π β LMod β§ π β π) β ((π β {π£ β£ βπ β πΎ π£ = (π Β· π)} β§ π β {π£ β£ βπ β πΎ π£ = (π Β· π)}) β (π₯ β πΎ β βπ β πΎ ((π₯ Β· π)(+gβπ)π) = (π Β· π)))) |
83 | 82 | expcomd 418 |
. . . . 5
β’ ((π β LMod β§ π β π) β (π β {π£ β£ βπ β πΎ π£ = (π Β· π)} β (π β {π£ β£ βπ β πΎ π£ = (π Β· π)} β (π₯ β πΎ β βπ β πΎ ((π₯ Β· π)(+gβπ)π) = (π Β· π))))) |
84 | 83 | com24 95 |
. . . 4
β’ ((π β LMod β§ π β π) β (π₯ β πΎ β (π β {π£ β£ βπ β πΎ π£ = (π Β· π)} β (π β {π£ β£ βπ β πΎ π£ = (π Β· π)} β βπ β πΎ ((π₯ Β· π)(+gβπ)π) = (π Β· π))))) |
85 | 84 | 3imp2 1350 |
. . 3
β’ (((π β LMod β§ π β π) β§ (π₯ β πΎ β§ π β {π£ β£ βπ β πΎ π£ = (π Β· π)} β§ π β {π£ β£ βπ β πΎ π£ = (π Β· π)})) β βπ β πΎ ((π₯ Β· π)(+gβπ)π) = (π Β· π)) |
86 | | ovex 7391 |
. . . 4
β’ ((π₯ Β· π)(+gβπ)π) β V |
87 | | eqeq1 2737 |
. . . . 5
β’ (π£ = ((π₯ Β· π)(+gβπ)π) β (π£ = (π Β· π) β ((π₯ Β· π)(+gβπ)π) = (π Β· π))) |
88 | 87 | rexbidv 3172 |
. . . 4
β’ (π£ = ((π₯ Β· π)(+gβπ)π) β (βπ β πΎ π£ = (π Β· π) β βπ β πΎ ((π₯ Β· π)(+gβπ)π) = (π Β· π))) |
89 | 86, 88 | elab 3631 |
. . 3
β’ (((π₯ Β· π)(+gβπ)π) β {π£ β£ βπ β πΎ π£ = (π Β· π)} β βπ β πΎ ((π₯ Β· π)(+gβπ)π) = (π Β· π)) |
90 | 85, 89 | sylibr 233 |
. 2
β’ (((π β LMod β§ π β π) β§ (π₯ β πΎ β§ π β {π£ β£ βπ β πΎ π£ = (π Β· π)} β§ π β {π£ β£ βπ β πΎ π£ = (π Β· π)})) β ((π₯ Β· π)(+gβπ)π) β {π£ β£ βπ β πΎ π£ = (π Β· π)}) |
91 | 2, 4, 6, 7, 9, 11,
18, 32, 90 | islssd 20411 |
1
β’ ((π β LMod β§ π β π) β {π£ β£ βπ β πΎ π£ = (π Β· π)} β π) |