Metamath Proof Explorer

Theorem cph2ass

Description: Move scalar multiplication to outside of inner product. See his35 . (Contributed by Mario Carneiro, 17-Oct-2015)

Ref Expression
Hypotheses cphipcj.h ⊢ , = ( ·𝑖 ‘ 𝑊 )
cphipcj.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
cphass.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
cphass.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
cphass.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
Assertion cph2ass ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( ( 𝐴 · 𝐶 ) , ( 𝐵 · 𝐷 ) ) = ( ( 𝐴 · ( ∗ ‘ 𝐵 ) ) · ( 𝐶 , 𝐷 ) ) )

Proof

Step Hyp Ref Expression
1 cphipcj.h ⊢ , = ( ·𝑖 ‘ 𝑊 )
2 cphipcj.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
3 cphass.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
4 cphass.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
5 cphass.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
6 simp1 ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → 𝑊 ∈ ℂPreHil )
7 simp2r ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → 𝐵 ∈ 𝐾 )
8 simp3l ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → 𝐶 ∈ 𝑉 )
9 simp3r ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → 𝐷 ∈ 𝑉 )
10 1 2 3 4 5 cphassr ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐵 ∈ 𝐾 ∧ 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( 𝐶 , ( 𝐵 · 𝐷 ) ) = ( ( ∗ ‘ 𝐵 ) · ( 𝐶 , 𝐷 ) ) )
11 6 7 8 9 10 syl13anc ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( 𝐶 , ( 𝐵 · 𝐷 ) ) = ( ( ∗ ‘ 𝐵 ) · ( 𝐶 , 𝐷 ) ) )
12 11 oveq2d ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( 𝐴 · ( 𝐶 , ( 𝐵 · 𝐷 ) ) ) = ( 𝐴 · ( ( ∗ ‘ 𝐵 ) · ( 𝐶 , 𝐷 ) ) ) )
13 simp2l ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → 𝐴 ∈ 𝐾 )
14 cphlmod ⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ LMod )
15 14 3ad2ant1 ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → 𝑊 ∈ LMod )
16 2 3 5 4 lmodvscl ⊢ ( ( 𝑊 ∈ LMod ∧ 𝐵 ∈ 𝐾 ∧ 𝐷 ∈ 𝑉 ) → ( 𝐵 · 𝐷 ) ∈ 𝑉 )
17 15 7 9 16 syl3anc ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( 𝐵 · 𝐷 ) ∈ 𝑉 )
18 1 2 3 4 5 cphass ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐶 ∈ 𝑉 ∧ ( 𝐵 · 𝐷 ) ∈ 𝑉 ) ) → ( ( 𝐴 · 𝐶 ) , ( 𝐵 · 𝐷 ) ) = ( 𝐴 · ( 𝐶 , ( 𝐵 · 𝐷 ) ) ) )
19 6 13 8 17 18 syl13anc ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( ( 𝐴 · 𝐶 ) , ( 𝐵 · 𝐷 ) ) = ( 𝐴 · ( 𝐶 , ( 𝐵 · 𝐷 ) ) ) )
20 cphclm ⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ ℂMod )
21 20 3ad2ant1 ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → 𝑊 ∈ ℂMod )
22 3 4 clmsscn ⊢ ( 𝑊 ∈ ℂMod → 𝐾 ⊆ ℂ )
23 21 22 syl ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → 𝐾 ⊆ ℂ )
24 23 13 sseldd ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → 𝐴 ∈ ℂ )
25 23 7 sseldd ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → 𝐵 ∈ ℂ )
26 25 cjcld ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( ∗ ‘ 𝐵 ) ∈ ℂ )
27 2 1 cphipcl ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) → ( 𝐶 , 𝐷 ) ∈ ℂ )
28 27 3expb ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( 𝐶 , 𝐷 ) ∈ ℂ )
29 28 3adant2 ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( 𝐶 , 𝐷 ) ∈ ℂ )
30 24 26 29 mulassd ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( ( 𝐴 · ( ∗ ‘ 𝐵 ) ) · ( 𝐶 , 𝐷 ) ) = ( 𝐴 · ( ( ∗ ‘ 𝐵 ) · ( 𝐶 , 𝐷 ) ) ) )
31 12 19 30 3eqtr4d ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( ( 𝐴 · 𝐶 ) , ( 𝐵 · 𝐷 ) ) = ( ( 𝐴 · ( ∗ ‘ 𝐵 ) ) · ( 𝐶 , 𝐷 ) ) )