This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
clmsub.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
Assertion clmsub ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ) → ( 𝐴 − 𝐵 ) = ( 𝐴 ( -g ‘ 𝐹 ) 𝐵 ) )

Proof

Step Hyp Ref Expression
1 clm0.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2 clmsub.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
3 1 2 clmsubrg ⊢ ( 𝑊 ∈ ℂMod → 𝐾 ∈ ( SubRing ‘ ℂfld ) )
4 subrgsubg ⊢ ( 𝐾 ∈ ( SubRing ‘ ℂfld ) → 𝐾 ∈ ( SubGrp ‘ ℂfld ) )
5 3 4 syl ⊢ ( 𝑊 ∈ ℂMod → 𝐾 ∈ ( SubGrp ‘ ℂfld ) )
6 cnfldsub ⊢ − = ( -g ‘ ℂfld )
7 eqid ⊢ ( ℂfld ↾s 𝐾 ) = ( ℂfld ↾s 𝐾 )
8 eqid ⊢ ( -g ‘ ( ℂfld ↾s 𝐾 ) ) = ( -g ‘ ( ℂfld ↾s 𝐾 ) )
9 6 7 8 subgsub ⊢ ( ( 𝐾 ∈ ( SubGrp ‘ ℂfld ) ∧ 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ) → ( 𝐴 − 𝐵 ) = ( 𝐴 ( -g ‘ ( ℂfld ↾s 𝐾 ) ) 𝐵 ) )
10 5 9 syl3an1 ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ) → ( 𝐴 − 𝐵 ) = ( 𝐴 ( -g ‘ ( ℂfld ↾s 𝐾 ) ) 𝐵 ) )
11 1 2 clmsca ⊢ ( 𝑊 ∈ ℂMod → 𝐹 = ( ℂfld ↾s 𝐾 ) )
12 11 fveq2d ⊢ ( 𝑊 ∈ ℂMod → ( -g ‘ 𝐹 ) = ( -g ‘ ( ℂfld ↾s 𝐾 ) ) )
13 12 3ad2ant1 ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ) → ( -g ‘ 𝐹 ) = ( -g ‘ ( ℂfld ↾s 𝐾 ) ) )
14 13 oveqd ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ) → ( 𝐴 ( -g ‘ 𝐹 ) 𝐵 ) = ( 𝐴 ( -g ‘ ( ℂfld ↾s 𝐾 ) ) 𝐵 ) )
15 10 14 eqtr4d ⊢ ( ( 𝑊 ∈ ℂMod ∧ 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ) → ( 𝐴 − 𝐵 ) = ( 𝐴 ( -g ‘ 𝐹 ) 𝐵 ) )