Step | Hyp | Ref
| Expression |
1 | | 3simpa 1148 |
. . . . . . . 8
β’ ((π β LMod β§ π β π΅ β§ π β π΅) β (π β LMod β§ π β π΅)) |
2 | 1 | adantr 482 |
. . . . . . 7
β’ (((π β LMod β§ π β π΅ β§ π β π΅) β§ π΄ β π) β (π β LMod β§ π β π΅)) |
3 | | lincresunit3lem3.b |
. . . . . . . 8
β’ π΅ = (Baseβπ) |
4 | | lincresunit3lem3.r |
. . . . . . . 8
β’ π
= (Scalarβπ) |
5 | | lincresunit3lem3.t |
. . . . . . . 8
β’ Β· = (
Β·π βπ) |
6 | | eqid 2736 |
. . . . . . . 8
β’
(1rβπ
) = (1rβπ
) |
7 | 3, 4, 5, 6 | lmodvs1 20196 |
. . . . . . 7
β’ ((π β LMod β§ π β π΅) β ((1rβπ
) Β· π) = π) |
8 | 2, 7 | syl 17 |
. . . . . 6
β’ (((π β LMod β§ π β π΅ β§ π β π΅) β§ π΄ β π) β ((1rβπ
) Β· π) = π) |
9 | 4 | lmodring 20176 |
. . . . . . . . . . . 12
β’ (π β LMod β π
β Ring) |
10 | 9 | 3ad2ant1 1133 |
. . . . . . . . . . 11
β’ ((π β LMod β§ π β π΅ β§ π β π΅) β π
β Ring) |
11 | 10 | adantr 482 |
. . . . . . . . . 10
β’ (((π β LMod β§ π β π΅ β§ π β π΅) β§ π΄ β π) β π
β Ring) |
12 | | lincresunit3lem3.u |
. . . . . . . . . . . . 13
β’ π = (Unitβπ
) |
13 | | lincresunit3lem3.n |
. . . . . . . . . . . . 13
β’ π = (invgβπ
) |
14 | 12, 13 | unitnegcl 19968 |
. . . . . . . . . . . 12
β’ ((π
β Ring β§ π΄ β π) β (πβπ΄) β π) |
15 | 9, 14 | sylan 581 |
. . . . . . . . . . 11
β’ ((π β LMod β§ π΄ β π) β (πβπ΄) β π) |
16 | 15 | 3ad2antl1 1185 |
. . . . . . . . . 10
β’ (((π β LMod β§ π β π΅ β§ π β π΅) β§ π΄ β π) β (πβπ΄) β π) |
17 | 11, 16 | jca 513 |
. . . . . . . . 9
β’ (((π β LMod β§ π β π΅ β§ π β π΅) β§ π΄ β π) β (π
β Ring β§ (πβπ΄) β π)) |
18 | | eqid 2736 |
. . . . . . . . . 10
β’
(invrβπ
) = (invrβπ
) |
19 | | eqid 2736 |
. . . . . . . . . 10
β’
(.rβπ
) = (.rβπ
) |
20 | 12, 18, 19, 6 | unitlinv 19964 |
. . . . . . . . 9
β’ ((π
β Ring β§ (πβπ΄) β π) β (((invrβπ
)β(πβπ΄))(.rβπ
)(πβπ΄)) = (1rβπ
)) |
21 | 17, 20 | syl 17 |
. . . . . . . 8
β’ (((π β LMod β§ π β π΅ β§ π β π΅) β§ π΄ β π) β (((invrβπ
)β(πβπ΄))(.rβπ
)(πβπ΄)) = (1rβπ
)) |
22 | 21 | eqcomd 2742 |
. . . . . . 7
β’ (((π β LMod β§ π β π΅ β§ π β π΅) β§ π΄ β π) β (1rβπ
) =
(((invrβπ
)β(πβπ΄))(.rβπ
)(πβπ΄))) |
23 | 22 | oveq1d 7322 |
. . . . . 6
β’ (((π β LMod β§ π β π΅ β§ π β π΅) β§ π΄ β π) β ((1rβπ
) Β· π) = ((((invrβπ
)β(πβπ΄))(.rβπ
)(πβπ΄)) Β· π)) |
24 | 8, 23 | eqtr3d 2778 |
. . . . 5
β’ (((π β LMod β§ π β π΅ β§ π β π΅) β§ π΄ β π) β π = ((((invrβπ
)β(πβπ΄))(.rβπ
)(πβπ΄)) Β· π)) |
25 | 24 | adantr 482 |
. . . 4
β’ ((((π β LMod β§ π β π΅ β§ π β π΅) β§ π΄ β π) β§ ((πβπ΄) Β· π) = ((πβπ΄) Β· π)) β π = ((((invrβπ
)β(πβπ΄))(.rβπ
)(πβπ΄)) Β· π)) |
26 | | simpl1 1191 |
. . . . . . . 8
β’ (((π β LMod β§ π β π΅ β§ π β π΅) β§ π΄ β π) β π β LMod) |
27 | | lincresunit3lem3.e |
. . . . . . . . . . 11
β’ πΈ = (Baseβπ
) |
28 | 12, 18, 27 | ringinvcl 19963 |
. . . . . . . . . 10
β’ ((π
β Ring β§ (πβπ΄) β π) β ((invrβπ
)β(πβπ΄)) β πΈ) |
29 | 17, 28 | syl 17 |
. . . . . . . . 9
β’ (((π β LMod β§ π β π΅ β§ π β π΅) β§ π΄ β π) β ((invrβπ
)β(πβπ΄)) β πΈ) |
30 | 4 | lmodfgrp 20177 |
. . . . . . . . . . 11
β’ (π β LMod β π
β Grp) |
31 | 30 | 3ad2ant1 1133 |
. . . . . . . . . 10
β’ ((π β LMod β§ π β π΅ β§ π β π΅) β π
β Grp) |
32 | 27, 12 | unitcl 19946 |
. . . . . . . . . 10
β’ (π΄ β π β π΄ β πΈ) |
33 | 27, 13 | grpinvcl 18672 |
. . . . . . . . . 10
β’ ((π
β Grp β§ π΄ β πΈ) β (πβπ΄) β πΈ) |
34 | 31, 32, 33 | syl2an 597 |
. . . . . . . . 9
β’ (((π β LMod β§ π β π΅ β§ π β π΅) β§ π΄ β π) β (πβπ΄) β πΈ) |
35 | | simpl2 1192 |
. . . . . . . . 9
β’ (((π β LMod β§ π β π΅ β§ π β π΅) β§ π΄ β π) β π β π΅) |
36 | 29, 34, 35 | 3jca 1128 |
. . . . . . . 8
β’ (((π β LMod β§ π β π΅ β§ π β π΅) β§ π΄ β π) β (((invrβπ
)β(πβπ΄)) β πΈ β§ (πβπ΄) β πΈ β§ π β π΅)) |
37 | 26, 36 | jca 513 |
. . . . . . 7
β’ (((π β LMod β§ π β π΅ β§ π β π΅) β§ π΄ β π) β (π β LMod β§
(((invrβπ
)β(πβπ΄)) β πΈ β§ (πβπ΄) β πΈ β§ π β π΅))) |
38 | 37 | adantr 482 |
. . . . . 6
β’ ((((π β LMod β§ π β π΅ β§ π β π΅) β§ π΄ β π) β§ ((πβπ΄) Β· π) = ((πβπ΄) Β· π)) β (π β LMod β§
(((invrβπ
)β(πβπ΄)) β πΈ β§ (πβπ΄) β πΈ β§ π β π΅))) |
39 | 3, 4, 5, 27, 19 | lmodvsass 20193 |
. . . . . 6
β’ ((π β LMod β§
(((invrβπ
)β(πβπ΄)) β πΈ β§ (πβπ΄) β πΈ β§ π β π΅)) β ((((invrβπ
)β(πβπ΄))(.rβπ
)(πβπ΄)) Β· π) = (((invrβπ
)β(πβπ΄)) Β· ((πβπ΄) Β· π))) |
40 | 38, 39 | syl 17 |
. . . . 5
β’ ((((π β LMod β§ π β π΅ β§ π β π΅) β§ π΄ β π) β§ ((πβπ΄) Β· π) = ((πβπ΄) Β· π)) β ((((invrβπ
)β(πβπ΄))(.rβπ
)(πβπ΄)) Β· π) = (((invrβπ
)β(πβπ΄)) Β· ((πβπ΄) Β· π))) |
41 | | oveq2 7315 |
. . . . . 6
β’ (((πβπ΄) Β· π) = ((πβπ΄) Β· π) β (((invrβπ
)β(πβπ΄)) Β· ((πβπ΄) Β· π)) = (((invrβπ
)β(πβπ΄)) Β· ((πβπ΄) Β· π))) |
42 | 41 | adantl 483 |
. . . . 5
β’ ((((π β LMod β§ π β π΅ β§ π β π΅) β§ π΄ β π) β§ ((πβπ΄) Β· π) = ((πβπ΄) Β· π)) β (((invrβπ
)β(πβπ΄)) Β· ((πβπ΄) Β· π)) = (((invrβπ
)β(πβπ΄)) Β· ((πβπ΄) Β· π))) |
43 | 26 | adantr 482 |
. . . . . . . 8
β’ ((((π β LMod β§ π β π΅ β§ π β π΅) β§ π΄ β π) β§ ((πβπ΄) Β· π) = ((πβπ΄) Β· π)) β π β LMod) |
44 | | simpl3 1193 |
. . . . . . . . . 10
β’ (((π β LMod β§ π β π΅ β§ π β π΅) β§ π΄ β π) β π β π΅) |
45 | 29, 34, 44 | 3jca 1128 |
. . . . . . . . 9
β’ (((π β LMod β§ π β π΅ β§ π β π΅) β§ π΄ β π) β (((invrβπ
)β(πβπ΄)) β πΈ β§ (πβπ΄) β πΈ β§ π β π΅)) |
46 | 45 | adantr 482 |
. . . . . . . 8
β’ ((((π β LMod β§ π β π΅ β§ π β π΅) β§ π΄ β π) β§ ((πβπ΄) Β· π) = ((πβπ΄) Β· π)) β (((invrβπ
)β(πβπ΄)) β πΈ β§ (πβπ΄) β πΈ β§ π β π΅)) |
47 | 43, 46 | jca 513 |
. . . . . . 7
β’ ((((π β LMod β§ π β π΅ β§ π β π΅) β§ π΄ β π) β§ ((πβπ΄) Β· π) = ((πβπ΄) Β· π)) β (π β LMod β§
(((invrβπ
)β(πβπ΄)) β πΈ β§ (πβπ΄) β πΈ β§ π β π΅))) |
48 | 3, 4, 5, 27, 19 | lmodvsass 20193 |
. . . . . . 7
β’ ((π β LMod β§
(((invrβπ
)β(πβπ΄)) β πΈ β§ (πβπ΄) β πΈ β§ π β π΅)) β ((((invrβπ
)β(πβπ΄))(.rβπ
)(πβπ΄)) Β· π) = (((invrβπ
)β(πβπ΄)) Β· ((πβπ΄) Β· π))) |
49 | 47, 48 | syl 17 |
. . . . . 6
β’ ((((π β LMod β§ π β π΅ β§ π β π΅) β§ π΄ β π) β§ ((πβπ΄) Β· π) = ((πβπ΄) Β· π)) β ((((invrβπ
)β(πβπ΄))(.rβπ
)(πβπ΄)) Β· π) = (((invrβπ
)β(πβπ΄)) Β· ((πβπ΄) Β· π))) |
50 | 17 | adantr 482 |
. . . . . . . 8
β’ ((((π β LMod β§ π β π΅ β§ π β π΅) β§ π΄ β π) β§ ((πβπ΄) Β· π) = ((πβπ΄) Β· π)) β (π
β Ring β§ (πβπ΄) β π)) |
51 | 50, 20 | syl 17 |
. . . . . . 7
β’ ((((π β LMod β§ π β π΅ β§ π β π΅) β§ π΄ β π) β§ ((πβπ΄) Β· π) = ((πβπ΄) Β· π)) β (((invrβπ
)β(πβπ΄))(.rβπ
)(πβπ΄)) = (1rβπ
)) |
52 | 51 | oveq1d 7322 |
. . . . . 6
β’ ((((π β LMod β§ π β π΅ β§ π β π΅) β§ π΄ β π) β§ ((πβπ΄) Β· π) = ((πβπ΄) Β· π)) β ((((invrβπ
)β(πβπ΄))(.rβπ
)(πβπ΄)) Β· π) = ((1rβπ
) Β· π)) |
53 | 49, 52 | eqtr3d 2778 |
. . . . 5
β’ ((((π β LMod β§ π β π΅ β§ π β π΅) β§ π΄ β π) β§ ((πβπ΄) Β· π) = ((πβπ΄) Β· π)) β (((invrβπ
)β(πβπ΄)) Β· ((πβπ΄) Β· π)) = ((1rβπ
) Β· π)) |
54 | 40, 42, 53 | 3eqtrd 2780 |
. . . 4
β’ ((((π β LMod β§ π β π΅ β§ π β π΅) β§ π΄ β π) β§ ((πβπ΄) Β· π) = ((πβπ΄) Β· π)) β ((((invrβπ
)β(πβπ΄))(.rβπ
)(πβπ΄)) Β· π) = ((1rβπ
) Β· π)) |
55 | | 3simpb 1149 |
. . . . . . 7
β’ ((π β LMod β§ π β π΅ β§ π β π΅) β (π β LMod β§ π β π΅)) |
56 | 55 | adantr 482 |
. . . . . 6
β’ (((π β LMod β§ π β π΅ β§ π β π΅) β§ π΄ β π) β (π β LMod β§ π β π΅)) |
57 | 56 | adantr 482 |
. . . . 5
β’ ((((π β LMod β§ π β π΅ β§ π β π΅) β§ π΄ β π) β§ ((πβπ΄) Β· π) = ((πβπ΄) Β· π)) β (π β LMod β§ π β π΅)) |
58 | 3, 4, 5, 6 | lmodvs1 20196 |
. . . . 5
β’ ((π β LMod β§ π β π΅) β ((1rβπ
) Β· π) = π) |
59 | 57, 58 | syl 17 |
. . . 4
β’ ((((π β LMod β§ π β π΅ β§ π β π΅) β§ π΄ β π) β§ ((πβπ΄) Β· π) = ((πβπ΄) Β· π)) β ((1rβπ
) Β· π) = π) |
60 | 25, 54, 59 | 3eqtrd 2780 |
. . 3
β’ ((((π β LMod β§ π β π΅ β§ π β π΅) β§ π΄ β π) β§ ((πβπ΄) Β· π) = ((πβπ΄) Β· π)) β π = π) |
61 | 60 | ex 414 |
. 2
β’ (((π β LMod β§ π β π΅ β§ π β π΅) β§ π΄ β π) β (((πβπ΄) Β· π) = ((πβπ΄) Β· π) β π = π)) |
62 | | oveq2 7315 |
. 2
β’ (π = π β ((πβπ΄) Β· π) = ((πβπ΄) Β· π)) |
63 | 61, 62 | impbid1 224 |
1
β’ (((π β LMod β§ π β π΅ β§ π β π΅) β§ π΄ β π) β (((πβπ΄) Β· π) = ((πβπ΄) Β· π) β π = π)) |