Metamath Proof Explorer

Theorem clmsub

Description: Subtraction in the scalar ring of a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015)

Ref Expression
Hypotheses clm0.f ⊢ F = Scalar ⁡ W
clmsub.k ⊢ K = Base F
Assertion clmsub ⊢ W ∈ CMod ∧ A ∈ K ∧ B ∈ K → A − B = A - F B

Proof

Step Hyp Ref Expression
1 clm0.f ⊢ F = Scalar ⁡ W
2 clmsub.k ⊢ K = Base F
3 1 2 clmsubrg ⊢ W ∈ CMod → K ∈ SubRing ⁡ ℂ fld
4 subrgsubg ⊢ K ∈ SubRing ⁡ ℂ fld → K ∈ SubGrp ⁡ ℂ fld
5 3 4 syl ⊢ W ∈ CMod → K ∈ SubGrp ⁡ ℂ fld
6 cnfldsub ⊢ − = - ℂ fld
7 eqid ⊢ ℂ fld ↾ 𝑠 K = ℂ fld ↾ 𝑠 K
8 eqid ⊢ - ℂ fld ↾ 𝑠 K = - ℂ fld ↾ 𝑠 K
9 6 7 8 subgsub ⊢ K ∈ SubGrp ⁡ ℂ fld ∧ A ∈ K ∧ B ∈ K → A − B = A - ℂ fld ↾ 𝑠 K B
10 5 9 syl3an1 ⊢ W ∈ CMod ∧ A ∈ K ∧ B ∈ K → A − B = A - ℂ fld ↾ 𝑠 K B
11 1 2 clmsca ⊢ W ∈ CMod → F = ℂ fld ↾ 𝑠 K
12 11 fveq2d ⊢ W ∈ CMod → - F = - ℂ fld ↾ 𝑠 K
13 12 3ad2ant1 ⊢ W ∈ CMod ∧ A ∈ K ∧ B ∈ K → - F = - ℂ fld ↾ 𝑠 K
14 13 oveqd ⊢ W ∈ CMod ∧ A ∈ K ∧ B ∈ K → A - F B = A - ℂ fld ↾ 𝑠 K B
15 10 14 eqtr4d ⊢ W ∈ CMod ∧ A ∈ K ∧ B ∈ K → A − B = A - F B