Step | Hyp | Ref
| Expression |
1 | | lspsneu.v |
. . . . . . 7
β’ π = (Baseβπ) |
2 | | lspsneu.s |
. . . . . . 7
β’ π = (Scalarβπ) |
3 | | lspsneu.k |
. . . . . . 7
β’ πΎ = (Baseβπ) |
4 | | lspsneu.o |
. . . . . . 7
β’ π = (0gβπ) |
5 | | lspsneu.t |
. . . . . . 7
β’ Β· = (
Β·π βπ) |
6 | | lspsneu.n |
. . . . . . 7
β’ π = (LSpanβπ) |
7 | | lspsneu.w |
. . . . . . 7
β’ (π β π β LVec) |
8 | | lspsneu.x |
. . . . . . 7
β’ (π β π β π) |
9 | | lspsneu.y |
. . . . . . . 8
β’ (π β π β (π β { 0 })) |
10 | 9 | eldifad 3923 |
. . . . . . 7
β’ (π β π β π) |
11 | 1, 2, 3, 4, 5, 6, 7, 8, 10 | lspsneq 20586 |
. . . . . 6
β’ (π β ((πβ{π}) = (πβ{π}) β βπ β (πΎ β {π})π = (π Β· π))) |
12 | 11 | biimpd 228 |
. . . . 5
β’ (π β ((πβ{π}) = (πβ{π}) β βπ β (πΎ β {π})π = (π Β· π))) |
13 | | eqtr2 2761 |
. . . . . . . . . 10
β’ ((π = (π Β· π) β§ π = (π Β· π)) β (π Β· π) = (π Β· π)) |
14 | 13 | 3ad2ant3 1136 |
. . . . . . . . 9
β’ (((π β§ (πβ{π}) = (πβ{π})) β§ (π β (πΎ β {π}) β§ π β (πΎ β {π})) β§ (π = (π Β· π) β§ π = (π Β· π))) β (π Β· π) = (π Β· π)) |
15 | | lspsneu.z |
. . . . . . . . . 10
β’ 0 =
(0gβπ) |
16 | | simp1l 1198 |
. . . . . . . . . . 11
β’ (((π β§ (πβ{π}) = (πβ{π})) β§ (π β (πΎ β {π}) β§ π β (πΎ β {π})) β§ (π = (π Β· π) β§ π = (π Β· π))) β π) |
17 | 16, 7 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ (πβ{π}) = (πβ{π})) β§ (π β (πΎ β {π}) β§ π β (πΎ β {π})) β§ (π = (π Β· π) β§ π = (π Β· π))) β π β LVec) |
18 | | simp2l 1200 |
. . . . . . . . . . 11
β’ (((π β§ (πβ{π}) = (πβ{π})) β§ (π β (πΎ β {π}) β§ π β (πΎ β {π})) β§ (π = (π Β· π) β§ π = (π Β· π))) β π β (πΎ β {π})) |
19 | 18 | eldifad 3923 |
. . . . . . . . . 10
β’ (((π β§ (πβ{π}) = (πβ{π})) β§ (π β (πΎ β {π}) β§ π β (πΎ β {π})) β§ (π = (π Β· π) β§ π = (π Β· π))) β π β πΎ) |
20 | | simp2r 1201 |
. . . . . . . . . . 11
β’ (((π β§ (πβ{π}) = (πβ{π})) β§ (π β (πΎ β {π}) β§ π β (πΎ β {π})) β§ (π = (π Β· π) β§ π = (π Β· π))) β π β (πΎ β {π})) |
21 | 20 | eldifad 3923 |
. . . . . . . . . 10
β’ (((π β§ (πβ{π}) = (πβ{π})) β§ (π β (πΎ β {π}) β§ π β (πΎ β {π})) β§ (π = (π Β· π) β§ π = (π Β· π))) β π β πΎ) |
22 | 16, 10 | syl 17 |
. . . . . . . . . 10
β’ (((π β§ (πβ{π}) = (πβ{π})) β§ (π β (πΎ β {π}) β§ π β (πΎ β {π})) β§ (π = (π Β· π) β§ π = (π Β· π))) β π β π) |
23 | | eldifsni 4751 |
. . . . . . . . . . 11
β’ (π β (π β { 0 }) β π β 0 ) |
24 | 16, 9, 23 | 3syl 18 |
. . . . . . . . . 10
β’ (((π β§ (πβ{π}) = (πβ{π})) β§ (π β (πΎ β {π}) β§ π β (πΎ β {π})) β§ (π = (π Β· π) β§ π = (π Β· π))) β π β 0 ) |
25 | 1, 5, 2, 3, 15, 17, 19, 21, 22, 24 | lvecvscan2 20576 |
. . . . . . . . 9
β’ (((π β§ (πβ{π}) = (πβ{π})) β§ (π β (πΎ β {π}) β§ π β (πΎ β {π})) β§ (π = (π Β· π) β§ π = (π Β· π))) β ((π Β· π) = (π Β· π) β π = π)) |
26 | 14, 25 | mpbid 231 |
. . . . . . . 8
β’ (((π β§ (πβ{π}) = (πβ{π})) β§ (π β (πΎ β {π}) β§ π β (πΎ β {π})) β§ (π = (π Β· π) β§ π = (π Β· π))) β π = π) |
27 | 26 | 3exp 1120 |
. . . . . . 7
β’ ((π β§ (πβ{π}) = (πβ{π})) β ((π β (πΎ β {π}) β§ π β (πΎ β {π})) β ((π = (π Β· π) β§ π = (π Β· π)) β π = π))) |
28 | 27 | ex 414 |
. . . . . 6
β’ (π β ((πβ{π}) = (πβ{π}) β ((π β (πΎ β {π}) β§ π β (πΎ β {π})) β ((π = (π Β· π) β§ π = (π Β· π)) β π = π)))) |
29 | 28 | ralrimdvv 3199 |
. . . . 5
β’ (π β ((πβ{π}) = (πβ{π}) β βπ β (πΎ β {π})βπ β (πΎ β {π})((π = (π Β· π) β§ π = (π Β· π)) β π = π))) |
30 | 12, 29 | jcad 514 |
. . . 4
β’ (π β ((πβ{π}) = (πβ{π}) β (βπ β (πΎ β {π})π = (π Β· π) β§ βπ β (πΎ β {π})βπ β (πΎ β {π})((π = (π Β· π) β§ π = (π Β· π)) β π = π)))) |
31 | | oveq1 7365 |
. . . . . 6
β’ (π = π β (π Β· π) = (π Β· π)) |
32 | 31 | eqeq2d 2748 |
. . . . 5
β’ (π = π β (π = (π Β· π) β π = (π Β· π))) |
33 | 32 | reu4 3690 |
. . . 4
β’
(β!π β
(πΎ β {π})π = (π Β· π) β (βπ β (πΎ β {π})π = (π Β· π) β§ βπ β (πΎ β {π})βπ β (πΎ β {π})((π = (π Β· π) β§ π = (π Β· π)) β π = π))) |
34 | 30, 33 | syl6ibr 252 |
. . 3
β’ (π β ((πβ{π}) = (πβ{π}) β β!π β (πΎ β {π})π = (π Β· π))) |
35 | | reurex 3358 |
. . . 4
β’
(β!π β
(πΎ β {π})π = (π Β· π) β βπ β (πΎ β {π})π = (π Β· π)) |
36 | 35, 11 | syl5ibr 246 |
. . 3
β’ (π β (β!π β (πΎ β {π})π = (π Β· π) β (πβ{π}) = (πβ{π}))) |
37 | 34, 36 | impbid 211 |
. 2
β’ (π β ((πβ{π}) = (πβ{π}) β β!π β (πΎ β {π})π = (π Β· π))) |
38 | | oveq1 7365 |
. . . 4
β’ (π = π β (π Β· π) = (π Β· π)) |
39 | 38 | eqeq2d 2748 |
. . 3
β’ (π = π β (π = (π Β· π) β π = (π Β· π))) |
40 | 39 | cbvreuvw 3378 |
. 2
β’
(β!π β
(πΎ β {π})π = (π Β· π) β β!π β (πΎ β {π})π = (π Β· π)) |
41 | 37, 40 | bitrdi 287 |
1
β’ (π β ((πβ{π}) = (πβ{π}) β β!π β (πΎ β {π})π = (π Β· π))) |