Metamath Proof Explorer


Theorem clmacl

Description: Closure of ring addition for a subcomplex module. (Contributed by Mario Carneiro, 16-Oct-2015)

Ref Expression
Hypotheses clm0.f 𝐹 = ( Scalar ‘ 𝑊 )
clmsub.k 𝐾 = ( Base ‘ 𝐹 )
Assertion clmacl ( ( 𝑊 ∈ ℂMod ∧ 𝑋𝐾𝑌𝐾 ) → ( 𝑋 + 𝑌 ) ∈ 𝐾 )

Proof

Step Hyp Ref Expression
1 clm0.f 𝐹 = ( Scalar ‘ 𝑊 )
2 clmsub.k 𝐾 = ( Base ‘ 𝐹 )
3 1 2 clmsubrg ( 𝑊 ∈ ℂMod → 𝐾 ∈ ( SubRing ‘ ℂfld ) )
4 cnfldadd + = ( +g ‘ ℂfld )
5 4 subrgacl ( ( 𝐾 ∈ ( SubRing ‘ ℂfld ) ∧ 𝑋𝐾𝑌𝐾 ) → ( 𝑋 + 𝑌 ) ∈ 𝐾 )
6 3 5 syl3an1 ( ( 𝑊 ∈ ℂMod ∧ 𝑋𝐾𝑌𝐾 ) → ( 𝑋 + 𝑌 ) ∈ 𝐾 )