Metamath Proof Explorer

Theorem isclm

Description: A subcomplex module is a left module over a subring of the field of complex numbers. (Contributed by Mario Carneiro, 16-Oct-2015)

Ref Expression
Hypotheses isclm.f ⊢ F = Scalar ⁡ W
isclm.k ⊢ K = Base F
Assertion isclm ⊢ W ∈ CMod ↔ W ∈ LMod ∧ F = ℂ fld ↾ 𝑠 K ∧ K ∈ SubRing ⁡ ℂ fld

Proof

Step Hyp Ref Expression
1 isclm.f ⊢ F = Scalar ⁡ W
2 isclm.k ⊢ K = Base F
3 fvexd ⊢ w = W → Scalar ⁡ w ∈ V
4 fvexd ⊢ w = W ∧ f = Scalar ⁡ w → Base f ∈ V
5 id ⊢ f = Scalar ⁡ w → f = Scalar ⁡ w
6 fveq2 ⊢ w = W → Scalar ⁡ w = Scalar ⁡ W
7 6 1 eqtr4di ⊢ w = W → Scalar ⁡ w = F
8 5 7 sylan9eqr ⊢ w = W ∧ f = Scalar ⁡ w → f = F
9 8 adantr ⊢ w = W ∧ f = Scalar ⁡ w ∧ k = Base f → f = F
10 id ⊢ k = Base f → k = Base f
11 8 fveq2d ⊢ w = W ∧ f = Scalar ⁡ w → Base f = Base F
12 11 2 eqtr4di ⊢ w = W ∧ f = Scalar ⁡ w → Base f = K
13 10 12 sylan9eqr ⊢ w = W ∧ f = Scalar ⁡ w ∧ k = Base f → k = K
14 13 oveq2d ⊢ w = W ∧ f = Scalar ⁡ w ∧ k = Base f → ℂ fld ↾ 𝑠 k = ℂ fld ↾ 𝑠 K
15 9 14 eqeq12d ⊢ w = W ∧ f = Scalar ⁡ w ∧ k = Base f → f = ℂ fld ↾ 𝑠 k ↔ F = ℂ fld ↾ 𝑠 K
16 13 eleq1d ⊢ w = W ∧ f = Scalar ⁡ w ∧ k = Base f → k ∈ SubRing ⁡ ℂ fld ↔ K ∈ SubRing ⁡ ℂ fld
17 15 16 anbi12d ⊢ w = W ∧ f = Scalar ⁡ w ∧ k = Base f → f = ℂ fld ↾ 𝑠 k ∧ k ∈ SubRing ⁡ ℂ fld ↔ F = ℂ fld ↾ 𝑠 K ∧ K ∈ SubRing ⁡ ℂ fld
18 4 17 sbcied ⊢ w = W ∧ f = Scalar ⁡ w → [˙Base f / k]˙ f = ℂ fld ↾ 𝑠 k ∧ k ∈ SubRing ⁡ ℂ fld ↔ F = ℂ fld ↾ 𝑠 K ∧ K ∈ SubRing ⁡ ℂ fld
19 3 18 sbcied ⊢ w = W → [˙ Scalar ⁡ w / f]˙ [˙Base f / k]˙ f = ℂ fld ↾ 𝑠 k ∧ k ∈ SubRing ⁡ ℂ fld ↔ F = ℂ fld ↾ 𝑠 K ∧ K ∈ SubRing ⁡ ℂ fld
20 df-clm ⊢ CMod = w ∈ LMod | [˙ Scalar ⁡ w / f]˙ [˙Base f / k]˙ f = ℂ fld ↾ 𝑠 k ∧ k ∈ SubRing ⁡ ℂ fld
21 19 20 elrab2 ⊢ W ∈ CMod ↔ W ∈ LMod ∧ F = ℂ fld ↾ 𝑠 K ∧ K ∈ SubRing ⁡ ℂ fld
22 3anass ⊢ W ∈ LMod ∧ F = ℂ fld ↾ 𝑠 K ∧ K ∈ SubRing ⁡ ℂ fld ↔ W ∈ LMod ∧ F = ℂ fld ↾ 𝑠 K ∧ K ∈ SubRing ⁡ ℂ fld
23 21 22 bitr4i ⊢ W ∈ CMod ↔ W ∈ LMod ∧ F = ℂ fld ↾ 𝑠 K ∧ K ∈ SubRing ⁡ ℂ fld