Proof of Theorem lssvs0or
Step | Hyp | Ref
| Expression |
1 | | lssvs0or.w |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑊 ∈ LVec) |
2 | | lssvs0or.f |
. . . . . . . . . . . . 13
⊢ 𝐹 = (Scalar‘𝑊) |
3 | 2 | lvecdrng 20009 |
. . . . . . . . . . . 12
⊢ (𝑊 ∈ LVec → 𝐹 ∈
DivRing) |
4 | 1, 3 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ∈ DivRing) |
5 | 4 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐴 · 𝑋) ∈ 𝑈) ∧ 𝐴 ≠ 0 ) → 𝐹 ∈ DivRing) |
6 | | lssvs0or.a |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐴 ∈ 𝐾) |
7 | 6 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐴 · 𝑋) ∈ 𝑈) ∧ 𝐴 ≠ 0 ) → 𝐴 ∈ 𝐾) |
8 | | simpr 488 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝐴 · 𝑋) ∈ 𝑈) ∧ 𝐴 ≠ 0 ) → 𝐴 ≠ 0 ) |
9 | | lssvs0or.k |
. . . . . . . . . . 11
⊢ 𝐾 = (Base‘𝐹) |
10 | | lssvs0or.o |
. . . . . . . . . . 11
⊢ 0 =
(0g‘𝐹) |
11 | | eqid 2739 |
. . . . . . . . . . 11
⊢
(.r‘𝐹) = (.r‘𝐹) |
12 | | eqid 2739 |
. . . . . . . . . . 11
⊢
(1r‘𝐹) = (1r‘𝐹) |
13 | | eqid 2739 |
. . . . . . . . . . 11
⊢
(invr‘𝐹) = (invr‘𝐹) |
14 | 9, 10, 11, 12, 13 | drnginvrl 19653 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ DivRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐴 ≠ 0 ) →
(((invr‘𝐹)‘𝐴)(.r‘𝐹)𝐴) = (1r‘𝐹)) |
15 | 5, 7, 8, 14 | syl3anc 1372 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐴 · 𝑋) ∈ 𝑈) ∧ 𝐴 ≠ 0 ) →
(((invr‘𝐹)‘𝐴)(.r‘𝐹)𝐴) = (1r‘𝐹)) |
16 | 15 | oveq1d 7198 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐴 · 𝑋) ∈ 𝑈) ∧ 𝐴 ≠ 0 ) →
((((invr‘𝐹)‘𝐴)(.r‘𝐹)𝐴) · 𝑋) = ((1r‘𝐹) · 𝑋)) |
17 | | lveclmod 20010 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod) |
18 | 1, 17 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝑊 ∈ LMod) |
19 | 18 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐴 · 𝑋) ∈ 𝑈) ∧ 𝐴 ≠ 0 ) → 𝑊 ∈ LMod) |
20 | 9, 10, 13 | drnginvrcl 19651 |
. . . . . . . . . 10
⊢ ((𝐹 ∈ DivRing ∧ 𝐴 ∈ 𝐾 ∧ 𝐴 ≠ 0 ) →
((invr‘𝐹)‘𝐴) ∈ 𝐾) |
21 | 5, 7, 8, 20 | syl3anc 1372 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐴 · 𝑋) ∈ 𝑈) ∧ 𝐴 ≠ 0 ) →
((invr‘𝐹)‘𝐴) ∈ 𝐾) |
22 | | lssvs0or.x |
. . . . . . . . . 10
⊢ (𝜑 → 𝑋 ∈ 𝑉) |
23 | 22 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝐴 · 𝑋) ∈ 𝑈) ∧ 𝐴 ≠ 0 ) → 𝑋 ∈ 𝑉) |
24 | | lssvs0or.v |
. . . . . . . . . 10
⊢ 𝑉 = (Base‘𝑊) |
25 | | lssvs0or.t |
. . . . . . . . . 10
⊢ · = (
·𝑠 ‘𝑊) |
26 | 24, 2, 25, 9, 11 | lmodvsass 19791 |
. . . . . . . . 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 19794 |
. . . . . . . . 9
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → ((1r‘𝐹) · 𝑋) = 𝑋) |
29 | 19, 23, 28 | syl2anc 587 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐴 · 𝑋) ∈ 𝑈) ∧ 𝐴 ≠ 0 ) →
((1r‘𝐹)
·
𝑋) = 𝑋) |
30 | 16, 27, 29 | 3eqtr3rd 2783 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝐴 · 𝑋) ∈ 𝑈) ∧ 𝐴 ≠ 0 ) → 𝑋 = (((invr‘𝐹)‘𝐴) · (𝐴 · 𝑋))) |
31 | | lssvs0or.u |
. . . . . . . . 9
⊢ (𝜑 → 𝑈 ∈ 𝑆) |
32 | 31 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐴 · 𝑋) ∈ 𝑈) ∧ 𝐴 ≠ 0 ) → 𝑈 ∈ 𝑆) |
33 | | simplr 769 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝐴 · 𝑋) ∈ 𝑈) ∧ 𝐴 ≠ 0 ) → (𝐴 · 𝑋) ∈ 𝑈) |
34 | | lssvs0or.s |
. . . . . . . . 9
⊢ 𝑆 = (LSubSp‘𝑊) |
35 | 2, 25, 9, 34 | lssvscl 19859 |
. . . . . . . 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 416 |
. . . . 5
⊢ ((𝜑 ∧ (𝐴 · 𝑋) ∈ 𝑈) → (𝐴 ≠ 0 → 𝑋 ∈ 𝑈)) |
39 | 38 | necon1bd 2953 |
. . . 4
⊢ ((𝜑 ∧ (𝐴 · 𝑋) ∈ 𝑈) → (¬ 𝑋 ∈ 𝑈 → 𝐴 = 0 )) |
40 | 39 | orrd 862 |
. . 3
⊢ ((𝜑 ∧ (𝐴 · 𝑋) ∈ 𝑈) → (𝑋 ∈ 𝑈 ∨ 𝐴 = 0 )) |
41 | 40 | orcomd 870 |
. 2
⊢ ((𝜑 ∧ (𝐴 · 𝑋) ∈ 𝑈) → (𝐴 = 0 ∨ 𝑋 ∈ 𝑈)) |
42 | | oveq1 7190 |
. . . . 5
⊢ (𝐴 = 0 → (𝐴 · 𝑋) = ( 0 · 𝑋)) |
43 | 42 | adantl 485 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 = 0 ) → (𝐴 · 𝑋) = ( 0 · 𝑋)) |
44 | | eqid 2739 |
. . . . . . . 8
⊢
(0g‘𝑊) = (0g‘𝑊) |
45 | 24, 2, 25, 10, 44 | lmod0vs 19799 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉) → ( 0 · 𝑋) = (0g‘𝑊)) |
46 | 18, 22, 45 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → ( 0 · 𝑋) = (0g‘𝑊)) |
47 | 44, 34 | lss0cl 19850 |
. . . . . . 7
⊢ ((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) → (0g‘𝑊) ∈ 𝑈) |
48 | 18, 31, 47 | syl2anc 587 |
. . . . . 6
⊢ (𝜑 → (0g‘𝑊) ∈ 𝑈) |
49 | 46, 48 | eqeltrd 2834 |
. . . . 5
⊢ (𝜑 → ( 0 · 𝑋) ∈ 𝑈) |
50 | 49 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 = 0 ) → ( 0 · 𝑋) ∈ 𝑈) |
51 | 43, 50 | eqeltrd 2834 |
. . 3
⊢ ((𝜑 ∧ 𝐴 = 0 ) → (𝐴 · 𝑋) ∈ 𝑈) |
52 | 18 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑈) → 𝑊 ∈ LMod) |
53 | 31 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑈) → 𝑈 ∈ 𝑆) |
54 | 6 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑈) → 𝐴 ∈ 𝐾) |
55 | | simpr 488 |
. . . 4
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑈) → 𝑋 ∈ 𝑈) |
56 | 2, 25, 9, 34 | lssvscl 19859 |
. . . 4
⊢ (((𝑊 ∈ LMod ∧ 𝑈 ∈ 𝑆) ∧ (𝐴 ∈ 𝐾 ∧ 𝑋 ∈ 𝑈)) → (𝐴 · 𝑋) ∈ 𝑈) |
57 | 52, 53, 54, 55, 56 | syl22anc 838 |
. . 3
⊢ ((𝜑 ∧ 𝑋 ∈ 𝑈) → (𝐴 · 𝑋) ∈ 𝑈) |
58 | 51, 57 | jaodan 957 |
. 2
⊢ ((𝜑 ∧ (𝐴 = 0 ∨ 𝑋 ∈ 𝑈)) → (𝐴 · 𝑋) ∈ 𝑈) |
59 | 41, 58 | impbida 801 |
1
⊢ (𝜑 → ((𝐴 · 𝑋) ∈ 𝑈 ↔ (𝐴 = 0 ∨ 𝑋 ∈ 𝑈))) |