Step | Hyp | Ref
| Expression |
1 | | lssvs0or.w |
. . . . . . . . . . . 12
β’ (π β π β LVec) |
2 | | lssvs0or.f |
. . . . . . . . . . . . 13
β’ πΉ = (Scalarβπ) |
3 | 2 | lvecdrng 20581 |
. . . . . . . . . . . 12
β’ (π β LVec β πΉ β
DivRing) |
4 | 1, 3 | syl 17 |
. . . . . . . . . . 11
β’ (π β πΉ β DivRing) |
5 | 4 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ (π΄ Β· π) β π) β§ π΄ β 0 ) β πΉ β DivRing) |
6 | | lssvs0or.a |
. . . . . . . . . . 11
β’ (π β π΄ β πΎ) |
7 | 6 | ad2antrr 725 |
. . . . . . . . . 10
β’ (((π β§ (π΄ Β· π) β π) β§ π΄ β 0 ) β π΄ β πΎ) |
8 | | simpr 486 |
. . . . . . . . . 10
β’ (((π β§ (π΄ Β· π) β π) β§ π΄ β 0 ) β π΄ β 0 ) |
9 | | lssvs0or.k |
. . . . . . . . . . 11
β’ πΎ = (BaseβπΉ) |
10 | | lssvs0or.o |
. . . . . . . . . . 11
β’ 0 =
(0gβπΉ) |
11 | | eqid 2733 |
. . . . . . . . . . 11
β’
(.rβπΉ) = (.rβπΉ) |
12 | | eqid 2733 |
. . . . . . . . . . 11
β’
(1rβπΉ) = (1rβπΉ) |
13 | | eqid 2733 |
. . . . . . . . . . 11
β’
(invrβπΉ) = (invrβπΉ) |
14 | 9, 10, 11, 12, 13 | drnginvrl 20220 |
. . . . . . . . . 10
β’ ((πΉ β DivRing β§ π΄ β πΎ β§ π΄ β 0 ) β
(((invrβπΉ)βπ΄)(.rβπΉ)π΄) = (1rβπΉ)) |
15 | 5, 7, 8, 14 | syl3anc 1372 |
. . . . . . . . 9
β’ (((π β§ (π΄ Β· π) β π) β§ π΄ β 0 ) β
(((invrβπΉ)βπ΄)(.rβπΉ)π΄) = (1rβπΉ)) |
16 | 15 | oveq1d 7373 |
. . . . . . . 8
β’ (((π β§ (π΄ Β· π) β π) β§ π΄ β 0 ) β
((((invrβπΉ)βπ΄)(.rβπΉ)π΄) Β· π) = ((1rβπΉ) Β· π)) |
17 | | lveclmod 20582 |
. . . . . . . . . . 11
β’ (π β LVec β π β LMod) |
18 | 1, 17 | syl 17 |
. . . . . . . . . 10
β’ (π β π β LMod) |
19 | 18 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ (π΄ Β· π) β π) β§ π΄ β 0 ) β π β LMod) |
20 | 9, 10, 13 | drnginvrcl 20217 |
. . . . . . . . . 10
β’ ((πΉ β DivRing β§ π΄ β πΎ β§ π΄ β 0 ) β
((invrβπΉ)βπ΄) β πΎ) |
21 | 5, 7, 8, 20 | syl3anc 1372 |
. . . . . . . . 9
β’ (((π β§ (π΄ Β· π) β π) β§ π΄ β 0 ) β
((invrβπΉ)βπ΄) β πΎ) |
22 | | lssvs0or.x |
. . . . . . . . . 10
β’ (π β π β π) |
23 | 22 | ad2antrr 725 |
. . . . . . . . 9
β’ (((π β§ (π΄ Β· π) β π) β§ π΄ β 0 ) β π β π) |
24 | | lssvs0or.v |
. . . . . . . . . 10
β’ π = (Baseβπ) |
25 | | lssvs0or.t |
. . . . . . . . . 10
β’ Β· = (
Β·π βπ) |
26 | 24, 2, 25, 9, 11 | lmodvsass 20362 |
. . . . . . . . 9
β’ ((π β LMod β§
(((invrβπΉ)βπ΄) β πΎ β§ π΄ β πΎ β§ π β π)) β ((((invrβπΉ)βπ΄)(.rβπΉ)π΄) Β· π) = (((invrβπΉ)βπ΄) Β· (π΄ Β· π))) |
27 | 19, 21, 7, 23, 26 | syl13anc 1373 |
. . . . . . . 8
β’ (((π β§ (π΄ Β· π) β π) β§ π΄ β 0 ) β
((((invrβπΉ)βπ΄)(.rβπΉ)π΄) Β· π) = (((invrβπΉ)βπ΄) Β· (π΄ Β· π))) |
28 | 24, 2, 25, 12 | lmodvs1 20365 |
. . . . . . . . 9
β’ ((π β LMod β§ π β π) β ((1rβπΉ) Β· π) = π) |
29 | 19, 23, 28 | syl2anc 585 |
. . . . . . . 8
β’ (((π β§ (π΄ Β· π) β π) β§ π΄ β 0 ) β
((1rβπΉ)
Β·
π) = π) |
30 | 16, 27, 29 | 3eqtr3rd 2782 |
. . . . . . 7
β’ (((π β§ (π΄ Β· π) β π) β§ π΄ β 0 ) β π = (((invrβπΉ)βπ΄) Β· (π΄ Β· π))) |
31 | | lssvs0or.u |
. . . . . . . . 9
β’ (π β π β π) |
32 | 31 | ad2antrr 725 |
. . . . . . . 8
β’ (((π β§ (π΄ Β· π) β π) β§ π΄ β 0 ) β π β π) |
33 | | simplr 768 |
. . . . . . . 8
β’ (((π β§ (π΄ Β· π) β π) β§ π΄ β 0 ) β (π΄ Β· π) β π) |
34 | | lssvs0or.s |
. . . . . . . . 9
β’ π = (LSubSpβπ) |
35 | 2, 25, 9, 34 | lssvscl 20431 |
. . . . . . . 8
β’ (((π β LMod β§ π β π) β§ (((invrβπΉ)βπ΄) β πΎ β§ (π΄ Β· π) β π)) β (((invrβπΉ)βπ΄) Β· (π΄ Β· π)) β π) |
36 | 19, 32, 21, 33, 35 | syl22anc 838 |
. . . . . . 7
β’ (((π β§ (π΄ Β· π) β π) β§ π΄ β 0 ) β
(((invrβπΉ)βπ΄) Β· (π΄ Β· π)) β π) |
37 | 30, 36 | eqeltrd 2834 |
. . . . . 6
β’ (((π β§ (π΄ Β· π) β π) β§ π΄ β 0 ) β π β π) |
38 | 37 | ex 414 |
. . . . 5
β’ ((π β§ (π΄ Β· π) β π) β (π΄ β 0 β π β π)) |
39 | 38 | necon1bd 2958 |
. . . 4
β’ ((π β§ (π΄ Β· π) β π) β (Β¬ π β π β π΄ = 0 )) |
40 | 39 | orrd 862 |
. . 3
β’ ((π β§ (π΄ Β· π) β π) β (π β π β¨ π΄ = 0 )) |
41 | 40 | orcomd 870 |
. 2
β’ ((π β§ (π΄ Β· π) β π) β (π΄ = 0 β¨ π β π)) |
42 | | oveq1 7365 |
. . . . 5
β’ (π΄ = 0 β (π΄ Β· π) = ( 0 Β· π)) |
43 | 42 | adantl 483 |
. . . 4
β’ ((π β§ π΄ = 0 ) β (π΄ Β· π) = ( 0 Β· π)) |
44 | | eqid 2733 |
. . . . . . . 8
β’
(0gβπ) = (0gβπ) |
45 | 24, 2, 25, 10, 44 | lmod0vs 20370 |
. . . . . . 7
β’ ((π β LMod β§ π β π) β ( 0 Β· π) = (0gβπ)) |
46 | 18, 22, 45 | syl2anc 585 |
. . . . . 6
β’ (π β ( 0 Β· π) = (0gβπ)) |
47 | 44, 34 | lss0cl 20422 |
. . . . . . 7
β’ ((π β LMod β§ π β π) β (0gβπ) β π) |
48 | 18, 31, 47 | syl2anc 585 |
. . . . . 6
β’ (π β (0gβπ) β π) |
49 | 46, 48 | eqeltrd 2834 |
. . . . 5
β’ (π β ( 0 Β· π) β π) |
50 | 49 | adantr 482 |
. . . 4
β’ ((π β§ π΄ = 0 ) β ( 0 Β· π) β π) |
51 | 43, 50 | eqeltrd 2834 |
. . 3
β’ ((π β§ π΄ = 0 ) β (π΄ Β· π) β π) |
52 | 18 | adantr 482 |
. . . 4
β’ ((π β§ π β π) β π β LMod) |
53 | 31 | adantr 482 |
. . . 4
β’ ((π β§ π β π) β π β π) |
54 | 6 | adantr 482 |
. . . 4
β’ ((π β§ π β π) β π΄ β πΎ) |
55 | | simpr 486 |
. . . 4
β’ ((π β§ π β π) β π β π) |
56 | 2, 25, 9, 34 | lssvscl 20431 |
. . . 4
β’ (((π β LMod β§ π β π) β§ (π΄ β πΎ β§ π β π)) β (π΄ Β· π) β π) |
57 | 52, 53, 54, 55, 56 | syl22anc 838 |
. . 3
β’ ((π β§ π β π) β (π΄ Β· π) β π) |
58 | 51, 57 | jaodan 957 |
. 2
β’ ((π β§ (π΄ = 0 β¨ π β π)) β (π΄ Β· π) β π) |
59 | 41, 58 | impbida 800 |
1
β’ (π β ((π΄ Β· π) β π β (π΄ = 0 β¨ π β π))) |