Step | Hyp | Ref
| Expression |
1 | | fvexd 6689 |
. . . 4
⊢ (𝑤 = 𝑊 → (Scalar‘𝑤) ∈ V) |
2 | | fvexd 6689 |
. . . . 5
⊢ ((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) → (Base‘𝑓) ∈ V) |
3 | | id 22 |
. . . . . . . . 9
⊢ (𝑓 = (Scalar‘𝑤) → 𝑓 = (Scalar‘𝑤)) |
4 | | fveq2 6674 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑊 → (Scalar‘𝑤) = (Scalar‘𝑊)) |
5 | | isclm.f |
. . . . . . . . . 10
⊢ 𝐹 = (Scalar‘𝑊) |
6 | 4, 5 | eqtr4di 2791 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 → (Scalar‘𝑤) = 𝐹) |
7 | 3, 6 | sylan9eqr 2795 |
. . . . . . . 8
⊢ ((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) → 𝑓 = 𝐹) |
8 | 7 | adantr 484 |
. . . . . . 7
⊢ (((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) ∧ 𝑘 = (Base‘𝑓)) → 𝑓 = 𝐹) |
9 | | id 22 |
. . . . . . . . 9
⊢ (𝑘 = (Base‘𝑓) → 𝑘 = (Base‘𝑓)) |
10 | 7 | fveq2d 6678 |
. . . . . . . . . 10
⊢ ((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) → (Base‘𝑓) = (Base‘𝐹)) |
11 | | isclm.k |
. . . . . . . . . 10
⊢ 𝐾 = (Base‘𝐹) |
12 | 10, 11 | eqtr4di 2791 |
. . . . . . . . 9
⊢ ((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) → (Base‘𝑓) = 𝐾) |
13 | 9, 12 | sylan9eqr 2795 |
. . . . . . . 8
⊢ (((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) ∧ 𝑘 = (Base‘𝑓)) → 𝑘 = 𝐾) |
14 | 13 | oveq2d 7186 |
. . . . . . 7
⊢ (((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) ∧ 𝑘 = (Base‘𝑓)) → (ℂfld
↾s 𝑘) =
(ℂfld ↾s 𝐾)) |
15 | 8, 14 | eqeq12d 2754 |
. . . . . 6
⊢ (((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) ∧ 𝑘 = (Base‘𝑓)) → (𝑓 = (ℂfld ↾s
𝑘) ↔ 𝐹 = (ℂfld
↾s 𝐾))) |
16 | 13 | eleq1d 2817 |
. . . . . 6
⊢ (((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) ∧ 𝑘 = (Base‘𝑓)) → (𝑘 ∈ (SubRing‘ℂfld)
↔ 𝐾 ∈
(SubRing‘ℂfld))) |
17 | 15, 16 | anbi12d 634 |
. . . . 5
⊢ (((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) ∧ 𝑘 = (Base‘𝑓)) → ((𝑓 = (ℂfld ↾s
𝑘) ∧ 𝑘 ∈
(SubRing‘ℂfld)) ↔ (𝐹 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)))) |
18 | 2, 17 | sbcied 3724 |
. . . 4
⊢ ((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) → ([(Base‘𝑓) / 𝑘](𝑓 = (ℂfld ↾s
𝑘) ∧ 𝑘 ∈
(SubRing‘ℂfld)) ↔ (𝐹 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)))) |
19 | 1, 18 | sbcied 3724 |
. . 3
⊢ (𝑤 = 𝑊 → ([(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂfld ↾s
𝑘) ∧ 𝑘 ∈
(SubRing‘ℂfld)) ↔ (𝐹 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)))) |
20 | | df-clm 23815 |
. . 3
⊢
ℂMod = {𝑤
∈ LMod ∣ [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂfld ↾s
𝑘) ∧ 𝑘 ∈
(SubRing‘ℂfld))} |
21 | 19, 20 | elrab2 3591 |
. 2
⊢ (𝑊 ∈ ℂMod ↔ (𝑊 ∈ LMod ∧ (𝐹 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)))) |
22 | | 3anass 1096 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝐹 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)) ↔ (𝑊 ∈ LMod ∧ (𝐹 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)))) |
23 | 21, 22 | bitr4i 281 |
1
⊢ (𝑊 ∈ ℂMod ↔ (𝑊 ∈ LMod ∧ 𝐹 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld))) |