Metamath Proof Explorer

Theorem bj-isclm

Description: The predicate "is a subcomplex module". (Contributed by BJ, 6-Jan-2024)

Ref Expression
Hypotheses bj-isclm.scal ⊢ φ → F = Scalar ⁡ W
bj-isclm.base ⊢ φ → K = Base F
Assertion bj-isclm ⊢ φ → W ∈ CMod ↔ W ∈ LMod ∧ F = ℂ fld ↾ 𝑠 K ∧ K ∈ SubRing ⁡ ℂ fld

Proof

Step Hyp Ref Expression
1 bj-isclm.scal ⊢ φ → F = Scalar ⁡ W
2 bj-isclm.base ⊢ φ → K = Base F
3 eqid ⊢ Scalar ⁡ W = Scalar ⁡ W
4 eqid ⊢ Base Scalar ⁡ W = Base Scalar ⁡ W
5 3 4 isclm ⊢ W ∈ CMod ↔ W ∈ LMod ∧ Scalar ⁡ W = ℂ fld ↾ 𝑠 Base Scalar ⁡ W ∧ Base Scalar ⁡ W ∈ SubRing ⁡ ℂ fld
6 1 eqcomd ⊢ φ → Scalar ⁡ W = F
7 fveq2 ⊢ F = Scalar ⁡ W → Base F = Base Scalar ⁡ W
8 eqtr ⊢ K = Base F ∧ Base F = Base Scalar ⁡ W → K = Base Scalar ⁡ W
9 8 eqcomd ⊢ K = Base F ∧ Base F = Base Scalar ⁡ W → Base Scalar ⁡ W = K
10 9 ex ⊢ K = Base F → Base F = Base Scalar ⁡ W → Base Scalar ⁡ W = K
11 2 7 10 syl2im ⊢ φ → F = Scalar ⁡ W → Base Scalar ⁡ W = K
12 1 11 mpd ⊢ φ → Base Scalar ⁡ W = K
13 12 oveq2d ⊢ φ → ℂ fld ↾ 𝑠 Base Scalar ⁡ W = ℂ fld ↾ 𝑠 K
14 6 13 eqeq12d ⊢ φ → Scalar ⁡ W = ℂ fld ↾ 𝑠 Base Scalar ⁡ W ↔ F = ℂ fld ↾ 𝑠 K
15 12 eleq1d ⊢ φ → Base Scalar ⁡ W ∈ SubRing ⁡ ℂ fld ↔ K ∈ SubRing ⁡ ℂ fld
16 14 15 3anbi23d ⊢ φ → W ∈ LMod ∧ Scalar ⁡ W = ℂ fld ↾ 𝑠 Base Scalar ⁡ W ∧ Base Scalar ⁡ W ∈ SubRing ⁡ ℂ fld ↔ W ∈ LMod ∧ F = ℂ fld ↾ 𝑠 K ∧ K ∈ SubRing ⁡ ℂ fld
17 5 16 bitrid ⊢ φ → W ∈ CMod ↔ W ∈ LMod ∧ F = ℂ fld ↾ 𝑠 K ∧ K ∈ SubRing ⁡ ℂ fld