Step | Hyp | Ref
| Expression |
1 | | simpl1 1191 |
. . . . 5
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ πΊ = (π Γ {(0gβπ·)})) β π β LVec) |
2 | | lveclmod 20709 |
. . . . . 6
β’ (π β LVec β π β LMod) |
3 | | eqlkr.d |
. . . . . . 7
β’ π· = (Scalarβπ) |
4 | 3 | lmodring 20471 |
. . . . . 6
β’ (π β LMod β π· β Ring) |
5 | 2, 4 | syl 17 |
. . . . 5
β’ (π β LVec β π· β Ring) |
6 | 1, 5 | syl 17 |
. . . 4
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ πΊ = (π Γ {(0gβπ·)})) β π· β Ring) |
7 | | eqlkr.k |
. . . . 5
β’ πΎ = (Baseβπ·) |
8 | | eqid 2732 |
. . . . 5
β’
(1rβπ·) = (1rβπ·) |
9 | 7, 8 | ringidcl 20076 |
. . . 4
β’ (π· β Ring β
(1rβπ·)
β πΎ) |
10 | 6, 9 | syl 17 |
. . 3
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ πΊ = (π Γ {(0gβπ·)})) β
(1rβπ·)
β πΎ) |
11 | | simp11 1203 |
. . . . . . . 8
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ πΊ = (π Γ {(0gβπ·)}) β§ π₯ β π) β π β LVec) |
12 | 11, 5 | syl 17 |
. . . . . . 7
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ πΊ = (π Γ {(0gβπ·)}) β§ π₯ β π) β π· β Ring) |
13 | | simp12l 1286 |
. . . . . . . 8
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ πΊ = (π Γ {(0gβπ·)}) β§ π₯ β π) β πΊ β πΉ) |
14 | | simp3 1138 |
. . . . . . . 8
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ πΊ = (π Γ {(0gβπ·)}) β§ π₯ β π) β π₯ β π) |
15 | | eqlkr.v |
. . . . . . . . 9
β’ π = (Baseβπ) |
16 | | eqlkr.f |
. . . . . . . . 9
β’ πΉ = (LFnlβπ) |
17 | 3, 7, 15, 16 | lflcl 37922 |
. . . . . . . 8
β’ ((π β LVec β§ πΊ β πΉ β§ π₯ β π) β (πΊβπ₯) β πΎ) |
18 | 11, 13, 14, 17 | syl3anc 1371 |
. . . . . . 7
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ πΊ = (π Γ {(0gβπ·)}) β§ π₯ β π) β (πΊβπ₯) β πΎ) |
19 | | eqlkr.t |
. . . . . . . 8
β’ Β· =
(.rβπ·) |
20 | 7, 19, 8 | ringridm 20080 |
. . . . . . 7
β’ ((π· β Ring β§ (πΊβπ₯) β πΎ) β ((πΊβπ₯) Β·
(1rβπ·)) =
(πΊβπ₯)) |
21 | 12, 18, 20 | syl2anc 584 |
. . . . . 6
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ πΊ = (π Γ {(0gβπ·)}) β§ π₯ β π) β ((πΊβπ₯) Β·
(1rβπ·)) =
(πΊβπ₯)) |
22 | | simp2 1137 |
. . . . . . . 8
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ πΊ = (π Γ {(0gβπ·)}) β§ π₯ β π) β πΊ = (π Γ {(0gβπ·)})) |
23 | | simp13 1205 |
. . . . . . . . . 10
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ πΊ = (π Γ {(0gβπ·)}) β§ π₯ β π) β (πΏβπΊ) = (πΏβπ»)) |
24 | 11, 2 | syl 17 |
. . . . . . . . . . . 12
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ πΊ = (π Γ {(0gβπ·)}) β§ π₯ β π) β π β LMod) |
25 | | eqid 2732 |
. . . . . . . . . . . . 13
β’
(0gβπ·) = (0gβπ·) |
26 | | eqlkr.l |
. . . . . . . . . . . . 13
β’ πΏ = (LKerβπ) |
27 | 3, 25, 15, 16, 26 | lkr0f 37952 |
. . . . . . . . . . . 12
β’ ((π β LMod β§ πΊ β πΉ) β ((πΏβπΊ) = π β πΊ = (π Γ {(0gβπ·)}))) |
28 | 24, 13, 27 | syl2anc 584 |
. . . . . . . . . . 11
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ πΊ = (π Γ {(0gβπ·)}) β§ π₯ β π) β ((πΏβπΊ) = π β πΊ = (π Γ {(0gβπ·)}))) |
29 | 22, 28 | mpbird 256 |
. . . . . . . . . 10
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ πΊ = (π Γ {(0gβπ·)}) β§ π₯ β π) β (πΏβπΊ) = π) |
30 | 23, 29 | eqtr3d 2774 |
. . . . . . . . 9
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ πΊ = (π Γ {(0gβπ·)}) β§ π₯ β π) β (πΏβπ») = π) |
31 | | simp12r 1287 |
. . . . . . . . . 10
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ πΊ = (π Γ {(0gβπ·)}) β§ π₯ β π) β π» β πΉ) |
32 | 3, 25, 15, 16, 26 | lkr0f 37952 |
. . . . . . . . . 10
β’ ((π β LMod β§ π» β πΉ) β ((πΏβπ») = π β π» = (π Γ {(0gβπ·)}))) |
33 | 24, 31, 32 | syl2anc 584 |
. . . . . . . . 9
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ πΊ = (π Γ {(0gβπ·)}) β§ π₯ β π) β ((πΏβπ») = π β π» = (π Γ {(0gβπ·)}))) |
34 | 30, 33 | mpbid 231 |
. . . . . . . 8
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ πΊ = (π Γ {(0gβπ·)}) β§ π₯ β π) β π» = (π Γ {(0gβπ·)})) |
35 | 22, 34 | eqtr4d 2775 |
. . . . . . 7
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ πΊ = (π Γ {(0gβπ·)}) β§ π₯ β π) β πΊ = π») |
36 | 35 | fveq1d 6890 |
. . . . . 6
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ πΊ = (π Γ {(0gβπ·)}) β§ π₯ β π) β (πΊβπ₯) = (π»βπ₯)) |
37 | 21, 36 | eqtr2d 2773 |
. . . . 5
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ πΊ = (π Γ {(0gβπ·)}) β§ π₯ β π) β (π»βπ₯) = ((πΊβπ₯) Β·
(1rβπ·))) |
38 | 37 | 3expia 1121 |
. . . 4
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ πΊ = (π Γ {(0gβπ·)})) β (π₯ β π β (π»βπ₯) = ((πΊβπ₯) Β·
(1rβπ·)))) |
39 | 38 | ralrimiv 3145 |
. . 3
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ πΊ = (π Γ {(0gβπ·)})) β βπ₯ β π (π»βπ₯) = ((πΊβπ₯) Β·
(1rβπ·))) |
40 | | oveq2 7413 |
. . . . . 6
β’ (π = (1rβπ·) β ((πΊβπ₯) Β· π) = ((πΊβπ₯) Β·
(1rβπ·))) |
41 | 40 | eqeq2d 2743 |
. . . . 5
β’ (π = (1rβπ·) β ((π»βπ₯) = ((πΊβπ₯) Β· π) β (π»βπ₯) = ((πΊβπ₯) Β·
(1rβπ·)))) |
42 | 41 | ralbidv 3177 |
. . . 4
β’ (π = (1rβπ·) β (βπ₯ β π (π»βπ₯) = ((πΊβπ₯) Β· π) β βπ₯ β π (π»βπ₯) = ((πΊβπ₯) Β·
(1rβπ·)))) |
43 | 42 | rspcev 3612 |
. . 3
β’
(((1rβπ·) β πΎ β§ βπ₯ β π (π»βπ₯) = ((πΊβπ₯) Β·
(1rβπ·)))
β βπ β
πΎ βπ₯ β π (π»βπ₯) = ((πΊβπ₯) Β· π)) |
44 | 10, 39, 43 | syl2anc 584 |
. 2
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ πΊ = (π Γ {(0gβπ·)})) β βπ β πΎ βπ₯ β π (π»βπ₯) = ((πΊβπ₯) Β· π)) |
45 | | simpl1 1191 |
. . . 4
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ πΊ β (π Γ {(0gβπ·)})) β π β LVec) |
46 | | simpl2l 1226 |
. . . 4
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ πΊ β (π Γ {(0gβπ·)})) β πΊ β πΉ) |
47 | | simpr 485 |
. . . 4
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ πΊ β (π Γ {(0gβπ·)})) β πΊ β (π Γ {(0gβπ·)})) |
48 | 3, 25, 8, 15, 16 | lfl1 37928 |
. . . 4
β’ ((π β LVec β§ πΊ β πΉ β§ πΊ β (π Γ {(0gβπ·)})) β βπ§ β π (πΊβπ§) = (1rβπ·)) |
49 | 45, 46, 47, 48 | syl3anc 1371 |
. . 3
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ πΊ β (π Γ {(0gβπ·)})) β βπ§ β π (πΊβπ§) = (1rβπ·)) |
50 | | simpl1 1191 |
. . . . . . . 8
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ (πΊ β (π Γ {(0gβπ·)}) β§ π§ β π β§ (πΊβπ§) = (1rβπ·))) β π β LVec) |
51 | | simpl2r 1227 |
. . . . . . . 8
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ (πΊ β (π Γ {(0gβπ·)}) β§ π§ β π β§ (πΊβπ§) = (1rβπ·))) β π» β πΉ) |
52 | | simpr2 1195 |
. . . . . . . 8
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ (πΊ β (π Γ {(0gβπ·)}) β§ π§ β π β§ (πΊβπ§) = (1rβπ·))) β π§ β π) |
53 | 3, 7, 15, 16 | lflcl 37922 |
. . . . . . . 8
β’ ((π β LVec β§ π» β πΉ β§ π§ β π) β (π»βπ§) β πΎ) |
54 | 50, 51, 52, 53 | syl3anc 1371 |
. . . . . . 7
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ (πΊ β (π Γ {(0gβπ·)}) β§ π§ β π β§ (πΊβπ§) = (1rβπ·))) β (π»βπ§) β πΎ) |
55 | | simp11 1203 |
. . . . . . . . . . . . . 14
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ (πΊ β (π Γ {(0gβπ·)}) β§ π§ β π β§ (πΊβπ§) = (1rβπ·)) β§ π₯ β π) β π β LVec) |
56 | 55, 2 | syl 17 |
. . . . . . . . . . . . 13
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ (πΊ β (π Γ {(0gβπ·)}) β§ π§ β π β§ (πΊβπ§) = (1rβπ·)) β§ π₯ β π) β π β LMod) |
57 | | simp12r 1287 |
. . . . . . . . . . . . 13
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ (πΊ β (π Γ {(0gβπ·)}) β§ π§ β π β§ (πΊβπ§) = (1rβπ·)) β§ π₯ β π) β π» β πΉ) |
58 | | simp12l 1286 |
. . . . . . . . . . . . . 14
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ (πΊ β (π Γ {(0gβπ·)}) β§ π§ β π β§ (πΊβπ§) = (1rβπ·)) β§ π₯ β π) β πΊ β πΉ) |
59 | | simp3 1138 |
. . . . . . . . . . . . . 14
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ (πΊ β (π Γ {(0gβπ·)}) β§ π§ β π β§ (πΊβπ§) = (1rβπ·)) β§ π₯ β π) β π₯ β π) |
60 | 3, 7, 15, 16 | lflcl 37922 |
. . . . . . . . . . . . . 14
β’ ((π β LMod β§ πΊ β πΉ β§ π₯ β π) β (πΊβπ₯) β πΎ) |
61 | 56, 58, 59, 60 | syl3anc 1371 |
. . . . . . . . . . . . 13
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ (πΊ β (π Γ {(0gβπ·)}) β§ π§ β π β§ (πΊβπ§) = (1rβπ·)) β§ π₯ β π) β (πΊβπ₯) β πΎ) |
62 | | simp22 1207 |
. . . . . . . . . . . . 13
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ (πΊ β (π Γ {(0gβπ·)}) β§ π§ β π β§ (πΊβπ§) = (1rβπ·)) β§ π₯ β π) β π§ β π) |
63 | | eqid 2732 |
. . . . . . . . . . . . . 14
β’ (
Β·π βπ) = ( Β·π
βπ) |
64 | 3, 7, 19, 15, 63, 16 | lflmul 37926 |
. . . . . . . . . . . . 13
β’ ((π β LMod β§ π» β πΉ β§ ((πΊβπ₯) β πΎ β§ π§ β π)) β (π»β((πΊβπ₯)( Β·π
βπ)π§)) = ((πΊβπ₯) Β· (π»βπ§))) |
65 | 56, 57, 61, 62, 64 | syl112anc 1374 |
. . . . . . . . . . . 12
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ (πΊ β (π Γ {(0gβπ·)}) β§ π§ β π β§ (πΊβπ§) = (1rβπ·)) β§ π₯ β π) β (π»β((πΊβπ₯)( Β·π
βπ)π§)) = ((πΊβπ₯) Β· (π»βπ§))) |
66 | 65 | oveq2d 7421 |
. . . . . . . . . . 11
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ (πΊ β (π Γ {(0gβπ·)}) β§ π§ β π β§ (πΊβπ§) = (1rβπ·)) β§ π₯ β π) β ((π»βπ₯)(-gβπ·)(π»β((πΊβπ₯)( Β·π
βπ)π§))) = ((π»βπ₯)(-gβπ·)((πΊβπ₯) Β· (π»βπ§)))) |
67 | 15, 3, 63, 7 | lmodvscl 20481 |
. . . . . . . . . . . . . 14
β’ ((π β LMod β§ (πΊβπ₯) β πΎ β§ π§ β π) β ((πΊβπ₯)( Β·π
βπ)π§) β π) |
68 | 56, 61, 62, 67 | syl3anc 1371 |
. . . . . . . . . . . . 13
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ (πΊ β (π Γ {(0gβπ·)}) β§ π§ β π β§ (πΊβπ§) = (1rβπ·)) β§ π₯ β π) β ((πΊβπ₯)( Β·π
βπ)π§) β π) |
69 | | eqid 2732 |
. . . . . . . . . . . . . 14
β’
(-gβπ·) = (-gβπ·) |
70 | | eqid 2732 |
. . . . . . . . . . . . . 14
β’
(-gβπ) = (-gβπ) |
71 | 3, 69, 15, 70, 16 | lflsub 37925 |
. . . . . . . . . . . . 13
β’ ((π β LMod β§ π» β πΉ β§ (π₯ β π β§ ((πΊβπ₯)( Β·π
βπ)π§) β π)) β (π»β(π₯(-gβπ)((πΊβπ₯)( Β·π
βπ)π§))) = ((π»βπ₯)(-gβπ·)(π»β((πΊβπ₯)( Β·π
βπ)π§)))) |
72 | 56, 57, 59, 68, 71 | syl112anc 1374 |
. . . . . . . . . . . 12
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ (πΊ β (π Γ {(0gβπ·)}) β§ π§ β π β§ (πΊβπ§) = (1rβπ·)) β§ π₯ β π) β (π»β(π₯(-gβπ)((πΊβπ₯)( Β·π
βπ)π§))) = ((π»βπ₯)(-gβπ·)(π»β((πΊβπ₯)( Β·π
βπ)π§)))) |
73 | 15, 70 | lmodvsubcl 20509 |
. . . . . . . . . . . . . . . . 17
β’ ((π β LMod β§ π₯ β π β§ ((πΊβπ₯)( Β·π
βπ)π§) β π) β (π₯(-gβπ)((πΊβπ₯)( Β·π
βπ)π§)) β π) |
74 | 56, 59, 68, 73 | syl3anc 1371 |
. . . . . . . . . . . . . . . 16
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ (πΊ β (π Γ {(0gβπ·)}) β§ π§ β π β§ (πΊβπ§) = (1rβπ·)) β§ π₯ β π) β (π₯(-gβπ)((πΊβπ₯)( Β·π
βπ)π§)) β π) |
75 | 3, 69, 15, 70, 16 | lflsub 37925 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β LMod β§ πΊ β πΉ β§ (π₯ β π β§ ((πΊβπ₯)( Β·π
βπ)π§) β π)) β (πΊβ(π₯(-gβπ)((πΊβπ₯)( Β·π
βπ)π§))) = ((πΊβπ₯)(-gβπ·)(πΊβ((πΊβπ₯)( Β·π
βπ)π§)))) |
76 | 56, 58, 59, 68, 75 | syl112anc 1374 |
. . . . . . . . . . . . . . . . 17
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ (πΊ β (π Γ {(0gβπ·)}) β§ π§ β π β§ (πΊβπ§) = (1rβπ·)) β§ π₯ β π) β (πΊβ(π₯(-gβπ)((πΊβπ₯)( Β·π
βπ)π§))) = ((πΊβπ₯)(-gβπ·)(πΊβ((πΊβπ₯)( Β·π
βπ)π§)))) |
77 | 55, 58, 59, 17 | syl3anc 1371 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ (πΊ β (π Γ {(0gβπ·)}) β§ π§ β π β§ (πΊβπ§) = (1rβπ·)) β§ π₯ β π) β (πΊβπ₯) β πΎ) |
78 | 3, 7, 19, 15, 63, 16 | lflmul 37926 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π β LMod β§ πΊ β πΉ β§ ((πΊβπ₯) β πΎ β§ π§ β π)) β (πΊβ((πΊβπ₯)( Β·π
βπ)π§)) = ((πΊβπ₯) Β· (πΊβπ§))) |
79 | 56, 58, 77, 62, 78 | syl112anc 1374 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ (πΊ β (π Γ {(0gβπ·)}) β§ π§ β π β§ (πΊβπ§) = (1rβπ·)) β§ π₯ β π) β (πΊβ((πΊβπ₯)( Β·π
βπ)π§)) = ((πΊβπ₯) Β· (πΊβπ§))) |
80 | | simp23 1208 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ (πΊ β (π Γ {(0gβπ·)}) β§ π§ β π β§ (πΊβπ§) = (1rβπ·)) β§ π₯ β π) β (πΊβπ§) = (1rβπ·)) |
81 | 80 | oveq2d 7421 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ (πΊ β (π Γ {(0gβπ·)}) β§ π§ β π β§ (πΊβπ§) = (1rβπ·)) β§ π₯ β π) β ((πΊβπ₯) Β· (πΊβπ§)) = ((πΊβπ₯) Β·
(1rβπ·))) |
82 | 55, 5 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ (πΊ β (π Γ {(0gβπ·)}) β§ π§ β π β§ (πΊβπ§) = (1rβπ·)) β§ π₯ β π) β π· β Ring) |
83 | 82, 77, 20 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ (πΊ β (π Γ {(0gβπ·)}) β§ π§ β π β§ (πΊβπ§) = (1rβπ·)) β§ π₯ β π) β ((πΊβπ₯) Β·
(1rβπ·)) =
(πΊβπ₯)) |
84 | 79, 81, 83 | 3eqtrd 2776 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ (πΊ β (π Γ {(0gβπ·)}) β§ π§ β π β§ (πΊβπ§) = (1rβπ·)) β§ π₯ β π) β (πΊβ((πΊβπ₯)( Β·π
βπ)π§)) = (πΊβπ₯)) |
85 | 84 | oveq2d 7421 |
. . . . . . . . . . . . . . . . 17
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ (πΊ β (π Γ {(0gβπ·)}) β§ π§ β π β§ (πΊβπ§) = (1rβπ·)) β§ π₯ β π) β ((πΊβπ₯)(-gβπ·)(πΊβ((πΊβπ₯)( Β·π
βπ)π§))) = ((πΊβπ₯)(-gβπ·)(πΊβπ₯))) |
86 | 3 | lmodfgrp 20472 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β LMod β π· β Grp) |
87 | 2, 86 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β LVec β π· β Grp) |
88 | 55, 87 | syl 17 |
. . . . . . . . . . . . . . . . . 18
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ (πΊ β (π Γ {(0gβπ·)}) β§ π§ β π β§ (πΊβπ§) = (1rβπ·)) β§ π₯ β π) β π· β Grp) |
89 | 7, 25, 69 | grpsubid 18903 |
. . . . . . . . . . . . . . . . . 18
β’ ((π· β Grp β§ (πΊβπ₯) β πΎ) β ((πΊβπ₯)(-gβπ·)(πΊβπ₯)) = (0gβπ·)) |
90 | 88, 77, 89 | syl2anc 584 |
. . . . . . . . . . . . . . . . 17
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ (πΊ β (π Γ {(0gβπ·)}) β§ π§ β π β§ (πΊβπ§) = (1rβπ·)) β§ π₯ β π) β ((πΊβπ₯)(-gβπ·)(πΊβπ₯)) = (0gβπ·)) |
91 | 76, 85, 90 | 3eqtrd 2776 |
. . . . . . . . . . . . . . . 16
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ (πΊ β (π Γ {(0gβπ·)}) β§ π§ β π β§ (πΊβπ§) = (1rβπ·)) β§ π₯ β π) β (πΊβ(π₯(-gβπ)((πΊβπ₯)( Β·π
βπ)π§))) = (0gβπ·)) |
92 | 15, 3, 25, 16, 26 | ellkr 37947 |
. . . . . . . . . . . . . . . . 17
β’ ((π β LVec β§ πΊ β πΉ) β ((π₯(-gβπ)((πΊβπ₯)( Β·π
βπ)π§)) β (πΏβπΊ) β ((π₯(-gβπ)((πΊβπ₯)( Β·π
βπ)π§)) β π β§ (πΊβ(π₯(-gβπ)((πΊβπ₯)( Β·π
βπ)π§))) = (0gβπ·)))) |
93 | 55, 58, 92 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ (πΊ β (π Γ {(0gβπ·)}) β§ π§ β π β§ (πΊβπ§) = (1rβπ·)) β§ π₯ β π) β ((π₯(-gβπ)((πΊβπ₯)( Β·π
βπ)π§)) β (πΏβπΊ) β ((π₯(-gβπ)((πΊβπ₯)( Β·π
βπ)π§)) β π β§ (πΊβ(π₯(-gβπ)((πΊβπ₯)( Β·π
βπ)π§))) = (0gβπ·)))) |
94 | 74, 91, 93 | mpbir2and 711 |
. . . . . . . . . . . . . . 15
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ (πΊ β (π Γ {(0gβπ·)}) β§ π§ β π β§ (πΊβπ§) = (1rβπ·)) β§ π₯ β π) β (π₯(-gβπ)((πΊβπ₯)( Β·π
βπ)π§)) β (πΏβπΊ)) |
95 | | simp13 1205 |
. . . . . . . . . . . . . . 15
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ (πΊ β (π Γ {(0gβπ·)}) β§ π§ β π β§ (πΊβπ§) = (1rβπ·)) β§ π₯ β π) β (πΏβπΊ) = (πΏβπ»)) |
96 | 94, 95 | eleqtrd 2835 |
. . . . . . . . . . . . . 14
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ (πΊ β (π Γ {(0gβπ·)}) β§ π§ β π β§ (πΊβπ§) = (1rβπ·)) β§ π₯ β π) β (π₯(-gβπ)((πΊβπ₯)( Β·π
βπ)π§)) β (πΏβπ»)) |
97 | 15, 3, 25, 16, 26 | ellkr 37947 |
. . . . . . . . . . . . . . 15
β’ ((π β LVec β§ π» β πΉ) β ((π₯(-gβπ)((πΊβπ₯)( Β·π
βπ)π§)) β (πΏβπ») β ((π₯(-gβπ)((πΊβπ₯)( Β·π
βπ)π§)) β π β§ (π»β(π₯(-gβπ)((πΊβπ₯)( Β·π
βπ)π§))) = (0gβπ·)))) |
98 | 55, 57, 97 | syl2anc 584 |
. . . . . . . . . . . . . 14
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ (πΊ β (π Γ {(0gβπ·)}) β§ π§ β π β§ (πΊβπ§) = (1rβπ·)) β§ π₯ β π) β ((π₯(-gβπ)((πΊβπ₯)( Β·π
βπ)π§)) β (πΏβπ») β ((π₯(-gβπ)((πΊβπ₯)( Β·π
βπ)π§)) β π β§ (π»β(π₯(-gβπ)((πΊβπ₯)( Β·π
βπ)π§))) = (0gβπ·)))) |
99 | 96, 98 | mpbid 231 |
. . . . . . . . . . . . 13
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ (πΊ β (π Γ {(0gβπ·)}) β§ π§ β π β§ (πΊβπ§) = (1rβπ·)) β§ π₯ β π) β ((π₯(-gβπ)((πΊβπ₯)( Β·π
βπ)π§)) β π β§ (π»β(π₯(-gβπ)((πΊβπ₯)( Β·π
βπ)π§))) = (0gβπ·))) |
100 | 99 | simprd 496 |
. . . . . . . . . . . 12
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ (πΊ β (π Γ {(0gβπ·)}) β§ π§ β π β§ (πΊβπ§) = (1rβπ·)) β§ π₯ β π) β (π»β(π₯(-gβπ)((πΊβπ₯)( Β·π
βπ)π§))) = (0gβπ·)) |
101 | 72, 100 | eqtr3d 2774 |
. . . . . . . . . . 11
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ (πΊ β (π Γ {(0gβπ·)}) β§ π§ β π β§ (πΊβπ§) = (1rβπ·)) β§ π₯ β π) β ((π»βπ₯)(-gβπ·)(π»β((πΊβπ₯)( Β·π
βπ)π§))) = (0gβπ·)) |
102 | 66, 101 | eqtr3d 2774 |
. . . . . . . . . 10
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ (πΊ β (π Γ {(0gβπ·)}) β§ π§ β π β§ (πΊβπ§) = (1rβπ·)) β§ π₯ β π) β ((π»βπ₯)(-gβπ·)((πΊβπ₯) Β· (π»βπ§))) = (0gβπ·)) |
103 | 3, 7, 15, 16 | lflcl 37922 |
. . . . . . . . . . . 12
β’ ((π β LVec β§ π» β πΉ β§ π₯ β π) β (π»βπ₯) β πΎ) |
104 | 55, 57, 59, 103 | syl3anc 1371 |
. . . . . . . . . . 11
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ (πΊ β (π Γ {(0gβπ·)}) β§ π§ β π β§ (πΊβπ§) = (1rβπ·)) β§ π₯ β π) β (π»βπ₯) β πΎ) |
105 | 54 | 3adant3 1132 |
. . . . . . . . . . . 12
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ (πΊ β (π Γ {(0gβπ·)}) β§ π§ β π β§ (πΊβπ§) = (1rβπ·)) β§ π₯ β π) β (π»βπ§) β πΎ) |
106 | 3, 7, 19 | lmodmcl 20476 |
. . . . . . . . . . . 12
β’ ((π β LMod β§ (πΊβπ₯) β πΎ β§ (π»βπ§) β πΎ) β ((πΊβπ₯) Β· (π»βπ§)) β πΎ) |
107 | 56, 77, 105, 106 | syl3anc 1371 |
. . . . . . . . . . 11
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ (πΊ β (π Γ {(0gβπ·)}) β§ π§ β π β§ (πΊβπ§) = (1rβπ·)) β§ π₯ β π) β ((πΊβπ₯) Β· (π»βπ§)) β πΎ) |
108 | 7, 25, 69 | grpsubeq0 18905 |
. . . . . . . . . . 11
β’ ((π· β Grp β§ (π»βπ₯) β πΎ β§ ((πΊβπ₯) Β· (π»βπ§)) β πΎ) β (((π»βπ₯)(-gβπ·)((πΊβπ₯) Β· (π»βπ§))) = (0gβπ·) β (π»βπ₯) = ((πΊβπ₯) Β· (π»βπ§)))) |
109 | 88, 104, 107, 108 | syl3anc 1371 |
. . . . . . . . . 10
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ (πΊ β (π Γ {(0gβπ·)}) β§ π§ β π β§ (πΊβπ§) = (1rβπ·)) β§ π₯ β π) β (((π»βπ₯)(-gβπ·)((πΊβπ₯) Β· (π»βπ§))) = (0gβπ·) β (π»βπ₯) = ((πΊβπ₯) Β· (π»βπ§)))) |
110 | 102, 109 | mpbid 231 |
. . . . . . . . 9
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ (πΊ β (π Γ {(0gβπ·)}) β§ π§ β π β§ (πΊβπ§) = (1rβπ·)) β§ π₯ β π) β (π»βπ₯) = ((πΊβπ₯) Β· (π»βπ§))) |
111 | 110 | 3expia 1121 |
. . . . . . . 8
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ (πΊ β (π Γ {(0gβπ·)}) β§ π§ β π β§ (πΊβπ§) = (1rβπ·))) β (π₯ β π β (π»βπ₯) = ((πΊβπ₯) Β· (π»βπ§)))) |
112 | 111 | ralrimiv 3145 |
. . . . . . 7
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ (πΊ β (π Γ {(0gβπ·)}) β§ π§ β π β§ (πΊβπ§) = (1rβπ·))) β βπ₯ β π (π»βπ₯) = ((πΊβπ₯) Β· (π»βπ§))) |
113 | | oveq2 7413 |
. . . . . . . . . 10
β’ (π = (π»βπ§) β ((πΊβπ₯) Β· π) = ((πΊβπ₯) Β· (π»βπ§))) |
114 | 113 | eqeq2d 2743 |
. . . . . . . . 9
β’ (π = (π»βπ§) β ((π»βπ₯) = ((πΊβπ₯) Β· π) β (π»βπ₯) = ((πΊβπ₯) Β· (π»βπ§)))) |
115 | 114 | ralbidv 3177 |
. . . . . . . 8
β’ (π = (π»βπ§) β (βπ₯ β π (π»βπ₯) = ((πΊβπ₯) Β· π) β βπ₯ β π (π»βπ₯) = ((πΊβπ₯) Β· (π»βπ§)))) |
116 | 115 | rspcev 3612 |
. . . . . . 7
β’ (((π»βπ§) β πΎ β§ βπ₯ β π (π»βπ₯) = ((πΊβπ₯) Β· (π»βπ§))) β βπ β πΎ βπ₯ β π (π»βπ₯) = ((πΊβπ₯) Β· π)) |
117 | 54, 112, 116 | syl2anc 584 |
. . . . . 6
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ (πΊ β (π Γ {(0gβπ·)}) β§ π§ β π β§ (πΊβπ§) = (1rβπ·))) β βπ β πΎ βπ₯ β π (π»βπ₯) = ((πΊβπ₯) Β· π)) |
118 | 117 | 3exp2 1354 |
. . . . 5
β’ ((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β (πΊ β (π Γ {(0gβπ·)}) β (π§ β π β ((πΊβπ§) = (1rβπ·) β βπ β πΎ βπ₯ β π (π»βπ₯) = ((πΊβπ₯) Β· π))))) |
119 | 118 | imp 407 |
. . . 4
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ πΊ β (π Γ {(0gβπ·)})) β (π§ β π β ((πΊβπ§) = (1rβπ·) β βπ β πΎ βπ₯ β π (π»βπ₯) = ((πΊβπ₯) Β· π)))) |
120 | 119 | rexlimdv 3153 |
. . 3
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ πΊ β (π Γ {(0gβπ·)})) β (βπ§ β π (πΊβπ§) = (1rβπ·) β βπ β πΎ βπ₯ β π (π»βπ₯) = ((πΊβπ₯) Β· π))) |
121 | 49, 120 | mpd 15 |
. 2
β’ (((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β§ πΊ β (π Γ {(0gβπ·)})) β βπ β πΎ βπ₯ β π (π»βπ₯) = ((πΊβπ₯) Β· π)) |
122 | 44, 121 | pm2.61dane 3029 |
1
β’ ((π β LVec β§ (πΊ β πΉ β§ π» β πΉ) β§ (πΏβπΊ) = (πΏβπ»)) β βπ β πΎ βπ₯ β π (π»βπ₯) = ((πΊβπ₯) Β· π)) |