Step | Hyp | Ref
| Expression |
1 | | df-ne 2941 |
. . . . 5
β’ (π΄ β π β Β¬ π΄ = π) |
2 | | oveq2 7366 |
. . . . . . . 8
β’ ((π΄ Β· π) = 0 β
(((invrβπΉ)βπ΄) Β· (π΄ Β· π)) = (((invrβπΉ)βπ΄) Β· 0 )) |
3 | 2 | ad2antlr 726 |
. . . . . . 7
β’ (((π β§ (π΄ Β· π) = 0 ) β§ π΄ β π) β (((invrβπΉ)βπ΄) Β· (π΄ Β· π)) = (((invrβπΉ)βπ΄) Β· 0 )) |
4 | | lvecmul0or.w |
. . . . . . . . . . . . 13
β’ (π β π β LVec) |
5 | 4 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ π΄ β π) β π β LVec) |
6 | | lvecmul0or.f |
. . . . . . . . . . . . 13
β’ πΉ = (Scalarβπ) |
7 | 6 | lvecdrng 20581 |
. . . . . . . . . . . 12
β’ (π β LVec β πΉ β
DivRing) |
8 | 5, 7 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π΄ β π) β πΉ β DivRing) |
9 | | lvecmul0or.a |
. . . . . . . . . . . 12
β’ (π β π΄ β πΎ) |
10 | 9 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π΄ β π) β π΄ β πΎ) |
11 | | simpr 486 |
. . . . . . . . . . 11
β’ ((π β§ π΄ β π) β π΄ β π) |
12 | | lvecmul0or.k |
. . . . . . . . . . . 12
β’ πΎ = (BaseβπΉ) |
13 | | lvecmul0or.o |
. . . . . . . . . . . 12
β’ π = (0gβπΉ) |
14 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(.rβπΉ) = (.rβπΉ) |
15 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(1rβπΉ) = (1rβπΉ) |
16 | | eqid 2733 |
. . . . . . . . . . . 12
β’
(invrβπΉ) = (invrβπΉ) |
17 | 12, 13, 14, 15, 16 | drnginvrl 20220 |
. . . . . . . . . . 11
β’ ((πΉ β DivRing β§ π΄ β πΎ β§ π΄ β π) β (((invrβπΉ)βπ΄)(.rβπΉ)π΄) = (1rβπΉ)) |
18 | 8, 10, 11, 17 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((π β§ π΄ β π) β (((invrβπΉ)βπ΄)(.rβπΉ)π΄) = (1rβπΉ)) |
19 | 18 | oveq1d 7373 |
. . . . . . . . 9
β’ ((π β§ π΄ β π) β ((((invrβπΉ)βπ΄)(.rβπΉ)π΄) Β· π) = ((1rβπΉ) Β· π)) |
20 | | lveclmod 20582 |
. . . . . . . . . . . 12
β’ (π β LVec β π β LMod) |
21 | 4, 20 | syl 17 |
. . . . . . . . . . 11
β’ (π β π β LMod) |
22 | 21 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π΄ β π) β π β LMod) |
23 | 12, 13, 16 | drnginvrcl 20217 |
. . . . . . . . . . 11
β’ ((πΉ β DivRing β§ π΄ β πΎ β§ π΄ β π) β ((invrβπΉ)βπ΄) β πΎ) |
24 | 8, 10, 11, 23 | syl3anc 1372 |
. . . . . . . . . 10
β’ ((π β§ π΄ β π) β ((invrβπΉ)βπ΄) β πΎ) |
25 | | lvecmul0or.x |
. . . . . . . . . . 11
β’ (π β π β π) |
26 | 25 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π΄ β π) β π β π) |
27 | | lvecmul0or.v |
. . . . . . . . . . 11
β’ π = (Baseβπ) |
28 | | lvecmul0or.s |
. . . . . . . . . . 11
β’ Β· = (
Β·π βπ) |
29 | 27, 6, 28, 12, 14 | lmodvsass 20362 |
. . . . . . . . . 10
β’ ((π β LMod β§
(((invrβπΉ)βπ΄) β πΎ β§ π΄ β πΎ β§ π β π)) β ((((invrβπΉ)βπ΄)(.rβπΉ)π΄) Β· π) = (((invrβπΉ)βπ΄) Β· (π΄ Β· π))) |
30 | 22, 24, 10, 26, 29 | syl13anc 1373 |
. . . . . . . . 9
β’ ((π β§ π΄ β π) β ((((invrβπΉ)βπ΄)(.rβπΉ)π΄) Β· π) = (((invrβπΉ)βπ΄) Β· (π΄ Β· π))) |
31 | 27, 6, 28, 15 | lmodvs1 20365 |
. . . . . . . . . . 11
β’ ((π β LMod β§ π β π) β ((1rβπΉ) Β· π) = π) |
32 | 21, 25, 31 | syl2anc 585 |
. . . . . . . . . 10
β’ (π β
((1rβπΉ)
Β·
π) = π) |
33 | 32 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π΄ β π) β ((1rβπΉ) Β· π) = π) |
34 | 19, 30, 33 | 3eqtr3d 2781 |
. . . . . . . 8
β’ ((π β§ π΄ β π) β (((invrβπΉ)βπ΄) Β· (π΄ Β· π)) = π) |
35 | 34 | adantlr 714 |
. . . . . . 7
β’ (((π β§ (π΄ Β· π) = 0 ) β§ π΄ β π) β (((invrβπΉ)βπ΄) Β· (π΄ Β· π)) = π) |
36 | 21 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ (π΄ Β· π) = 0 ) β π β LMod) |
37 | 36 | adantr 482 |
. . . . . . . 8
β’ (((π β§ (π΄ Β· π) = 0 ) β§ π΄ β π) β π β LMod) |
38 | 24 | adantlr 714 |
. . . . . . . 8
β’ (((π β§ (π΄ Β· π) = 0 ) β§ π΄ β π) β ((invrβπΉ)βπ΄) β πΎ) |
39 | | lvecmul0or.z |
. . . . . . . . 9
β’ 0 =
(0gβπ) |
40 | 6, 28, 12, 39 | lmodvs0 20371 |
. . . . . . . 8
β’ ((π β LMod β§
((invrβπΉ)βπ΄) β πΎ) β (((invrβπΉ)βπ΄) Β· 0 ) = 0 ) |
41 | 37, 38, 40 | syl2anc 585 |
. . . . . . 7
β’ (((π β§ (π΄ Β· π) = 0 ) β§ π΄ β π) β (((invrβπΉ)βπ΄) Β· 0 ) = 0 ) |
42 | 3, 35, 41 | 3eqtr3d 2781 |
. . . . . 6
β’ (((π β§ (π΄ Β· π) = 0 ) β§ π΄ β π) β π = 0 ) |
43 | 42 | ex 414 |
. . . . 5
β’ ((π β§ (π΄ Β· π) = 0 ) β (π΄ β π β π = 0 )) |
44 | 1, 43 | biimtrrid 242 |
. . . 4
β’ ((π β§ (π΄ Β· π) = 0 ) β (Β¬ π΄ = π β π = 0 )) |
45 | 44 | orrd 862 |
. . 3
β’ ((π β§ (π΄ Β· π) = 0 ) β (π΄ = π β¨ π = 0 )) |
46 | 45 | ex 414 |
. 2
β’ (π β ((π΄ Β· π) = 0 β (π΄ = π β¨ π = 0 ))) |
47 | 27, 6, 28, 13, 39 | lmod0vs 20370 |
. . . . 5
β’ ((π β LMod β§ π β π) β (π Β· π) = 0 ) |
48 | 21, 25, 47 | syl2anc 585 |
. . . 4
β’ (π β (π Β· π) = 0 ) |
49 | | oveq1 7365 |
. . . . 5
β’ (π΄ = π β (π΄ Β· π) = (π Β· π)) |
50 | 49 | eqeq1d 2735 |
. . . 4
β’ (π΄ = π β ((π΄ Β· π) = 0 β (π Β· π) = 0 )) |
51 | 48, 50 | syl5ibrcom 247 |
. . 3
β’ (π β (π΄ = π β (π΄ Β· π) = 0 )) |
52 | 6, 28, 12, 39 | lmodvs0 20371 |
. . . . 5
β’ ((π β LMod β§ π΄ β πΎ) β (π΄ Β· 0 ) = 0 ) |
53 | 21, 9, 52 | syl2anc 585 |
. . . 4
β’ (π β (π΄ Β· 0 ) = 0 ) |
54 | | oveq2 7366 |
. . . . 5
β’ (π = 0 β (π΄ Β· π) = (π΄ Β· 0 )) |
55 | 54 | eqeq1d 2735 |
. . . 4
β’ (π = 0 β ((π΄ Β· π) = 0 β (π΄ Β· 0 ) = 0 )) |
56 | 53, 55 | syl5ibrcom 247 |
. . 3
β’ (π β (π = 0 β (π΄ Β· π) = 0 )) |
57 | 51, 56 | jaod 858 |
. 2
β’ (π β ((π΄ = π β¨ π = 0 ) β (π΄ Β· π) = 0 )) |
58 | 46, 57 | impbid 211 |
1
β’ (π β ((π΄ Β· π) = 0 β (π΄ = π β¨ π = 0 ))) |