Step | Hyp | Ref
| Expression |
1 | | fvex 6113 |
. . . . 5
⊢
(Scalar‘𝑤)
∈ V |
2 | 1 | a1i 11 |
. . . 4
⊢ (𝑤 = 𝑊 → (Scalar‘𝑤) ∈ V) |
3 | | fvex 6113 |
. . . . . 6
⊢
(Base‘𝑓)
∈ V |
4 | 3 | a1i 11 |
. . . . 5
⊢ ((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) → (Base‘𝑓) ∈ V) |
5 | | id 22 |
. . . . . . . . 9
⊢ (𝑓 = (Scalar‘𝑤) → 𝑓 = (Scalar‘𝑤)) |
6 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑊 → (Scalar‘𝑤) = (Scalar‘𝑊)) |
7 | | isclm.f |
. . . . . . . . . 10
⊢ 𝐹 = (Scalar‘𝑊) |
8 | 6, 7 | syl6eqr 2662 |
. . . . . . . . 9
⊢ (𝑤 = 𝑊 → (Scalar‘𝑤) = 𝐹) |
9 | 5, 8 | sylan9eqr 2666 |
. . . . . . . 8
⊢ ((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) → 𝑓 = 𝐹) |
10 | 9 | adantr 480 |
. . . . . . 7
⊢ (((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) ∧ 𝑘 = (Base‘𝑓)) → 𝑓 = 𝐹) |
11 | | id 22 |
. . . . . . . . 9
⊢ (𝑘 = (Base‘𝑓) → 𝑘 = (Base‘𝑓)) |
12 | 9 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) → (Base‘𝑓) = (Base‘𝐹)) |
13 | | isclm.k |
. . . . . . . . . 10
⊢ 𝐾 = (Base‘𝐹) |
14 | 12, 13 | syl6eqr 2662 |
. . . . . . . . 9
⊢ ((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) → (Base‘𝑓) = 𝐾) |
15 | 11, 14 | sylan9eqr 2666 |
. . . . . . . 8
⊢ (((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) ∧ 𝑘 = (Base‘𝑓)) → 𝑘 = 𝐾) |
16 | 15 | oveq2d 6565 |
. . . . . . 7
⊢ (((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) ∧ 𝑘 = (Base‘𝑓)) → (ℂfld
↾s 𝑘) =
(ℂfld ↾s 𝐾)) |
17 | 10, 16 | eqeq12d 2625 |
. . . . . 6
⊢ (((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) ∧ 𝑘 = (Base‘𝑓)) → (𝑓 = (ℂfld ↾s
𝑘) ↔ 𝐹 = (ℂfld
↾s 𝐾))) |
18 | 15 | eleq1d 2672 |
. . . . . 6
⊢ (((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) ∧ 𝑘 = (Base‘𝑓)) → (𝑘 ∈ (SubRing‘ℂfld)
↔ 𝐾 ∈
(SubRing‘ℂfld))) |
19 | 17, 18 | anbi12d 743 |
. . . . 5
⊢ (((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) ∧ 𝑘 = (Base‘𝑓)) → ((𝑓 = (ℂfld ↾s
𝑘) ∧ 𝑘 ∈
(SubRing‘ℂfld)) ↔ (𝐹 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)))) |
20 | 4, 19 | sbcied 3439 |
. . . 4
⊢ ((𝑤 = 𝑊 ∧ 𝑓 = (Scalar‘𝑤)) → ([(Base‘𝑓) / 𝑘](𝑓 = (ℂfld ↾s
𝑘) ∧ 𝑘 ∈
(SubRing‘ℂfld)) ↔ (𝐹 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)))) |
21 | 2, 20 | sbcied 3439 |
. . 3
⊢ (𝑤 = 𝑊 → ([(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂfld ↾s
𝑘) ∧ 𝑘 ∈
(SubRing‘ℂfld)) ↔ (𝐹 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)))) |
22 | | df-clm 22671 |
. . 3
⊢
ℂMod = {𝑤
∈ LMod ∣ [(Scalar‘𝑤) / 𝑓][(Base‘𝑓) / 𝑘](𝑓 = (ℂfld ↾s
𝑘) ∧ 𝑘 ∈
(SubRing‘ℂfld))} |
23 | 21, 22 | elrab2 3333 |
. 2
⊢ (𝑊 ∈ ℂMod ↔ (𝑊 ∈ LMod ∧ (𝐹 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)))) |
24 | | 3anass 1035 |
. 2
⊢ ((𝑊 ∈ LMod ∧ 𝐹 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)) ↔ (𝑊 ∈ LMod ∧ (𝐹 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)))) |
25 | 23, 24 | bitr4i 266 |
1
⊢ (𝑊 ∈ ℂMod ↔ (𝑊 ∈ LMod ∧ 𝐹 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld))) |