Step | Hyp | Ref
| Expression |
1 | | eqlkr3.w |
. . . 4
β’ (π β π β LVec) |
2 | | eqlkr3.g |
. . . 4
β’ (π β πΊ β πΉ) |
3 | | eqlkr3.s |
. . . . 5
β’ π = (Scalarβπ) |
4 | | eqlkr3.r |
. . . . 5
β’ π
= (Baseβπ) |
5 | | eqlkr3.v |
. . . . 5
β’ π = (Baseβπ) |
6 | | eqlkr3.f |
. . . . 5
β’ πΉ = (LFnlβπ) |
7 | 3, 4, 5, 6 | lflf 37575 |
. . . 4
β’ ((π β LVec β§ πΊ β πΉ) β πΊ:πβΆπ
) |
8 | 1, 2, 7 | syl2anc 585 |
. . 3
β’ (π β πΊ:πβΆπ
) |
9 | 8 | ffnd 6673 |
. 2
β’ (π β πΊ Fn π) |
10 | | eqlkr3.h |
. . . 4
β’ (π β π» β πΉ) |
11 | 3, 4, 5, 6 | lflf 37575 |
. . . 4
β’ ((π β LVec β§ π» β πΉ) β π»:πβΆπ
) |
12 | 1, 10, 11 | syl2anc 585 |
. . 3
β’ (π β π»:πβΆπ
) |
13 | 12 | ffnd 6673 |
. 2
β’ (π β π» Fn π) |
14 | | eqlkr3.e |
. . . . . . 7
β’ (π β (πΎβπΊ) = (πΎβπ»)) |
15 | | eqid 2733 |
. . . . . . . 8
β’
(.rβπ) = (.rβπ) |
16 | | eqlkr3.k |
. . . . . . . 8
β’ πΎ = (LKerβπ) |
17 | 3, 4, 15, 5, 6, 16 | eqlkr 37611 |
. . . . . . 7
β’ ((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΎβπΊ) = (πΎβπ»)) β βπ β π
βπ₯ β π (π»βπ₯) = ((πΊβπ₯)(.rβπ)π)) |
18 | 1, 2, 10, 14, 17 | syl121anc 1376 |
. . . . . 6
β’ (π β βπ β π
βπ₯ β π (π»βπ₯) = ((πΊβπ₯)(.rβπ)π)) |
19 | | eqlkr3.x |
. . . . . . . . . . 11
β’ (π β π β π) |
20 | 19 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π β π
) β π β π) |
21 | | fveq2 6846 |
. . . . . . . . . . . 12
β’ (π₯ = π β (π»βπ₯) = (π»βπ)) |
22 | | fveq2 6846 |
. . . . . . . . . . . . 13
β’ (π₯ = π β (πΊβπ₯) = (πΊβπ)) |
23 | 22 | oveq1d 7376 |
. . . . . . . . . . . 12
β’ (π₯ = π β ((πΊβπ₯)(.rβπ)π) = ((πΊβπ)(.rβπ)π)) |
24 | 21, 23 | eqeq12d 2749 |
. . . . . . . . . . 11
β’ (π₯ = π β ((π»βπ₯) = ((πΊβπ₯)(.rβπ)π) β (π»βπ) = ((πΊβπ)(.rβπ)π))) |
25 | 24 | rspcv 3579 |
. . . . . . . . . 10
β’ (π β π β (βπ₯ β π (π»βπ₯) = ((πΊβπ₯)(.rβπ)π) β (π»βπ) = ((πΊβπ)(.rβπ)π))) |
26 | 20, 25 | syl 17 |
. . . . . . . . 9
β’ ((π β§ π β π
) β (βπ₯ β π (π»βπ₯) = ((πΊβπ₯)(.rβπ)π) β (π»βπ) = ((πΊβπ)(.rβπ)π))) |
27 | | eqlkr3.a |
. . . . . . . . . . . . . . 15
β’ (π β (πΊβπ) = (π»βπ)) |
28 | 27 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π
) β (πΊβπ) = (π»βπ)) |
29 | 28 | adantr 482 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π
) β§ (π»βπ) = ((πΊβπ)(.rβπ)π)) β (πΊβπ) = (π»βπ)) |
30 | | simpr 486 |
. . . . . . . . . . . . 13
β’ (((π β§ π β π
) β§ (π»βπ) = ((πΊβπ)(.rβπ)π)) β (π»βπ) = ((πΊβπ)(.rβπ)π)) |
31 | 29, 30 | eqtr2d 2774 |
. . . . . . . . . . . 12
β’ (((π β§ π β π
) β§ (π»βπ) = ((πΊβπ)(.rβπ)π)) β ((πΊβπ)(.rβπ)π) = (πΊβπ)) |
32 | 31 | oveq2d 7377 |
. . . . . . . . . . 11
β’ (((π β§ π β π
) β§ (π»βπ) = ((πΊβπ)(.rβπ)π)) β (((invrβπ)β(πΊβπ))(.rβπ)((πΊβπ)(.rβπ)π)) = (((invrβπ)β(πΊβπ))(.rβπ)(πΊβπ))) |
33 | 3 | lvecdrng 20610 |
. . . . . . . . . . . . . . . . 17
β’ (π β LVec β π β
DivRing) |
34 | 1, 33 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β π β DivRing) |
35 | 34 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π
) β π β DivRing) |
36 | 3, 4, 5, 6 | lflcl 37576 |
. . . . . . . . . . . . . . . . 17
β’ ((π β LVec β§ πΊ β πΉ β§ π β π) β (πΊβπ) β π
) |
37 | 1, 2, 19, 36 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
β’ (π β (πΊβπ) β π
) |
38 | 37 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π
) β (πΊβπ) β π
) |
39 | | eqlkr3.n |
. . . . . . . . . . . . . . . 16
β’ (π β (πΊβπ) β 0 ) |
40 | 39 | adantr 482 |
. . . . . . . . . . . . . . 15
β’ ((π β§ π β π
) β (πΊβπ) β 0 ) |
41 | | eqlkr3.o |
. . . . . . . . . . . . . . . 16
β’ 0 =
(0gβπ) |
42 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
β’
(1rβπ) = (1rβπ) |
43 | | eqid 2733 |
. . . . . . . . . . . . . . . 16
β’
(invrβπ) = (invrβπ) |
44 | 4, 41, 15, 42, 43 | drnginvrl 20243 |
. . . . . . . . . . . . . . 15
β’ ((π β DivRing β§ (πΊβπ) β π
β§ (πΊβπ) β 0 ) β
(((invrβπ)β(πΊβπ))(.rβπ)(πΊβπ)) = (1rβπ)) |
45 | 35, 38, 40, 44 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π
) β (((invrβπ)β(πΊβπ))(.rβπ)(πΊβπ)) = (1rβπ)) |
46 | 45 | oveq1d 7376 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π
) β ((((invrβπ)β(πΊβπ))(.rβπ)(πΊβπ))(.rβπ)π) = ((1rβπ)(.rβπ)π)) |
47 | | lveclmod 20611 |
. . . . . . . . . . . . . . . . 17
β’ (π β LVec β π β LMod) |
48 | 1, 47 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β π β LMod) |
49 | 3 | lmodring 20373 |
. . . . . . . . . . . . . . . 16
β’ (π β LMod β π β Ring) |
50 | 48, 49 | syl 17 |
. . . . . . . . . . . . . . 15
β’ (π β π β Ring) |
51 | 50 | adantr 482 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π
) β π β Ring) |
52 | 4, 41, 43 | drnginvrcl 20240 |
. . . . . . . . . . . . . . 15
β’ ((π β DivRing β§ (πΊβπ) β π
β§ (πΊβπ) β 0 ) β
((invrβπ)β(πΊβπ)) β π
) |
53 | 35, 38, 40, 52 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π
) β ((invrβπ)β(πΊβπ)) β π
) |
54 | | simpr 486 |
. . . . . . . . . . . . . 14
β’ ((π β§ π β π
) β π β π
) |
55 | 4, 15 | ringass 19992 |
. . . . . . . . . . . . . 14
β’ ((π β Ring β§
(((invrβπ)β(πΊβπ)) β π
β§ (πΊβπ) β π
β§ π β π
)) β ((((invrβπ)β(πΊβπ))(.rβπ)(πΊβπ))(.rβπ)π) = (((invrβπ)β(πΊβπ))(.rβπ)((πΊβπ)(.rβπ)π))) |
56 | 51, 53, 38, 54, 55 | syl13anc 1373 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π
) β ((((invrβπ)β(πΊβπ))(.rβπ)(πΊβπ))(.rβπ)π) = (((invrβπ)β(πΊβπ))(.rβπ)((πΊβπ)(.rβπ)π))) |
57 | 4, 15, 42 | ringlidm 20000 |
. . . . . . . . . . . . . 14
β’ ((π β Ring β§ π β π
) β ((1rβπ)(.rβπ)π) = π) |
58 | 51, 54, 57 | syl2anc 585 |
. . . . . . . . . . . . 13
β’ ((π β§ π β π
) β ((1rβπ)(.rβπ)π) = π) |
59 | 46, 56, 58 | 3eqtr3d 2781 |
. . . . . . . . . . . 12
β’ ((π β§ π β π
) β (((invrβπ)β(πΊβπ))(.rβπ)((πΊβπ)(.rβπ)π)) = π) |
60 | 59 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π β π
) β§ (π»βπ) = ((πΊβπ)(.rβπ)π)) β (((invrβπ)β(πΊβπ))(.rβπ)((πΊβπ)(.rβπ)π)) = π) |
61 | 45 | adantr 482 |
. . . . . . . . . . 11
β’ (((π β§ π β π
) β§ (π»βπ) = ((πΊβπ)(.rβπ)π)) β (((invrβπ)β(πΊβπ))(.rβπ)(πΊβπ)) = (1rβπ)) |
62 | 32, 60, 61 | 3eqtr3d 2781 |
. . . . . . . . . 10
β’ (((π β§ π β π
) β§ (π»βπ) = ((πΊβπ)(.rβπ)π)) β π = (1rβπ)) |
63 | 62 | ex 414 |
. . . . . . . . 9
β’ ((π β§ π β π
) β ((π»βπ) = ((πΊβπ)(.rβπ)π) β π = (1rβπ))) |
64 | 26, 63 | syld 47 |
. . . . . . . 8
β’ ((π β§ π β π
) β (βπ₯ β π (π»βπ₯) = ((πΊβπ₯)(.rβπ)π) β π = (1rβπ))) |
65 | 64 | ancrd 553 |
. . . . . . 7
β’ ((π β§ π β π
) β (βπ₯ β π (π»βπ₯) = ((πΊβπ₯)(.rβπ)π) β (π = (1rβπ) β§ βπ₯ β π (π»βπ₯) = ((πΊβπ₯)(.rβπ)π)))) |
66 | 65 | reximdva 3162 |
. . . . . 6
β’ (π β (βπ β π
βπ₯ β π (π»βπ₯) = ((πΊβπ₯)(.rβπ)π) β βπ β π
(π = (1rβπ) β§ βπ₯ β π (π»βπ₯) = ((πΊβπ₯)(.rβπ)π)))) |
67 | 18, 66 | mpd 15 |
. . . . 5
β’ (π β βπ β π
(π = (1rβπ) β§ βπ₯ β π (π»βπ₯) = ((πΊβπ₯)(.rβπ)π))) |
68 | 4, 42 | ringidcl 19997 |
. . . . . . 7
β’ (π β Ring β
(1rβπ)
β π
) |
69 | 50, 68 | syl 17 |
. . . . . 6
β’ (π β (1rβπ) β π
) |
70 | | oveq2 7369 |
. . . . . . . . 9
β’ (π = (1rβπ) β ((πΊβπ₯)(.rβπ)π) = ((πΊβπ₯)(.rβπ)(1rβπ))) |
71 | 70 | eqeq2d 2744 |
. . . . . . . 8
β’ (π = (1rβπ) β ((π»βπ₯) = ((πΊβπ₯)(.rβπ)π) β (π»βπ₯) = ((πΊβπ₯)(.rβπ)(1rβπ)))) |
72 | 71 | ralbidv 3171 |
. . . . . . 7
β’ (π = (1rβπ) β (βπ₯ β π (π»βπ₯) = ((πΊβπ₯)(.rβπ)π) β βπ₯ β π (π»βπ₯) = ((πΊβπ₯)(.rβπ)(1rβπ)))) |
73 | 72 | ceqsrexv 3609 |
. . . . . 6
β’
((1rβπ) β π
β (βπ β π
(π = (1rβπ) β§ βπ₯ β π (π»βπ₯) = ((πΊβπ₯)(.rβπ)π)) β βπ₯ β π (π»βπ₯) = ((πΊβπ₯)(.rβπ)(1rβπ)))) |
74 | 69, 73 | syl 17 |
. . . . 5
β’ (π β (βπ β π
(π = (1rβπ) β§ βπ₯ β π (π»βπ₯) = ((πΊβπ₯)(.rβπ)π)) β βπ₯ β π (π»βπ₯) = ((πΊβπ₯)(.rβπ)(1rβπ)))) |
75 | 67, 74 | mpbid 231 |
. . . 4
β’ (π β βπ₯ β π (π»βπ₯) = ((πΊβπ₯)(.rβπ)(1rβπ))) |
76 | 75 | r19.21bi 3233 |
. . 3
β’ ((π β§ π₯ β π) β (π»βπ₯) = ((πΊβπ₯)(.rβπ)(1rβπ))) |
77 | 48 | adantr 482 |
. . . . 5
β’ ((π β§ π₯ β π) β π β LMod) |
78 | 77, 49 | syl 17 |
. . . 4
β’ ((π β§ π₯ β π) β π β Ring) |
79 | 1 | adantr 482 |
. . . . 5
β’ ((π β§ π₯ β π) β π β LVec) |
80 | 2 | adantr 482 |
. . . . 5
β’ ((π β§ π₯ β π) β πΊ β πΉ) |
81 | | simpr 486 |
. . . . 5
β’ ((π β§ π₯ β π) β π₯ β π) |
82 | 3, 4, 5, 6 | lflcl 37576 |
. . . . 5
β’ ((π β LVec β§ πΊ β πΉ β§ π₯ β π) β (πΊβπ₯) β π
) |
83 | 79, 80, 81, 82 | syl3anc 1372 |
. . . 4
β’ ((π β§ π₯ β π) β (πΊβπ₯) β π
) |
84 | 4, 15, 42 | ringridm 20001 |
. . . 4
β’ ((π β Ring β§ (πΊβπ₯) β π
) β ((πΊβπ₯)(.rβπ)(1rβπ)) = (πΊβπ₯)) |
85 | 78, 83, 84 | syl2anc 585 |
. . 3
β’ ((π β§ π₯ β π) β ((πΊβπ₯)(.rβπ)(1rβπ)) = (πΊβπ₯)) |
86 | 76, 85 | eqtr2d 2774 |
. 2
β’ ((π β§ π₯ β π) β (πΊβπ₯) = (π»βπ₯)) |
87 | 9, 13, 86 | eqfnfvd 6989 |
1
β’ (π β πΊ = π») |