Proof of Theorem cvsi
Step | Hyp | Ref
| Expression |
1 | | df-cvs 22924 |
. . . 4
⊢
ℂVec = (ℂMod ∩ LVec) |
2 | 1 | eleq2i 2693 |
. . 3
⊢ (𝑊 ∈ ℂVec ↔ 𝑊 ∈ (ℂMod ∩
LVec)) |
3 | | elin 3796 |
. . 3
⊢ (𝑊 ∈ (ℂMod ∩ LVec)
↔ (𝑊 ∈ ℂMod
∧ 𝑊 ∈
LVec)) |
4 | 2, 3 | bitri 264 |
. 2
⊢ (𝑊 ∈ ℂVec ↔ (𝑊 ∈ ℂMod ∧ 𝑊 ∈ LVec)) |
5 | | lveclmod 19106 |
. . . . 5
⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod) |
6 | | lmodabl 18910 |
. . . . 5
⊢ (𝑊 ∈ LMod → 𝑊 ∈ Abel) |
7 | 5, 6 | syl 17 |
. . . 4
⊢ (𝑊 ∈ LVec → 𝑊 ∈ Abel) |
8 | 7 | adantl 482 |
. . 3
⊢ ((𝑊 ∈ ℂMod ∧ 𝑊 ∈ LVec) → 𝑊 ∈ Abel) |
9 | | eqid 2622 |
. . . . . 6
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) |
10 | | cvsi.s |
. . . . . 6
⊢ 𝑆 =
(Base‘(Scalar‘𝑊)) |
11 | 9, 10 | clmsscn 22879 |
. . . . 5
⊢ (𝑊 ∈ ℂMod → 𝑆 ⊆
ℂ) |
12 | | clmlmod 22867 |
. . . . . 6
⊢ (𝑊 ∈ ℂMod → 𝑊 ∈ LMod) |
13 | | cvsi.x |
. . . . . . 7
⊢ 𝑋 = (Base‘𝑊) |
14 | | cvsi.m |
. . . . . . 7
⊢ ∙ = (
·sf ‘𝑊) |
15 | 13, 9, 10, 14 | lmodscaf 18885 |
. . . . . 6
⊢ (𝑊 ∈ LMod → ∙
:(𝑆 × 𝑋)⟶𝑋) |
16 | 12, 15 | syl 17 |
. . . . 5
⊢ (𝑊 ∈ ℂMod → ∙
:(𝑆 × 𝑋)⟶𝑋) |
17 | 11, 16 | jca 554 |
. . . 4
⊢ (𝑊 ∈ ℂMod → (𝑆 ⊆ ℂ ∧ ∙
:(𝑆 × 𝑋)⟶𝑋)) |
18 | 17 | adantr 481 |
. . 3
⊢ ((𝑊 ∈ ℂMod ∧ 𝑊 ∈ LVec) → (𝑆 ⊆ ℂ ∧ ∙
:(𝑆 × 𝑋)⟶𝑋)) |
19 | 9 | clm1 22873 |
. . . . . . . . 9
⊢ (𝑊 ∈ ℂMod → 1 =
(1r‘(Scalar‘𝑊))) |
20 | 19 | adantr 481 |
. . . . . . . 8
⊢ ((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) → 1 =
(1r‘(Scalar‘𝑊))) |
21 | 20 | oveq1d 6665 |
. . . . . . 7
⊢ ((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) → (1 · 𝑥) = ((1r‘(Scalar‘𝑊)) · 𝑥)) |
22 | 12 | anim1i 592 |
. . . . . . . 8
⊢ ((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) → (𝑊 ∈ LMod ∧ 𝑥 ∈ 𝑋)) |
23 | | cvsi.t |
. . . . . . . . 9
⊢ · = (
·𝑠 ‘𝑊) |
24 | | eqid 2622 |
. . . . . . . . 9
⊢
(1r‘(Scalar‘𝑊)) =
(1r‘(Scalar‘𝑊)) |
25 | 13, 9, 23, 24 | lmodvs1 18891 |
. . . . . . . 8
⊢ ((𝑊 ∈ LMod ∧ 𝑥 ∈ 𝑋) →
((1r‘(Scalar‘𝑊)) · 𝑥) = 𝑥) |
26 | 22, 25 | syl 17 |
. . . . . . 7
⊢ ((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) →
((1r‘(Scalar‘𝑊)) · 𝑥) = 𝑥) |
27 | 21, 26 | eqtrd 2656 |
. . . . . 6
⊢ ((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) → (1 · 𝑥) = 𝑥) |
28 | 12 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) → 𝑊 ∈ LMod) |
29 | 28 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑆) → 𝑊 ∈ LMod) |
30 | 29 | adantr 481 |
. . . . . . . . . . 11
⊢ ((((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑋) → 𝑊 ∈ LMod) |
31 | | simplr 792 |
. . . . . . . . . . . 12
⊢ ((((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑋) → 𝑦 ∈ 𝑆) |
32 | | simpllr 799 |
. . . . . . . . . . . 12
⊢ ((((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑋) → 𝑥 ∈ 𝑋) |
33 | | simpr 477 |
. . . . . . . . . . . 12
⊢ ((((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑋) → 𝑧 ∈ 𝑋) |
34 | 31, 32, 33 | 3jca 1242 |
. . . . . . . . . . 11
⊢ ((((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑋) → (𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) |
35 | 30, 34 | jca 554 |
. . . . . . . . . 10
⊢ ((((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑋) → (𝑊 ∈ LMod ∧ (𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋))) |
36 | | cvsi.a |
. . . . . . . . . . 11
⊢ + =
(+g‘𝑊) |
37 | 13, 36, 9, 23, 10 | lmodvsdi 18886 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ LMod ∧ (𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) |
38 | 35, 37 | syl 17 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑋) → (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) |
39 | 38 | ralrimiva 2966 |
. . . . . . . 8
⊢ (((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑆) → ∀𝑧 ∈ 𝑋 (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) |
40 | 9 | clmadd 22874 |
. . . . . . . . . . . . . . . 16
⊢ (𝑊 ∈ ℂMod → + =
(+g‘(Scalar‘𝑊))) |
41 | 40 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) → + =
(+g‘(Scalar‘𝑊))) |
42 | 41 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑆) → + =
(+g‘(Scalar‘𝑊))) |
43 | 42 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑆) → + =
(+g‘(Scalar‘𝑊))) |
44 | 43 | oveqd 6667 |
. . . . . . . . . . . 12
⊢ ((((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑆) → (𝑦 + 𝑧) = (𝑦(+g‘(Scalar‘𝑊))𝑧)) |
45 | 44 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ ((((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑆) → ((𝑦 + 𝑧) · 𝑥) = ((𝑦(+g‘(Scalar‘𝑊))𝑧) · 𝑥)) |
46 | 29 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑆) → 𝑊 ∈ LMod) |
47 | | simpr 477 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑆) → 𝑦 ∈ 𝑆) |
48 | 47 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑆) → 𝑦 ∈ 𝑆) |
49 | | simpr 477 |
. . . . . . . . . . . . . 14
⊢ ((((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑆) → 𝑧 ∈ 𝑆) |
50 | | simpr 477 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) → 𝑥 ∈ 𝑋) |
51 | 50 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑆) → 𝑥 ∈ 𝑋) |
52 | 51 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑆) → 𝑥 ∈ 𝑋) |
53 | 48, 49, 52 | 3jca 1242 |
. . . . . . . . . . . . 13
⊢ ((((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑆) → (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ∧ 𝑥 ∈ 𝑋)) |
54 | 46, 53 | jca 554 |
. . . . . . . . . . . 12
⊢ ((((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑆) → (𝑊 ∈ LMod ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ∧ 𝑥 ∈ 𝑋))) |
55 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢
(+g‘(Scalar‘𝑊)) =
(+g‘(Scalar‘𝑊)) |
56 | 13, 36, 9, 23, 10, 55 | lmodvsdir 18887 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ LMod ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ∧ 𝑥 ∈ 𝑋)) → ((𝑦(+g‘(Scalar‘𝑊))𝑧) · 𝑥) = ((𝑦 · 𝑥) + (𝑧 · 𝑥))) |
57 | 54, 56 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑆) → ((𝑦(+g‘(Scalar‘𝑊))𝑧) · 𝑥) = ((𝑦 · 𝑥) + (𝑧 · 𝑥))) |
58 | 45, 57 | eqtrd 2656 |
. . . . . . . . . 10
⊢ ((((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑆) → ((𝑦 + 𝑧) · 𝑥) = ((𝑦 · 𝑥) + (𝑧 · 𝑥))) |
59 | 9 | clmmul 22875 |
. . . . . . . . . . . . . . . 16
⊢ (𝑊 ∈ ℂMod →
· = (.r‘(Scalar‘𝑊))) |
60 | 59 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) → · =
(.r‘(Scalar‘𝑊))) |
61 | 60 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑆) → · =
(.r‘(Scalar‘𝑊))) |
62 | 61 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑆) → · =
(.r‘(Scalar‘𝑊))) |
63 | 62 | oveqd 6667 |
. . . . . . . . . . . 12
⊢ ((((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑆) → (𝑦 · 𝑧) = (𝑦(.r‘(Scalar‘𝑊))𝑧)) |
64 | 63 | oveq1d 6665 |
. . . . . . . . . . 11
⊢ ((((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑆) → ((𝑦 · 𝑧) · 𝑥) = ((𝑦(.r‘(Scalar‘𝑊))𝑧) · 𝑥)) |
65 | | eqid 2622 |
. . . . . . . . . . . . 13
⊢
(.r‘(Scalar‘𝑊)) =
(.r‘(Scalar‘𝑊)) |
66 | 13, 9, 23, 10, 65 | lmodvsass 18888 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ LMod ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ∧ 𝑥 ∈ 𝑋)) → ((𝑦(.r‘(Scalar‘𝑊))𝑧) · 𝑥) = (𝑦 · (𝑧 · 𝑥))) |
67 | 54, 66 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑆) → ((𝑦(.r‘(Scalar‘𝑊))𝑧) · 𝑥) = (𝑦 · (𝑧 · 𝑥))) |
68 | 64, 67 | eqtrd 2656 |
. . . . . . . . . 10
⊢ ((((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑆) → ((𝑦 · 𝑧) · 𝑥) = (𝑦 · (𝑧 · 𝑥))) |
69 | 58, 68 | jca 554 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑆) → (((𝑦 + 𝑧) · 𝑥) = ((𝑦 · 𝑥) + (𝑧 · 𝑥)) ∧ ((𝑦 · 𝑧) · 𝑥) = (𝑦 · (𝑧 · 𝑥)))) |
70 | 69 | ralrimiva 2966 |
. . . . . . . 8
⊢ (((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑆) → ∀𝑧 ∈ 𝑆 (((𝑦 + 𝑧) · 𝑥) = ((𝑦 · 𝑥) + (𝑧 · 𝑥)) ∧ ((𝑦 · 𝑧) · 𝑥) = (𝑦 · (𝑧 · 𝑥)))) |
71 | 39, 70 | jca 554 |
. . . . . . 7
⊢ (((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑆) → (∀𝑧 ∈ 𝑋 (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ∀𝑧 ∈ 𝑆 (((𝑦 + 𝑧) · 𝑥) = ((𝑦 · 𝑥) + (𝑧 · 𝑥)) ∧ ((𝑦 · 𝑧) · 𝑥) = (𝑦 · (𝑧 · 𝑥))))) |
72 | 71 | ralrimiva 2966 |
. . . . . 6
⊢ ((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) → ∀𝑦 ∈ 𝑆 (∀𝑧 ∈ 𝑋 (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ∀𝑧 ∈ 𝑆 (((𝑦 + 𝑧) · 𝑥) = ((𝑦 · 𝑥) + (𝑧 · 𝑥)) ∧ ((𝑦 · 𝑧) · 𝑥) = (𝑦 · (𝑧 · 𝑥))))) |
73 | 27, 72 | jca 554 |
. . . . 5
⊢ ((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) → ((1 · 𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑆 (∀𝑧 ∈ 𝑋 (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ∀𝑧 ∈ 𝑆 (((𝑦 + 𝑧) · 𝑥) = ((𝑦 · 𝑥) + (𝑧 · 𝑥)) ∧ ((𝑦 · 𝑧) · 𝑥) = (𝑦 · (𝑧 · 𝑥)))))) |
74 | 73 | ralrimiva 2966 |
. . . 4
⊢ (𝑊 ∈ ℂMod →
∀𝑥 ∈ 𝑋 ((1 · 𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑆 (∀𝑧 ∈ 𝑋 (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ∀𝑧 ∈ 𝑆 (((𝑦 + 𝑧) · 𝑥) = ((𝑦 · 𝑥) + (𝑧 · 𝑥)) ∧ ((𝑦 · 𝑧) · 𝑥) = (𝑦 · (𝑧 · 𝑥)))))) |
75 | 74 | adantr 481 |
. . 3
⊢ ((𝑊 ∈ ℂMod ∧ 𝑊 ∈ LVec) →
∀𝑥 ∈ 𝑋 ((1 · 𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑆 (∀𝑧 ∈ 𝑋 (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ∀𝑧 ∈ 𝑆 (((𝑦 + 𝑧) · 𝑥) = ((𝑦 · 𝑥) + (𝑧 · 𝑥)) ∧ ((𝑦 · 𝑧) · 𝑥) = (𝑦 · (𝑧 · 𝑥)))))) |
76 | 8, 18, 75 | 3jca 1242 |
. 2
⊢ ((𝑊 ∈ ℂMod ∧ 𝑊 ∈ LVec) → (𝑊 ∈ Abel ∧ (𝑆 ⊆ ℂ ∧ ∙
:(𝑆 × 𝑋)⟶𝑋) ∧ ∀𝑥 ∈ 𝑋 ((1 · 𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑆 (∀𝑧 ∈ 𝑋 (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ∀𝑧 ∈ 𝑆 (((𝑦 + 𝑧) · 𝑥) = ((𝑦 · 𝑥) + (𝑧 · 𝑥)) ∧ ((𝑦 · 𝑧) · 𝑥) = (𝑦 · (𝑧 · 𝑥))))))) |
77 | 4, 76 | sylbi 207 |
1
⊢ (𝑊 ∈ ℂVec → (𝑊 ∈ Abel ∧ (𝑆 ⊆ ℂ ∧ ∙
:(𝑆 × 𝑋)⟶𝑋) ∧ ∀𝑥 ∈ 𝑋 ((1 · 𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑆 (∀𝑧 ∈ 𝑋 (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ∀𝑧 ∈ 𝑆 (((𝑦 + 𝑧) · 𝑥) = ((𝑦 · 𝑥) + (𝑧 · 𝑥)) ∧ ((𝑦 · 𝑧) · 𝑥) = (𝑦 · (𝑧 · 𝑥))))))) |