Proof of Theorem isncvsngp
Step | Hyp | Ref
| Expression |
1 | | isnvc 22309 |
. . . . . 6
⊢ (𝑊 ∈ NrmVec ↔ (𝑊 ∈ NrmMod ∧ 𝑊 ∈ LVec)) |
2 | | ancom 465 |
. . . . . 6
⊢ ((𝑊 ∈ NrmMod ∧ 𝑊 ∈ LVec) ↔ (𝑊 ∈ LVec ∧ 𝑊 ∈
NrmMod)) |
3 | 1, 2 | bitri 263 |
. . . . 5
⊢ (𝑊 ∈ NrmVec ↔ (𝑊 ∈ LVec ∧ 𝑊 ∈
NrmMod)) |
4 | 3 | a1i 11 |
. . . 4
⊢ (𝑊 ∈ ℂVec → (𝑊 ∈ NrmVec ↔ (𝑊 ∈ LVec ∧ 𝑊 ∈
NrmMod))) |
5 | | id 22 |
. . . . . 6
⊢ (𝑊 ∈ ℂVec → 𝑊 ∈
ℂVec) |
6 | 5 | cvslvec 22733 |
. . . . 5
⊢ (𝑊 ∈ ℂVec → 𝑊 ∈ LVec) |
7 | 6 | biantrurd 528 |
. . . 4
⊢ (𝑊 ∈ ℂVec → (𝑊 ∈ NrmMod ↔ (𝑊 ∈ LVec ∧ 𝑊 ∈
NrmMod))) |
8 | 5 | cvsclm 22734 |
. . . . 5
⊢ (𝑊 ∈ ℂVec → 𝑊 ∈
ℂMod) |
9 | | isncvsngp.v |
. . . . . . 7
⊢ 𝑉 = (Base‘𝑊) |
10 | | isncvsngp.n |
. . . . . . 7
⊢ 𝑁 = (norm‘𝑊) |
11 | | isncvsngp.s |
. . . . . . 7
⊢ · = (
·𝑠 ‘𝑊) |
12 | | isncvsngp.f |
. . . . . . 7
⊢ 𝐹 = (Scalar‘𝑊) |
13 | | isncvsngp.k |
. . . . . . 7
⊢ 𝐾 = (Base‘𝐹) |
14 | | eqid 2610 |
. . . . . . 7
⊢
(norm‘𝐹) =
(norm‘𝐹) |
15 | 9, 10, 11, 12, 13, 14 | isnlm 22289 |
. . . . . 6
⊢ (𝑊 ∈ NrmMod ↔ ((𝑊 ∈ NrmGrp ∧ 𝑊 ∈ LMod ∧ 𝐹 ∈ NrmRing) ∧
∀𝑘 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝑁‘(𝑘 · 𝑥)) = (((norm‘𝐹)‘𝑘) · (𝑁‘𝑥)))) |
16 | | 3anass 1035 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ NrmGrp ∧ 𝑊 ∈ LMod ∧ 𝐹 ∈ NrmRing) ↔ (𝑊 ∈ NrmGrp ∧ (𝑊 ∈ LMod ∧ 𝐹 ∈
NrmRing))) |
17 | | ancom 465 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ NrmGrp ∧ (𝑊 ∈ LMod ∧ 𝐹 ∈ NrmRing)) ↔ ((𝑊 ∈ LMod ∧ 𝐹 ∈ NrmRing) ∧ 𝑊 ∈
NrmGrp)) |
18 | 16, 17 | bitri 263 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ NrmGrp ∧ 𝑊 ∈ LMod ∧ 𝐹 ∈ NrmRing) ↔ ((𝑊 ∈ LMod ∧ 𝐹 ∈ NrmRing) ∧ 𝑊 ∈
NrmGrp)) |
19 | 18 | anbi1i 727 |
. . . . . . . . 9
⊢ (((𝑊 ∈ NrmGrp ∧ 𝑊 ∈ LMod ∧ 𝐹 ∈ NrmRing) ∧
∀𝑘 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝑁‘(𝑘 · 𝑥)) = (((norm‘𝐹)‘𝑘) · (𝑁‘𝑥))) ↔ (((𝑊 ∈ LMod ∧ 𝐹 ∈ NrmRing) ∧ 𝑊 ∈ NrmGrp) ∧ ∀𝑘 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝑁‘(𝑘 · 𝑥)) = (((norm‘𝐹)‘𝑘) · (𝑁‘𝑥)))) |
20 | | anass 679 |
. . . . . . . . 9
⊢ ((((𝑊 ∈ LMod ∧ 𝐹 ∈ NrmRing) ∧ 𝑊 ∈ NrmGrp) ∧
∀𝑘 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝑁‘(𝑘 · 𝑥)) = (((norm‘𝐹)‘𝑘) · (𝑁‘𝑥))) ↔ ((𝑊 ∈ LMod ∧ 𝐹 ∈ NrmRing) ∧ (𝑊 ∈ NrmGrp ∧ ∀𝑘 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝑁‘(𝑘 · 𝑥)) = (((norm‘𝐹)‘𝑘) · (𝑁‘𝑥))))) |
21 | 19, 20 | bitri 263 |
. . . . . . . 8
⊢ (((𝑊 ∈ NrmGrp ∧ 𝑊 ∈ LMod ∧ 𝐹 ∈ NrmRing) ∧
∀𝑘 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝑁‘(𝑘 · 𝑥)) = (((norm‘𝐹)‘𝑘) · (𝑁‘𝑥))) ↔ ((𝑊 ∈ LMod ∧ 𝐹 ∈ NrmRing) ∧ (𝑊 ∈ NrmGrp ∧ ∀𝑘 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝑁‘(𝑘 · 𝑥)) = (((norm‘𝐹)‘𝑘) · (𝑁‘𝑥))))) |
22 | 21 | a1i 11 |
. . . . . . 7
⊢ (𝑊 ∈ ℂMod →
(((𝑊 ∈ NrmGrp ∧
𝑊 ∈ LMod ∧ 𝐹 ∈ NrmRing) ∧
∀𝑘 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝑁‘(𝑘 · 𝑥)) = (((norm‘𝐹)‘𝑘) · (𝑁‘𝑥))) ↔ ((𝑊 ∈ LMod ∧ 𝐹 ∈ NrmRing) ∧ (𝑊 ∈ NrmGrp ∧ ∀𝑘 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝑁‘(𝑘 · 𝑥)) = (((norm‘𝐹)‘𝑘) · (𝑁‘𝑥)))))) |
23 | | clmlmod 22675 |
. . . . . . . . 9
⊢ (𝑊 ∈ ℂMod → 𝑊 ∈ LMod) |
24 | 12, 13 | clmsca 22673 |
. . . . . . . . . 10
⊢ (𝑊 ∈ ℂMod → 𝐹 = (ℂfld
↾s 𝐾)) |
25 | | cnnrg 22394 |
. . . . . . . . . . 11
⊢
ℂfld ∈ NrmRing |
26 | 12, 13 | clmsubrg 22674 |
. . . . . . . . . . 11
⊢ (𝑊 ∈ ℂMod → 𝐾 ∈
(SubRing‘ℂfld)) |
27 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(ℂfld ↾s 𝐾) = (ℂfld
↾s 𝐾) |
28 | 27 | subrgnrg 22287 |
. . . . . . . . . . 11
⊢
((ℂfld ∈ NrmRing ∧ 𝐾 ∈
(SubRing‘ℂfld)) → (ℂfld
↾s 𝐾)
∈ NrmRing) |
29 | 25, 26, 28 | sylancr 694 |
. . . . . . . . . 10
⊢ (𝑊 ∈ ℂMod →
(ℂfld ↾s 𝐾) ∈ NrmRing) |
30 | 24, 29 | eqeltrd 2688 |
. . . . . . . . 9
⊢ (𝑊 ∈ ℂMod → 𝐹 ∈
NrmRing) |
31 | 23, 30 | jca 553 |
. . . . . . . 8
⊢ (𝑊 ∈ ℂMod → (𝑊 ∈ LMod ∧ 𝐹 ∈
NrmRing)) |
32 | 31 | biantrurd 528 |
. . . . . . 7
⊢ (𝑊 ∈ ℂMod →
((𝑊 ∈ NrmGrp ∧
∀𝑘 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝑁‘(𝑘 · 𝑥)) = (((norm‘𝐹)‘𝑘) · (𝑁‘𝑥))) ↔ ((𝑊 ∈ LMod ∧ 𝐹 ∈ NrmRing) ∧ (𝑊 ∈ NrmGrp ∧ ∀𝑘 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝑁‘(𝑘 · 𝑥)) = (((norm‘𝐹)‘𝑘) · (𝑁‘𝑥)))))) |
33 | | ralcom 3079 |
. . . . . . . . 9
⊢
(∀𝑘 ∈
𝐾 ∀𝑥 ∈ 𝑉 (𝑁‘(𝑘 · 𝑥)) = (((norm‘𝐹)‘𝑘) · (𝑁‘𝑥)) ↔ ∀𝑥 ∈ 𝑉 ∀𝑘 ∈ 𝐾 (𝑁‘(𝑘 · 𝑥)) = (((norm‘𝐹)‘𝑘) · (𝑁‘𝑥))) |
34 | 24 | fveq2d 6107 |
. . . . . . . . . . . . . . . 16
⊢ (𝑊 ∈ ℂMod →
(norm‘𝐹) =
(norm‘(ℂfld ↾s 𝐾))) |
35 | | subrgsubg 18609 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐾 ∈
(SubRing‘ℂfld) → 𝐾 ∈
(SubGrp‘ℂfld)) |
36 | | eqid 2610 |
. . . . . . . . . . . . . . . . . 18
⊢
(norm‘ℂfld) =
(norm‘ℂfld) |
37 | | eqid 2610 |
. . . . . . . . . . . . . . . . . 18
⊢
(norm‘(ℂfld ↾s 𝐾)) = (norm‘(ℂfld
↾s 𝐾)) |
38 | 27, 36, 37 | subgnm 22247 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐾 ∈
(SubGrp‘ℂfld) → (norm‘(ℂfld
↾s 𝐾)) =
((norm‘ℂfld) ↾ 𝐾)) |
39 | 26, 35, 38 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ (𝑊 ∈ ℂMod →
(norm‘(ℂfld ↾s 𝐾)) = ((norm‘ℂfld)
↾ 𝐾)) |
40 | 34, 39 | eqtrd 2644 |
. . . . . . . . . . . . . . 15
⊢ (𝑊 ∈ ℂMod →
(norm‘𝐹) =
((norm‘ℂfld) ↾ 𝐾)) |
41 | 40 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ ℂMod ∧ (𝑥 ∈ 𝑉 ∧ 𝑘 ∈ 𝐾)) → (norm‘𝐹) = ((norm‘ℂfld)
↾ 𝐾)) |
42 | 41 | fveq1d 6105 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ ℂMod ∧ (𝑥 ∈ 𝑉 ∧ 𝑘 ∈ 𝐾)) → ((norm‘𝐹)‘𝑘) = (((norm‘ℂfld)
↾ 𝐾)‘𝑘)) |
43 | | cnfldnm 22392 |
. . . . . . . . . . . . . . . . 17
⊢ abs =
(norm‘ℂfld) |
44 | 43 | eqcomi 2619 |
. . . . . . . . . . . . . . . 16
⊢
(norm‘ℂfld) = abs |
45 | 44 | reseq1i 5313 |
. . . . . . . . . . . . . . 15
⊢
((norm‘ℂfld) ↾ 𝐾) = (abs ↾ 𝐾) |
46 | 45 | fveq1i 6104 |
. . . . . . . . . . . . . 14
⊢
(((norm‘ℂfld) ↾ 𝐾)‘𝑘) = ((abs ↾ 𝐾)‘𝑘) |
47 | | fvres 6117 |
. . . . . . . . . . . . . . 15
⊢ (𝑘 ∈ 𝐾 → ((abs ↾ 𝐾)‘𝑘) = (abs‘𝑘)) |
48 | 47 | ad2antll 761 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ ℂMod ∧ (𝑥 ∈ 𝑉 ∧ 𝑘 ∈ 𝐾)) → ((abs ↾ 𝐾)‘𝑘) = (abs‘𝑘)) |
49 | 46, 48 | syl5eq 2656 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ ℂMod ∧ (𝑥 ∈ 𝑉 ∧ 𝑘 ∈ 𝐾)) →
(((norm‘ℂfld) ↾ 𝐾)‘𝑘) = (abs‘𝑘)) |
50 | 42, 49 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ ((𝑊 ∈ ℂMod ∧ (𝑥 ∈ 𝑉 ∧ 𝑘 ∈ 𝐾)) → ((norm‘𝐹)‘𝑘) = (abs‘𝑘)) |
51 | 50 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ ℂMod ∧ (𝑥 ∈ 𝑉 ∧ 𝑘 ∈ 𝐾)) → (((norm‘𝐹)‘𝑘) · (𝑁‘𝑥)) = ((abs‘𝑘) · (𝑁‘𝑥))) |
52 | 51 | eqeq2d 2620 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ ℂMod ∧ (𝑥 ∈ 𝑉 ∧ 𝑘 ∈ 𝐾)) → ((𝑁‘(𝑘 · 𝑥)) = (((norm‘𝐹)‘𝑘) · (𝑁‘𝑥)) ↔ (𝑁‘(𝑘 · 𝑥)) = ((abs‘𝑘) · (𝑁‘𝑥)))) |
53 | 52 | 2ralbidva 2971 |
. . . . . . . . 9
⊢ (𝑊 ∈ ℂMod →
(∀𝑥 ∈ 𝑉 ∀𝑘 ∈ 𝐾 (𝑁‘(𝑘 · 𝑥)) = (((norm‘𝐹)‘𝑘) · (𝑁‘𝑥)) ↔ ∀𝑥 ∈ 𝑉 ∀𝑘 ∈ 𝐾 (𝑁‘(𝑘 · 𝑥)) = ((abs‘𝑘) · (𝑁‘𝑥)))) |
54 | 33, 53 | syl5bb 271 |
. . . . . . . 8
⊢ (𝑊 ∈ ℂMod →
(∀𝑘 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝑁‘(𝑘 · 𝑥)) = (((norm‘𝐹)‘𝑘) · (𝑁‘𝑥)) ↔ ∀𝑥 ∈ 𝑉 ∀𝑘 ∈ 𝐾 (𝑁‘(𝑘 · 𝑥)) = ((abs‘𝑘) · (𝑁‘𝑥)))) |
55 | 54 | anbi2d 736 |
. . . . . . 7
⊢ (𝑊 ∈ ℂMod →
((𝑊 ∈ NrmGrp ∧
∀𝑘 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝑁‘(𝑘 · 𝑥)) = (((norm‘𝐹)‘𝑘) · (𝑁‘𝑥))) ↔ (𝑊 ∈ NrmGrp ∧ ∀𝑥 ∈ 𝑉 ∀𝑘 ∈ 𝐾 (𝑁‘(𝑘 · 𝑥)) = ((abs‘𝑘) · (𝑁‘𝑥))))) |
56 | 22, 32, 55 | 3bitr2d 295 |
. . . . . 6
⊢ (𝑊 ∈ ℂMod →
(((𝑊 ∈ NrmGrp ∧
𝑊 ∈ LMod ∧ 𝐹 ∈ NrmRing) ∧
∀𝑘 ∈ 𝐾 ∀𝑥 ∈ 𝑉 (𝑁‘(𝑘 · 𝑥)) = (((norm‘𝐹)‘𝑘) · (𝑁‘𝑥))) ↔ (𝑊 ∈ NrmGrp ∧ ∀𝑥 ∈ 𝑉 ∀𝑘 ∈ 𝐾 (𝑁‘(𝑘 · 𝑥)) = ((abs‘𝑘) · (𝑁‘𝑥))))) |
57 | 15, 56 | syl5bb 271 |
. . . . 5
⊢ (𝑊 ∈ ℂMod → (𝑊 ∈ NrmMod ↔ (𝑊 ∈ NrmGrp ∧
∀𝑥 ∈ 𝑉 ∀𝑘 ∈ 𝐾 (𝑁‘(𝑘 · 𝑥)) = ((abs‘𝑘) · (𝑁‘𝑥))))) |
58 | 8, 57 | syl 17 |
. . . 4
⊢ (𝑊 ∈ ℂVec → (𝑊 ∈ NrmMod ↔ (𝑊 ∈ NrmGrp ∧
∀𝑥 ∈ 𝑉 ∀𝑘 ∈ 𝐾 (𝑁‘(𝑘 · 𝑥)) = ((abs‘𝑘) · (𝑁‘𝑥))))) |
59 | 4, 7, 58 | 3bitr2d 295 |
. . 3
⊢ (𝑊 ∈ ℂVec → (𝑊 ∈ NrmVec ↔ (𝑊 ∈ NrmGrp ∧
∀𝑥 ∈ 𝑉 ∀𝑘 ∈ 𝐾 (𝑁‘(𝑘 · 𝑥)) = ((abs‘𝑘) · (𝑁‘𝑥))))) |
60 | 59 | pm5.32i 667 |
. 2
⊢ ((𝑊 ∈ ℂVec ∧ 𝑊 ∈ NrmVec) ↔ (𝑊 ∈ ℂVec ∧ (𝑊 ∈ NrmGrp ∧
∀𝑥 ∈ 𝑉 ∀𝑘 ∈ 𝐾 (𝑁‘(𝑘 · 𝑥)) = ((abs‘𝑘) · (𝑁‘𝑥))))) |
61 | | elin 3758 |
. . 3
⊢ (𝑊 ∈ (NrmVec ∩
ℂVec) ↔ (𝑊
∈ NrmVec ∧ 𝑊
∈ ℂVec)) |
62 | | ancom 465 |
. . 3
⊢ ((𝑊 ∈ NrmVec ∧ 𝑊 ∈ ℂVec) ↔
(𝑊 ∈ ℂVec ∧
𝑊 ∈
NrmVec)) |
63 | 61, 62 | bitri 263 |
. 2
⊢ (𝑊 ∈ (NrmVec ∩
ℂVec) ↔ (𝑊
∈ ℂVec ∧ 𝑊
∈ NrmVec)) |
64 | | 3anass 1035 |
. 2
⊢ ((𝑊 ∈ ℂVec ∧ 𝑊 ∈ NrmGrp ∧
∀𝑥 ∈ 𝑉 ∀𝑘 ∈ 𝐾 (𝑁‘(𝑘 · 𝑥)) = ((abs‘𝑘) · (𝑁‘𝑥))) ↔ (𝑊 ∈ ℂVec ∧ (𝑊 ∈ NrmGrp ∧ ∀𝑥 ∈ 𝑉 ∀𝑘 ∈ 𝐾 (𝑁‘(𝑘 · 𝑥)) = ((abs‘𝑘) · (𝑁‘𝑥))))) |
65 | 60, 63, 64 | 3bitr4i 291 |
1
⊢ (𝑊 ∈ (NrmVec ∩
ℂVec) ↔ (𝑊
∈ ℂVec ∧ 𝑊
∈ NrmGrp ∧ ∀𝑥 ∈ 𝑉 ∀𝑘 ∈ 𝐾 (𝑁‘(𝑘 · 𝑥)) = ((abs‘𝑘) · (𝑁‘𝑥)))) |