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

Metamath Proof Explorer

Theorem cphassr

Description: "Associative" law for second argument of inner product (compare cphass ). See ipassr , his52 . (Contributed by Mario Carneiro, 16-Oct-2015)

Ref Expression
Hypotheses cphipcj.h ⊢ , = ( ·𝑖 ‘ 𝑊 )
cphipcj.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
cphass.f ⊢ 𝐹 = ( Scalar ‘ 𝑊 )
cphass.k ⊢ 𝐾 = ( Base ‘ 𝐹 )
cphass.s ⊢ · = ( ·𝑠 ‘ 𝑊 )
Assertion cphassr ( ( 𝑊 ∈ ℂ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 cphclm ⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ ℂMod )
7 6 adantr ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝑊 ∈ ℂMod )
8 3 clmmul ⊢ ( 𝑊 ∈ ℂMod → · = ( .r ‘ 𝐹 ) )
9 7 8 syl ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → · = ( .r ‘ 𝐹 ) )
10 eqidd ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝐵 , 𝐶 ) = ( 𝐵 , 𝐶 ) )
11 3 clmcj ⊢ ( 𝑊 ∈ ℂMod → ∗ = ( *𝑟 ‘ 𝐹 ) )
12 7 11 syl ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ∗ = ( *𝑟 ‘ 𝐹 ) )
13 12 fveq1d ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ∗ ‘ 𝐴 ) = ( ( *𝑟 ‘ 𝐹 ) ‘ 𝐴 ) )
14 9 10 13 oveq123d ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝐵 , 𝐶 ) · ( ∗ ‘ 𝐴 ) ) = ( ( 𝐵 , 𝐶 ) ( .r ‘ 𝐹 ) ( ( *𝑟 ‘ 𝐹 ) ‘ 𝐴 ) ) )
15 3 4 clmsscn ⊢ ( 𝑊 ∈ ℂMod → 𝐾 ⊆ ℂ )
16 7 15 syl ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐾 ⊆ ℂ )
17 simpr1 ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐴 ∈ 𝐾 )
18 16 17 sseldd ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → 𝐴 ∈ ℂ )
19 18 cjcld ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ∗ ‘ 𝐴 ) ∈ ℂ )
20 2 1 cphipcl ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 𝐵 , 𝐶 ) ∈ ℂ )
21 20 3adant3r1 ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝐵 , 𝐶 ) ∈ ℂ )
22 19 21 mulcomd ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( ∗ ‘ 𝐴 ) · ( 𝐵 , 𝐶 ) ) = ( ( 𝐵 , 𝐶 ) · ( ∗ ‘ 𝐴 ) ) )
23 cphphl ⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ PreHil )
24 3anrot ⊢ ( ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ↔ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝐾 ) )
25 24 biimpi ⊢ ( ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) → ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝐾 ) )
26 eqid ⊢ ( .r ‘ 𝐹 ) = ( .r ‘ 𝐹 )
27 eqid ⊢ ( *𝑟 ‘ 𝐹 ) = ( *𝑟 ‘ 𝐹 )
28 3 1 2 4 5 26 27 ipassr ⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ∧ 𝐴 ∈ 𝐾 ) ) → ( 𝐵 , ( 𝐴 · 𝐶 ) ) = ( ( 𝐵 , 𝐶 ) ( .r ‘ 𝐹 ) ( ( *𝑟 ‘ 𝐹 ) ‘ 𝐴 ) ) )
29 23 25 28 syl2an ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝐵 , ( 𝐴 · 𝐶 ) ) = ( ( 𝐵 , 𝐶 ) ( .r ‘ 𝐹 ) ( ( *𝑟 ‘ 𝐹 ) ‘ 𝐴 ) ) )
30 14 22 29 3eqtr4rd ⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝐵 , ( 𝐴 · 𝐶 ) ) = ( ( ∗ ‘ 𝐴 ) · ( 𝐵 , 𝐶 ) ) )