Step | Hyp | Ref
| Expression |
1 | | simpllr 774 |
. . . 4
β’ ((((π β LVec β§ π βΌ π) β§ π β πΎ) β§ π = (π Β· π)) β π βΌ π) |
2 | | prjsprel.1 |
. . . . . 6
β’ βΌ =
{β¨π₯, π¦β© β£ ((π₯ β π΅ β§ π¦ β π΅) β§ βπ β πΎ π₯ = (π Β· π¦))} |
3 | 2 | prjsprel 41033 |
. . . . 5
β’ (π βΌ π β ((π β π΅ β§ π β π΅) β§ βπ β πΎ π = (π Β· π))) |
4 | | pm3.22 460 |
. . . . . 6
β’ ((π β π΅ β§ π β π΅) β (π β π΅ β§ π β π΅)) |
5 | 4 | adantr 481 |
. . . . 5
β’ (((π β π΅ β§ π β π΅) β§ βπ β πΎ π = (π Β· π)) β (π β π΅ β§ π β π΅)) |
6 | 3, 5 | sylbi 216 |
. . . 4
β’ (π βΌ π β (π β π΅ β§ π β π΅)) |
7 | 1, 6 | syl 17 |
. . 3
β’ ((((π β LVec β§ π βΌ π) β§ π β πΎ) β§ π = (π Β· π)) β (π β π΅ β§ π β π΅)) |
8 | | simplll 773 |
. . . . . 6
β’ ((((π β LVec β§ π βΌ π) β§ π β πΎ) β§ π = (π Β· π)) β π β LVec) |
9 | | prjspertr.s |
. . . . . . 7
β’ π = (Scalarβπ) |
10 | 9 | lvecdrng 20638 |
. . . . . 6
β’ (π β LVec β π β
DivRing) |
11 | 8, 10 | syl 17 |
. . . . 5
β’ ((((π β LVec β§ π βΌ π) β§ π β πΎ) β§ π = (π Β· π)) β π β DivRing) |
12 | | simplr 767 |
. . . . 5
β’ ((((π β LVec β§ π βΌ π) β§ π β πΎ) β§ π = (π Β· π)) β π β πΎ) |
13 | | simpll 765 |
. . . . . . . 8
β’ (((π β π΅ β§ π β π΅) β§ βπ β πΎ π = (π Β· π)) β π β π΅) |
14 | 3, 13 | sylbi 216 |
. . . . . . 7
β’ (π βΌ π β π β π΅) |
15 | | eldifsni 4770 |
. . . . . . . 8
β’ (π β ((Baseβπ) β
{(0gβπ)})
β π β
(0gβπ)) |
16 | | prjspertr.b |
. . . . . . . 8
β’ π΅ = ((Baseβπ) β
{(0gβπ)}) |
17 | 15, 16 | eleq2s 2850 |
. . . . . . 7
β’ (π β π΅ β π β (0gβπ)) |
18 | 1, 14, 17 | 3syl 18 |
. . . . . 6
β’ ((((π β LVec β§ π βΌ π) β§ π β πΎ) β§ π = (π Β· π)) β π β (0gβπ)) |
19 | | simplr 767 |
. . . . . . 7
β’
(((((π β LVec
β§ π βΌ π) β§ π β πΎ) β§ π = (π Β· π)) β§ π = (0gβπ)) β π = (π Β· π)) |
20 | | simpr 485 |
. . . . . . . 8
β’
(((((π β LVec
β§ π βΌ π) β§ π β πΎ) β§ π = (π Β· π)) β§ π = (0gβπ)) β π = (0gβπ)) |
21 | 20 | oveq1d 7392 |
. . . . . . 7
β’
(((((π β LVec
β§ π βΌ π) β§ π β πΎ) β§ π = (π Β· π)) β§ π = (0gβπ)) β (π Β· π) = ((0gβπ) Β· π)) |
22 | | lveclmod 20639 |
. . . . . . . . 9
β’ (π β LVec β π β LMod) |
23 | 22 | ad4antr 730 |
. . . . . . . 8
β’
(((((π β LVec
β§ π βΌ π) β§ π β πΎ) β§ π = (π Β· π)) β§ π = (0gβπ)) β π β LMod) |
24 | | simplr 767 |
. . . . . . . . . . 11
β’ (((π β π΅ β§ π β π΅) β§ βπ β πΎ π = (π Β· π)) β π β π΅) |
25 | 3, 24 | sylbi 216 |
. . . . . . . . . 10
β’ (π βΌ π β π β π΅) |
26 | | eldifi 4106 |
. . . . . . . . . . 11
β’ (π β ((Baseβπ) β
{(0gβπ)})
β π β
(Baseβπ)) |
27 | 26, 16 | eleq2s 2850 |
. . . . . . . . . 10
β’ (π β π΅ β π β (Baseβπ)) |
28 | 1, 25, 27 | 3syl 18 |
. . . . . . . . 9
β’ ((((π β LVec β§ π βΌ π) β§ π β πΎ) β§ π = (π Β· π)) β π β (Baseβπ)) |
29 | 28 | adantr 481 |
. . . . . . . 8
β’
(((((π β LVec
β§ π βΌ π) β§ π β πΎ) β§ π = (π Β· π)) β§ π = (0gβπ)) β π β (Baseβπ)) |
30 | | eqid 2731 |
. . . . . . . . 9
β’
(Baseβπ) =
(Baseβπ) |
31 | | prjspertr.x |
. . . . . . . . 9
β’ Β· = (
Β·π βπ) |
32 | | eqid 2731 |
. . . . . . . . 9
β’
(0gβπ) = (0gβπ) |
33 | | eqid 2731 |
. . . . . . . . 9
β’
(0gβπ) = (0gβπ) |
34 | 30, 9, 31, 32, 33 | lmod0vs 20427 |
. . . . . . . 8
β’ ((π β LMod β§ π β (Baseβπ)) β
((0gβπ)
Β·
π) =
(0gβπ)) |
35 | 23, 29, 34 | syl2anc 584 |
. . . . . . 7
β’
(((((π β LVec
β§ π βΌ π) β§ π β πΎ) β§ π = (π Β· π)) β§ π = (0gβπ)) β ((0gβπ) Β· π) = (0gβπ)) |
36 | 19, 21, 35 | 3eqtrd 2775 |
. . . . . 6
β’
(((((π β LVec
β§ π βΌ π) β§ π β πΎ) β§ π = (π Β· π)) β§ π = (0gβπ)) β π = (0gβπ)) |
37 | 18, 36 | mteqand 3032 |
. . . . 5
β’ ((((π β LVec β§ π βΌ π) β§ π β πΎ) β§ π = (π Β· π)) β π β (0gβπ)) |
38 | | prjspertr.k |
. . . . . 6
β’ πΎ = (Baseβπ) |
39 | | eqid 2731 |
. . . . . 6
β’
(invrβπ) = (invrβπ) |
40 | 38, 32, 39 | drnginvrcl 20261 |
. . . . 5
β’ ((π β DivRing β§ π β πΎ β§ π β (0gβπ)) β ((invrβπ)βπ) β πΎ) |
41 | 11, 12, 37, 40 | syl3anc 1371 |
. . . 4
β’ ((((π β LVec β§ π βΌ π) β§ π β πΎ) β§ π = (π Β· π)) β ((invrβπ)βπ) β πΎ) |
42 | | oveq1 7384 |
. . . . . 6
β’ (π = ((invrβπ)βπ) β (π Β· π) = (((invrβπ)βπ) Β· π)) |
43 | 42 | eqeq2d 2742 |
. . . . 5
β’ (π = ((invrβπ)βπ) β (π = (π Β· π) β π = (((invrβπ)βπ) Β· π))) |
44 | 43 | adantl 482 |
. . . 4
β’
(((((π β LVec
β§ π βΌ π) β§ π β πΎ) β§ π = (π Β· π)) β§ π = ((invrβπ)βπ)) β (π = (π Β· π) β π = (((invrβπ)βπ) Β· π))) |
45 | | simpr 485 |
. . . . 5
β’ ((((π β LVec β§ π βΌ π) β§ π β πΎ) β§ π = (π Β· π)) β π = (π Β· π)) |
46 | | nelsn 4646 |
. . . . . . . 8
β’ (π β (0gβπ) β Β¬ π β
{(0gβπ)}) |
47 | 37, 46 | syl 17 |
. . . . . . 7
β’ ((((π β LVec β§ π βΌ π) β§ π β πΎ) β§ π = (π Β· π)) β Β¬ π β {(0gβπ)}) |
48 | 12, 47 | eldifd 3939 |
. . . . . 6
β’ ((((π β LVec β§ π βΌ π) β§ π β πΎ) β§ π = (π Β· π)) β π β (πΎ β {(0gβπ)})) |
49 | | eldifi 4106 |
. . . . . . . 8
β’ (π β ((Baseβπ) β
{(0gβπ)})
β π β
(Baseβπ)) |
50 | 49, 16 | eleq2s 2850 |
. . . . . . 7
β’ (π β π΅ β π β (Baseβπ)) |
51 | 1, 14, 50 | 3syl 18 |
. . . . . 6
β’ ((((π β LVec β§ π βΌ π) β§ π β πΎ) β§ π = (π Β· π)) β π β (Baseβπ)) |
52 | 30, 31, 9, 38, 32, 39, 8, 48, 51, 28 | lvecinv 20648 |
. . . . 5
β’ ((((π β LVec β§ π βΌ π) β§ π β πΎ) β§ π = (π Β· π)) β (π = (π Β· π) β π = (((invrβπ)βπ) Β· π))) |
53 | 45, 52 | mpbid 231 |
. . . 4
β’ ((((π β LVec β§ π βΌ π) β§ π β πΎ) β§ π = (π Β· π)) β π = (((invrβπ)βπ) Β· π)) |
54 | 41, 44, 53 | rspcedvd 3597 |
. . 3
β’ ((((π β LVec β§ π βΌ π) β§ π β πΎ) β§ π = (π Β· π)) β βπ β πΎ π = (π Β· π)) |
55 | 2 | prjsprel 41033 |
. . 3
β’ (π βΌ π β ((π β π΅ β§ π β π΅) β§ βπ β πΎ π = (π Β· π))) |
56 | 7, 54, 55 | sylanbrc 583 |
. 2
β’ ((((π β LVec β§ π βΌ π) β§ π β πΎ) β§ π = (π Β· π)) β π βΌ π) |
57 | | simpr 485 |
. . . 4
β’ (((π β π΅ β§ π β π΅) β§ βπ β πΎ π = (π Β· π)) β βπ β πΎ π = (π Β· π)) |
58 | 3, 57 | sylbi 216 |
. . 3
β’ (π βΌ π β βπ β πΎ π = (π Β· π)) |
59 | 58 | adantl 482 |
. 2
β’ ((π β LVec β§ π βΌ π) β βπ β πΎ π = (π Β· π)) |
60 | 56, 59 | r19.29a 3161 |
1
β’ ((π β LVec β§ π βΌ π) β π βΌ π) |