Proof of Theorem cvsi
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | df-cvs 25158 | . . 3
⊢
ℂVec = (ℂMod ∩ LVec) | 
| 2 | 1 | elin2 4202 | . 2
⊢ (𝑊 ∈ ℂVec ↔ (𝑊 ∈ ℂMod ∧ 𝑊 ∈ LVec)) | 
| 3 |  | lveclmod 21106 | . . . . 5
⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod) | 
| 4 |  | lmodabl 20908 | . . . . 5
⊢ (𝑊 ∈ LMod → 𝑊 ∈ Abel) | 
| 5 | 3, 4 | syl 17 | . . . 4
⊢ (𝑊 ∈ LVec → 𝑊 ∈ Abel) | 
| 6 | 5 | adantl 481 | . . 3
⊢ ((𝑊 ∈ ℂMod ∧ 𝑊 ∈ LVec) → 𝑊 ∈ Abel) | 
| 7 |  | eqid 2736 | . . . . . 6
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) | 
| 8 |  | cvsi.s | . . . . . 6
⊢ 𝑆 =
(Base‘(Scalar‘𝑊)) | 
| 9 | 7, 8 | clmsscn 25113 | . . . . 5
⊢ (𝑊 ∈ ℂMod → 𝑆 ⊆
ℂ) | 
| 10 |  | clmlmod 25101 | . . . . . 6
⊢ (𝑊 ∈ ℂMod → 𝑊 ∈ LMod) | 
| 11 |  | cvsi.x | . . . . . . 7
⊢ 𝑋 = (Base‘𝑊) | 
| 12 |  | cvsi.m | . . . . . . 7
⊢  ∙ = (
·sf ‘𝑊) | 
| 13 | 11, 7, 8, 12 | lmodscaf 20883 | . . . . . 6
⊢ (𝑊 ∈ LMod → ∙
:(𝑆 × 𝑋)⟶𝑋) | 
| 14 | 10, 13 | syl 17 | . . . . 5
⊢ (𝑊 ∈ ℂMod → ∙
:(𝑆 × 𝑋)⟶𝑋) | 
| 15 | 9, 14 | jca 511 | . . . 4
⊢ (𝑊 ∈ ℂMod → (𝑆 ⊆ ℂ ∧ ∙
:(𝑆 × 𝑋)⟶𝑋)) | 
| 16 | 15 | adantr 480 | . . 3
⊢ ((𝑊 ∈ ℂMod ∧ 𝑊 ∈ LVec) → (𝑆 ⊆ ℂ ∧ ∙
:(𝑆 × 𝑋)⟶𝑋)) | 
| 17 |  | cvsi.t | . . . . . . 7
⊢  · = (
·𝑠 ‘𝑊) | 
| 18 | 11, 17 | clmvs1 25127 | . . . . . 6
⊢ ((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) → (1 · 𝑥) = 𝑥) | 
| 19 | 10 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) → 𝑊 ∈ LMod) | 
| 20 | 19 | ad2antrr 726 | . . . . . . . . . 10
⊢ ((((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑋) → 𝑊 ∈ LMod) | 
| 21 |  | simplr 768 | . . . . . . . . . 10
⊢ ((((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑋) → 𝑦 ∈ 𝑆) | 
| 22 |  | simpllr 775 | . . . . . . . . . 10
⊢ ((((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑋) → 𝑥 ∈ 𝑋) | 
| 23 |  | simpr 484 | . . . . . . . . . 10
⊢ ((((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑋) → 𝑧 ∈ 𝑋) | 
| 24 |  | cvsi.a | . . . . . . . . . . 11
⊢  + =
(+g‘𝑊) | 
| 25 | 11, 24, 7, 17, 8 | lmodvsdi 20884 | . . . . . . . . . 10
⊢ ((𝑊 ∈ LMod ∧ (𝑦 ∈ 𝑆 ∧ 𝑥 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋)) → (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) | 
| 26 | 20, 21, 22, 23, 25 | syl13anc 1373 | . . . . . . . . 9
⊢ ((((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑋) → (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) | 
| 27 | 26 | ralrimiva 3145 | . . . . . . . 8
⊢ (((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑆) → ∀𝑧 ∈ 𝑋 (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧))) | 
| 28 | 7 | clmadd 25108 | . . . . . . . . . . . . . 14
⊢ (𝑊 ∈ ℂMod → + =
(+g‘(Scalar‘𝑊))) | 
| 29 | 28 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑆) → + =
(+g‘(Scalar‘𝑊))) | 
| 30 | 29 | oveqdr 7460 | . . . . . . . . . . . 12
⊢ ((((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑆) → (𝑦 + 𝑧) = (𝑦(+g‘(Scalar‘𝑊))𝑧)) | 
| 31 | 30 | oveq1d 7447 | . . . . . . . . . . 11
⊢ ((((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑆) → ((𝑦 + 𝑧) · 𝑥) = ((𝑦(+g‘(Scalar‘𝑊))𝑧) · 𝑥)) | 
| 32 | 19 | ad2antrr 726 | . . . . . . . . . . . 12
⊢ ((((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑆) → 𝑊 ∈ LMod) | 
| 33 |  | simplr 768 | . . . . . . . . . . . 12
⊢ ((((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑆) → 𝑦 ∈ 𝑆) | 
| 34 |  | simpr 484 | . . . . . . . . . . . 12
⊢ ((((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑆) → 𝑧 ∈ 𝑆) | 
| 35 |  | simpllr 775 | . . . . . . . . . . . 12
⊢ ((((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑆) → 𝑥 ∈ 𝑋) | 
| 36 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢
(+g‘(Scalar‘𝑊)) =
(+g‘(Scalar‘𝑊)) | 
| 37 | 11, 24, 7, 17, 8, 36 | lmodvsdir 20885 | . . . . . . . . . . . 12
⊢ ((𝑊 ∈ LMod ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ∧ 𝑥 ∈ 𝑋)) → ((𝑦(+g‘(Scalar‘𝑊))𝑧) · 𝑥) = ((𝑦 · 𝑥) + (𝑧 · 𝑥))) | 
| 38 | 32, 33, 34, 35, 37 | syl13anc 1373 | . . . . . . . . . . 11
⊢ ((((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑆) → ((𝑦(+g‘(Scalar‘𝑊))𝑧) · 𝑥) = ((𝑦 · 𝑥) + (𝑧 · 𝑥))) | 
| 39 | 31, 38 | eqtrd 2776 | . . . . . . . . . 10
⊢ ((((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑆) → ((𝑦 + 𝑧) · 𝑥) = ((𝑦 · 𝑥) + (𝑧 · 𝑥))) | 
| 40 | 7 | clmmul 25109 | . . . . . . . . . . . . . 14
⊢ (𝑊 ∈ ℂMod →
· = (.r‘(Scalar‘𝑊))) | 
| 41 | 40 | ad2antrr 726 | . . . . . . . . . . . . 13
⊢ (((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑆) → · =
(.r‘(Scalar‘𝑊))) | 
| 42 | 41 | oveqdr 7460 | . . . . . . . . . . . 12
⊢ ((((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑆) → (𝑦 · 𝑧) = (𝑦(.r‘(Scalar‘𝑊))𝑧)) | 
| 43 | 42 | oveq1d 7447 | . . . . . . . . . . 11
⊢ ((((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑆) → ((𝑦 · 𝑧) · 𝑥) = ((𝑦(.r‘(Scalar‘𝑊))𝑧) · 𝑥)) | 
| 44 |  | eqid 2736 | . . . . . . . . . . . . 13
⊢
(.r‘(Scalar‘𝑊)) =
(.r‘(Scalar‘𝑊)) | 
| 45 | 11, 7, 17, 8, 44 | lmodvsass 20886 | . . . . . . . . . . . 12
⊢ ((𝑊 ∈ LMod ∧ (𝑦 ∈ 𝑆 ∧ 𝑧 ∈ 𝑆 ∧ 𝑥 ∈ 𝑋)) → ((𝑦(.r‘(Scalar‘𝑊))𝑧) · 𝑥) = (𝑦 · (𝑧 · 𝑥))) | 
| 46 | 32, 33, 34, 35, 45 | syl13anc 1373 | . . . . . . . . . . 11
⊢ ((((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑆) → ((𝑦(.r‘(Scalar‘𝑊))𝑧) · 𝑥) = (𝑦 · (𝑧 · 𝑥))) | 
| 47 | 43, 46 | eqtrd 2776 | . . . . . . . . . 10
⊢ ((((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑆) → ((𝑦 · 𝑧) · 𝑥) = (𝑦 · (𝑧 · 𝑥))) | 
| 48 | 39, 47 | jca 511 | . . . . . . . . 9
⊢ ((((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑆) ∧ 𝑧 ∈ 𝑆) → (((𝑦 + 𝑧) · 𝑥) = ((𝑦 · 𝑥) + (𝑧 · 𝑥)) ∧ ((𝑦 · 𝑧) · 𝑥) = (𝑦 · (𝑧 · 𝑥)))) | 
| 49 | 48 | ralrimiva 3145 | . . . . . . . 8
⊢ (((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑆) → ∀𝑧 ∈ 𝑆 (((𝑦 + 𝑧) · 𝑥) = ((𝑦 · 𝑥) + (𝑧 · 𝑥)) ∧ ((𝑦 · 𝑧) · 𝑥) = (𝑦 · (𝑧 · 𝑥)))) | 
| 50 | 27, 49 | jca 511 | . . . . . . 7
⊢ (((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) ∧ 𝑦 ∈ 𝑆) → (∀𝑧 ∈ 𝑋 (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ∀𝑧 ∈ 𝑆 (((𝑦 + 𝑧) · 𝑥) = ((𝑦 · 𝑥) + (𝑧 · 𝑥)) ∧ ((𝑦 · 𝑧) · 𝑥) = (𝑦 · (𝑧 · 𝑥))))) | 
| 51 | 50 | ralrimiva 3145 | . . . . . 6
⊢ ((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) → ∀𝑦 ∈ 𝑆 (∀𝑧 ∈ 𝑋 (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ∀𝑧 ∈ 𝑆 (((𝑦 + 𝑧) · 𝑥) = ((𝑦 · 𝑥) + (𝑧 · 𝑥)) ∧ ((𝑦 · 𝑧) · 𝑥) = (𝑦 · (𝑧 · 𝑥))))) | 
| 52 | 18, 51 | jca 511 | . . . . 5
⊢ ((𝑊 ∈ ℂMod ∧ 𝑥 ∈ 𝑋) → ((1 · 𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑆 (∀𝑧 ∈ 𝑋 (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ∀𝑧 ∈ 𝑆 (((𝑦 + 𝑧) · 𝑥) = ((𝑦 · 𝑥) + (𝑧 · 𝑥)) ∧ ((𝑦 · 𝑧) · 𝑥) = (𝑦 · (𝑧 · 𝑥)))))) | 
| 53 | 52 | ralrimiva 3145 | . . . 4
⊢ (𝑊 ∈ ℂMod →
∀𝑥 ∈ 𝑋 ((1 · 𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑆 (∀𝑧 ∈ 𝑋 (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ∀𝑧 ∈ 𝑆 (((𝑦 + 𝑧) · 𝑥) = ((𝑦 · 𝑥) + (𝑧 · 𝑥)) ∧ ((𝑦 · 𝑧) · 𝑥) = (𝑦 · (𝑧 · 𝑥)))))) | 
| 54 | 53 | adantr 480 | . . 3
⊢ ((𝑊 ∈ ℂMod ∧ 𝑊 ∈ LVec) →
∀𝑥 ∈ 𝑋 ((1 · 𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑆 (∀𝑧 ∈ 𝑋 (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ∀𝑧 ∈ 𝑆 (((𝑦 + 𝑧) · 𝑥) = ((𝑦 · 𝑥) + (𝑧 · 𝑥)) ∧ ((𝑦 · 𝑧) · 𝑥) = (𝑦 · (𝑧 · 𝑥)))))) | 
| 55 | 6, 16, 54 | 3jca 1128 | . 2
⊢ ((𝑊 ∈ ℂMod ∧ 𝑊 ∈ LVec) → (𝑊 ∈ Abel ∧ (𝑆 ⊆ ℂ ∧ ∙
:(𝑆 × 𝑋)⟶𝑋) ∧ ∀𝑥 ∈ 𝑋 ((1 · 𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑆 (∀𝑧 ∈ 𝑋 (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ∀𝑧 ∈ 𝑆 (((𝑦 + 𝑧) · 𝑥) = ((𝑦 · 𝑥) + (𝑧 · 𝑥)) ∧ ((𝑦 · 𝑧) · 𝑥) = (𝑦 · (𝑧 · 𝑥))))))) | 
| 56 | 2, 55 | sylbi 217 | 1
⊢ (𝑊 ∈ ℂVec → (𝑊 ∈ Abel ∧ (𝑆 ⊆ ℂ ∧ ∙
:(𝑆 × 𝑋)⟶𝑋) ∧ ∀𝑥 ∈ 𝑋 ((1 · 𝑥) = 𝑥 ∧ ∀𝑦 ∈ 𝑆 (∀𝑧 ∈ 𝑋 (𝑦 · (𝑥 + 𝑧)) = ((𝑦 · 𝑥) + (𝑦 · 𝑧)) ∧ ∀𝑧 ∈ 𝑆 (((𝑦 + 𝑧) · 𝑥) = ((𝑦 · 𝑥) + (𝑧 · 𝑥)) ∧ ((𝑦 · 𝑧) · 𝑥) = (𝑦 · (𝑧 · 𝑥))))))) |