Metamath Proof Explorer

Theorem cvsdiv

Description: Division of the scalar ring of a subcomplex vector space. (Contributed by Thierry Arnoux, 22-May-2019)

Ref Expression
Hypotheses cvsdiv.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
cvsdiv.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
Assertion cvsdiv ( ( 𝑊 ∈ ℂVec ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) ) → ( 𝐴 / 𝐵 ) = ( 𝐴 ( /r ‘ 𝐹 ) 𝐵 ) )

Proof

Step Hyp Ref Expression
1 cvsdiv.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2 cvsdiv.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
3 simpl ⊢ ( ( 𝑊 ∈ ℂVec ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) ) → 𝑊 ∈ ℂVec )
4 3 cvsclm ⊢ ( ( 𝑊 ∈ ℂVec ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) ) → 𝑊 ∈ ℂMod )
5 1 2 clmsubrg ⊢ ( 𝑊 ∈ ℂMod → 𝐾 ∈ ( SubRing ‘ ℂfld ) )
6 4 5 syl ⊢ ( ( 𝑊 ∈ ℂVec ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) ) → 𝐾 ∈ ( SubRing ‘ ℂfld ) )
7 simpr1 ⊢ ( ( 𝑊 ∈ ℂVec ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) ) → 𝐴 ∈ 𝐾 )
8 simpr2 ⊢ ( ( 𝑊 ∈ ℂVec ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) ) → 𝐵 ∈ 𝐾 )
9 simpr3 ⊢ ( ( 𝑊 ∈ ℂVec ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) ) → 𝐵 ≠ 0 )
10 eldifsn ⊢ ( 𝐵 ∈ ( 𝐾 ∖ { 0 } ) ↔ ( 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) )
11 8 9 10 sylanbrc ⊢ ( ( 𝑊 ∈ ℂVec ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) ) → 𝐵 ∈ ( 𝐾 ∖ { 0 } ) )
12 1 2 cvsunit ⊢ ( 𝑊 ∈ ℂVec → ( 𝐾 ∖ { 0 } ) = ( Unit ‘ 𝐹 ) )
13 3 12 syl ⊢ ( ( 𝑊 ∈ ℂVec ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) ) → ( 𝐾 ∖ { 0 } ) = ( Unit ‘ 𝐹 ) )
14 1 2 clmsca ⊢ ( 𝑊 ∈ ℂMod → 𝐹 = ( ℂfld ↾s 𝐾 ) )
15 4 14 syl ⊢ ( ( 𝑊 ∈ ℂVec ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) ) → 𝐹 = ( ℂfld ↾s 𝐾 ) )
16 15 fveq2d ⊢ ( ( 𝑊 ∈ ℂVec ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) ) → ( Unit ‘ 𝐹 ) = ( Unit ‘ ( ℂfld ↾s 𝐾 ) ) )
17 13 16 eqtrd ⊢ ( ( 𝑊 ∈ ℂVec ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) ) → ( 𝐾 ∖ { 0 } ) = ( Unit ‘ ( ℂfld ↾s 𝐾 ) ) )
18 11 17 eleqtrd ⊢ ( ( 𝑊 ∈ ℂVec ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) ) → 𝐵 ∈ ( Unit ‘ ( ℂfld ↾s 𝐾 ) ) )
19 eqid ⊢ ( ℂfld ↾s 𝐾 ) = ( ℂfld ↾s 𝐾 )
20 cnflddiv ⊢ / = ( /r ‘ ℂfld )
21 eqid ⊢ ( Unit ‘ ( ℂfld ↾s 𝐾 ) ) = ( Unit ‘ ( ℂfld ↾s 𝐾 ) )
22 eqid ⊢ ( /r ‘ ( ℂfld ↾s 𝐾 ) ) = ( /r ‘ ( ℂfld ↾s 𝐾 ) )
23 19 20 21 22 subrgdv ⊢ ( ( 𝐾 ∈ ( SubRing ‘ ℂfld ) ∧ 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ ( Unit ‘ ( ℂfld ↾s 𝐾 ) ) ) → ( 𝐴 / 𝐵 ) = ( 𝐴 ( /r ‘ ( ℂfld ↾s 𝐾 ) ) 𝐵 ) )
24 6 7 18 23 syl3anc ⊢ ( ( 𝑊 ∈ ℂVec ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) ) → ( 𝐴 / 𝐵 ) = ( 𝐴 ( /r ‘ ( ℂfld ↾s 𝐾 ) ) 𝐵 ) )
25 15 fveq2d ⊢ ( ( 𝑊 ∈ ℂVec ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) ) → ( /r ‘ 𝐹 ) = ( /r ‘ ( ℂfld ↾s 𝐾 ) ) )
26 25 oveqd ⊢ ( ( 𝑊 ∈ ℂVec ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) ) → ( 𝐴 ( /r ‘ 𝐹 ) 𝐵 ) = ( 𝐴 ( /r ‘ ( ℂfld ↾s 𝐾 ) ) 𝐵 ) )
27 24 26 eqtr4d ⊢ ( ( 𝑊 ∈ ℂVec ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ∧ 𝐵 ≠ 0 ) ) → ( 𝐴 / 𝐵 ) = ( 𝐴 ( /r ‘ 𝐹 ) 𝐵 ) )