Proof of Theorem bj-isclm
Step | Hyp | Ref
| Expression |
1 | | eqid 2739 |
. . 3
⊢
(Scalar‘𝑊) =
(Scalar‘𝑊) |
2 | | eqid 2739 |
. . 3
⊢
(Base‘(Scalar‘𝑊)) = (Base‘(Scalar‘𝑊)) |
3 | 1, 2 | isclm 23819 |
. 2
⊢ (𝑊 ∈ ℂMod ↔ (𝑊 ∈ LMod ∧
(Scalar‘𝑊) =
(ℂfld ↾s (Base‘(Scalar‘𝑊))) ∧
(Base‘(Scalar‘𝑊)) ∈
(SubRing‘ℂfld))) |
4 | | bj-isclm.scal |
. . . . 5
⊢ (𝜑 → 𝐹 = (Scalar‘𝑊)) |
5 | 4 | eqcomd 2745 |
. . . 4
⊢ (𝜑 → (Scalar‘𝑊) = 𝐹) |
6 | | bj-isclm.base |
. . . . . . 7
⊢ (𝜑 → 𝐾 = (Base‘𝐹)) |
7 | | fveq2 6677 |
. . . . . . 7
⊢ (𝐹 = (Scalar‘𝑊) → (Base‘𝐹) =
(Base‘(Scalar‘𝑊))) |
8 | | eqtr 2759 |
. . . . . . . . 9
⊢ ((𝐾 = (Base‘𝐹) ∧ (Base‘𝐹) = (Base‘(Scalar‘𝑊))) → 𝐾 = (Base‘(Scalar‘𝑊))) |
9 | 8 | eqcomd 2745 |
. . . . . . . 8
⊢ ((𝐾 = (Base‘𝐹) ∧ (Base‘𝐹) = (Base‘(Scalar‘𝑊))) →
(Base‘(Scalar‘𝑊)) = 𝐾) |
10 | 9 | ex 416 |
. . . . . . 7
⊢ (𝐾 = (Base‘𝐹) → ((Base‘𝐹) = (Base‘(Scalar‘𝑊)) →
(Base‘(Scalar‘𝑊)) = 𝐾)) |
11 | 6, 7, 10 | syl2im 40 |
. . . . . 6
⊢ (𝜑 → (𝐹 = (Scalar‘𝑊) → (Base‘(Scalar‘𝑊)) = 𝐾)) |
12 | 4, 11 | mpd 15 |
. . . . 5
⊢ (𝜑 →
(Base‘(Scalar‘𝑊)) = 𝐾) |
13 | 12 | oveq2d 7189 |
. . . 4
⊢ (𝜑 → (ℂfld
↾s (Base‘(Scalar‘𝑊))) = (ℂfld
↾s 𝐾)) |
14 | 5, 13 | eqeq12d 2755 |
. . 3
⊢ (𝜑 → ((Scalar‘𝑊) = (ℂfld
↾s (Base‘(Scalar‘𝑊))) ↔ 𝐹 = (ℂfld
↾s 𝐾))) |
15 | 12 | eleq1d 2818 |
. . 3
⊢ (𝜑 →
((Base‘(Scalar‘𝑊)) ∈
(SubRing‘ℂfld) ↔ 𝐾 ∈
(SubRing‘ℂfld))) |
16 | 14, 15 | 3anbi23d 1440 |
. 2
⊢ (𝜑 → ((𝑊 ∈ LMod ∧ (Scalar‘𝑊) = (ℂfld
↾s (Base‘(Scalar‘𝑊))) ∧ (Base‘(Scalar‘𝑊)) ∈
(SubRing‘ℂfld)) ↔ (𝑊 ∈ LMod ∧ 𝐹 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)))) |
17 | 3, 16 | syl5bb 286 |
1
⊢ (𝜑 → (𝑊 ∈ ℂMod ↔ (𝑊 ∈ LMod ∧ 𝐹 = (ℂfld
↾s 𝐾)
∧ 𝐾 ∈
(SubRing‘ℂfld)))) |