Step | Hyp | Ref
| Expression |
1 | | oveq2 7366 |
. . . 4
β’ (π = (π΄ Β· π) β ((πΌβπ΄) Β· π) = ((πΌβπ΄) Β· (π΄ Β· π))) |
2 | | lvecinv.w |
. . . . . . . 8
β’ (π β π β LVec) |
3 | | lvecinv.f |
. . . . . . . . 9
β’ πΉ = (Scalarβπ) |
4 | 3 | lvecdrng 20581 |
. . . . . . . 8
β’ (π β LVec β πΉ β
DivRing) |
5 | 2, 4 | syl 17 |
. . . . . . 7
β’ (π β πΉ β DivRing) |
6 | | lvecinv.a |
. . . . . . . 8
β’ (π β π΄ β (πΎ β { 0 })) |
7 | 6 | eldifad 3923 |
. . . . . . 7
β’ (π β π΄ β πΎ) |
8 | | eldifsni 4751 |
. . . . . . . 8
β’ (π΄ β (πΎ β { 0 }) β π΄ β 0 ) |
9 | 6, 8 | syl 17 |
. . . . . . 7
β’ (π β π΄ β 0 ) |
10 | | lvecinv.k |
. . . . . . . 8
β’ πΎ = (BaseβπΉ) |
11 | | lvecinv.o |
. . . . . . . 8
β’ 0 =
(0gβπΉ) |
12 | | eqid 2733 |
. . . . . . . 8
β’
(.rβπΉ) = (.rβπΉ) |
13 | | eqid 2733 |
. . . . . . . 8
β’
(1rβπΉ) = (1rβπΉ) |
14 | | lvecinv.i |
. . . . . . . 8
β’ πΌ = (invrβπΉ) |
15 | 10, 11, 12, 13, 14 | drnginvrl 20220 |
. . . . . . 7
β’ ((πΉ β DivRing β§ π΄ β πΎ β§ π΄ β 0 ) β ((πΌβπ΄)(.rβπΉ)π΄) = (1rβπΉ)) |
16 | 5, 7, 9, 15 | syl3anc 1372 |
. . . . . 6
β’ (π β ((πΌβπ΄)(.rβπΉ)π΄) = (1rβπΉ)) |
17 | 16 | oveq1d 7373 |
. . . . 5
β’ (π β (((πΌβπ΄)(.rβπΉ)π΄) Β· π) = ((1rβπΉ) Β· π)) |
18 | | lveclmod 20582 |
. . . . . . 7
β’ (π β LVec β π β LMod) |
19 | 2, 18 | syl 17 |
. . . . . 6
β’ (π β π β LMod) |
20 | 10, 11, 14 | drnginvrcl 20217 |
. . . . . . 7
β’ ((πΉ β DivRing β§ π΄ β πΎ β§ π΄ β 0 ) β (πΌβπ΄) β πΎ) |
21 | 5, 7, 9, 20 | syl3anc 1372 |
. . . . . 6
β’ (π β (πΌβπ΄) β πΎ) |
22 | | lvecinv.y |
. . . . . 6
β’ (π β π β π) |
23 | | lvecinv.v |
. . . . . . 7
β’ π = (Baseβπ) |
24 | | lvecinv.t |
. . . . . . 7
β’ Β· = (
Β·π βπ) |
25 | 23, 3, 24, 10, 12 | lmodvsass 20362 |
. . . . . 6
β’ ((π β LMod β§ ((πΌβπ΄) β πΎ β§ π΄ β πΎ β§ π β π)) β (((πΌβπ΄)(.rβπΉ)π΄) Β· π) = ((πΌβπ΄) Β· (π΄ Β· π))) |
26 | 19, 21, 7, 22, 25 | syl13anc 1373 |
. . . . 5
β’ (π β (((πΌβπ΄)(.rβπΉ)π΄) Β· π) = ((πΌβπ΄) Β· (π΄ Β· π))) |
27 | 23, 3, 24, 13 | lmodvs1 20365 |
. . . . . 6
β’ ((π β LMod β§ π β π) β ((1rβπΉ) Β· π) = π) |
28 | 19, 22, 27 | syl2anc 585 |
. . . . 5
β’ (π β
((1rβπΉ)
Β·
π) = π) |
29 | 17, 26, 28 | 3eqtr3d 2781 |
. . . 4
β’ (π β ((πΌβπ΄) Β· (π΄ Β· π)) = π) |
30 | 1, 29 | sylan9eqr 2795 |
. . 3
β’ ((π β§ π = (π΄ Β· π)) β ((πΌβπ΄) Β· π) = π) |
31 | 10, 11, 12, 13, 14 | drnginvrr 20221 |
. . . . . . 7
β’ ((πΉ β DivRing β§ π΄ β πΎ β§ π΄ β 0 ) β (π΄(.rβπΉ)(πΌβπ΄)) = (1rβπΉ)) |
32 | 5, 7, 9, 31 | syl3anc 1372 |
. . . . . 6
β’ (π β (π΄(.rβπΉ)(πΌβπ΄)) = (1rβπΉ)) |
33 | 32 | oveq1d 7373 |
. . . . 5
β’ (π β ((π΄(.rβπΉ)(πΌβπ΄)) Β· π) = ((1rβπΉ) Β· π)) |
34 | | lvecinv.x |
. . . . . 6
β’ (π β π β π) |
35 | 23, 3, 24, 10, 12 | lmodvsass 20362 |
. . . . . 6
β’ ((π β LMod β§ (π΄ β πΎ β§ (πΌβπ΄) β πΎ β§ π β π)) β ((π΄(.rβπΉ)(πΌβπ΄)) Β· π) = (π΄ Β· ((πΌβπ΄) Β· π))) |
36 | 19, 7, 21, 34, 35 | syl13anc 1373 |
. . . . 5
β’ (π β ((π΄(.rβπΉ)(πΌβπ΄)) Β· π) = (π΄ Β· ((πΌβπ΄) Β· π))) |
37 | 23, 3, 24, 13 | lmodvs1 20365 |
. . . . . 6
β’ ((π β LMod β§ π β π) β ((1rβπΉ) Β· π) = π) |
38 | 19, 34, 37 | syl2anc 585 |
. . . . 5
β’ (π β
((1rβπΉ)
Β·
π) = π) |
39 | 33, 36, 38 | 3eqtr3rd 2782 |
. . . 4
β’ (π β π = (π΄ Β· ((πΌβπ΄) Β· π))) |
40 | | oveq2 7366 |
. . . 4
β’ (((πΌβπ΄) Β· π) = π β (π΄ Β· ((πΌβπ΄) Β· π)) = (π΄ Β· π)) |
41 | 39, 40 | sylan9eq 2793 |
. . 3
β’ ((π β§ ((πΌβπ΄) Β· π) = π) β π = (π΄ Β· π)) |
42 | 30, 41 | impbida 800 |
. 2
β’ (π β (π = (π΄ Β· π) β ((πΌβπ΄) Β· π) = π)) |
43 | | eqcom 2740 |
. 2
β’ (((πΌβπ΄) Β· π) = π β π = ((πΌβπ΄) Β· π)) |
44 | 42, 43 | bitrdi 287 |
1
β’ (π β (π = (π΄ Β· π) β π = ((πΌβπ΄) Β· π))) |