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 ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
isclm.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
Assertion isclm ( 𝑊 ∈ ℂMod ↔ ( 𝑊 ∈ LMod ∧ 𝐹 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) )

Proof

Step Hyp Ref Expression
1 isclm.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2 isclm.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
3 fvexd ⊢ ( 𝑤 = 𝑊 → ( Scalar ‘ 𝑤 ) ∈ V )
4 fvexd ⊢ ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) → ( Base ‘ 𝑓 ) ∈ V )
5 id ⊢ ( 𝑓 = ( Scalar ‘ 𝑤 ) → 𝑓 = ( Scalar ‘ 𝑤 ) )
6 fveq2 ⊢ ( 𝑤 = 𝑊 → ( Scalar ‘ 𝑤 ) = ( Scalar ‘ 𝑊 ) )
7 6 1 eqtr4di ⊢ ( 𝑤 = 𝑊 → ( Scalar ‘ 𝑤 ) = 𝐹 )
8 5 7 sylan9eqr ⊢ ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) → 𝑓 = 𝐹 )
9 8 adantr ⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) ∧ 𝑘 = ( Base ‘ 𝑓 ) ) → 𝑓 = 𝐹 )
10 id ⊢ ( 𝑘 = ( Base ‘ 𝑓 ) → 𝑘 = ( Base ‘ 𝑓 ) )
11 8 fveq2d ⊢ ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) → ( Base ‘ 𝑓 ) = ( Base ‘ 𝐹 ) )
12 11 2 eqtr4di ⊢ ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) → ( Base ‘ 𝑓 ) = 𝐾 )
13 10 12 sylan9eqr ⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) ∧ 𝑘 = ( Base ‘ 𝑓 ) ) → 𝑘 = 𝐾 )
14 13 oveq2d ⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) ∧ 𝑘 = ( Base ‘ 𝑓 ) ) → ( ℂfld ↾s 𝑘 ) = ( ℂfld ↾s 𝐾 ) )
15 9 14 eqeq12d ⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) ∧ 𝑘 = ( Base ‘ 𝑓 ) ) → ( 𝑓 = ( ℂfld ↾s 𝑘 ) ↔ 𝐹 = ( ℂfld ↾s 𝐾 ) ) )
16 13 eleq1d ⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) ∧ 𝑘 = ( Base ‘ 𝑓 ) ) → ( 𝑘 ∈ ( SubRing ‘ ℂfld ) ↔ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) )
17 15 16 anbi12d ⊢ ( ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) ∧ 𝑘 = ( Base ‘ 𝑓 ) ) → ( ( 𝑓 = ( ℂfld ↾s 𝑘 ) ∧ 𝑘 ∈ ( SubRing ‘ ℂfld ) ) ↔ ( 𝐹 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ) )
18 4 17 sbcied ⊢ ( ( 𝑤 = 𝑊 ∧ 𝑓 = ( Scalar ‘ 𝑤 ) ) → ( [ ( Base ‘ 𝑓 ) / 𝑘 ] ( 𝑓 = ( ℂfld ↾s 𝑘 ) ∧ 𝑘 ∈ ( SubRing ‘ ℂfld ) ) ↔ ( 𝐹 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ) )
19 3 18 sbcied ⊢ ( 𝑤 = 𝑊 → ( [ ( Scalar ‘ 𝑤 ) / 𝑓 ] [ ( Base ‘ 𝑓 ) / 𝑘 ] ( 𝑓 = ( ℂfld ↾s 𝑘 ) ∧ 𝑘 ∈ ( SubRing ‘ ℂfld ) ) ↔ ( 𝐹 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ) )
20 df-clm ⊢ ℂMod = { 𝑤 ∈ LMod ∣ [ ( Scalar ‘ 𝑤 ) / 𝑓 ] [ ( Base ‘ 𝑓 ) / 𝑘 ] ( 𝑓 = ( ℂfld ↾s 𝑘 ) ∧ 𝑘 ∈ ( SubRing ‘ ℂfld ) ) }
21 19 20 elrab2 ⊢ ( 𝑊 ∈ ℂMod ↔ ( 𝑊 ∈ LMod ∧ ( 𝐹 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ) )
22 3anass ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐹 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ↔ ( 𝑊 ∈ LMod ∧ ( 𝐹 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) ) )
23 21 22 bitr4i ⊢ ( 𝑊 ∈ ℂMod ↔ ( 𝑊 ∈ LMod ∧ 𝐹 = ( ℂfld ↾s 𝐾 ) ∧ 𝐾 ∈ ( SubRing ‘ ℂfld ) ) )