Theorem cphassir

Description: "Associative" law for the second argument of an inner product with scalar _ i . (Contributed by AV, 17-Oct-2021)

	Ref	Expression
Hypotheses	cphassi.x	⊢ 𝑋 = ( Base ‘ 𝑊 )
	cphassi.s	⊢ · = ( ·𝑠 ‘ 𝑊 )
	cphassi.i	⊢ , = ( ·𝑖 ‘ 𝑊 )
	cphassi.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	cphassi.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
Assertion	cphassir	⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 , ( i · 𝐵 ) ) = ( - i · ( 𝐴 , 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		cphassi.x	⊢ 𝑋 = ( Base ‘ 𝑊 )
2		cphassi.s	⊢ · = ( ·𝑠 ‘ 𝑊 )
3		cphassi.i	⊢ , = ( ·𝑖 ‘ 𝑊 )
4		cphassi.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
5		cphassi.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
6		simp1l	⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝑊 ∈ ℂPreHil )
7		simp1r	⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → i ∈ 𝐾 )
8		simp2	⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐴 ∈ 𝑋 )
9		simp3	⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → 𝐵 ∈ 𝑋 )
10	3 1 4 5 2	cphassr	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( i ∈ 𝐾 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 , ( i · 𝐵 ) ) = ( ( ∗ ‘ i ) · ( 𝐴 , 𝐵 ) ) )
11	6 7 8 9 10	syl13anc	⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 , ( i · 𝐵 ) ) = ( ( ∗ ‘ i ) · ( 𝐴 , 𝐵 ) ) )
12		cji	⊢ ( ∗ ‘ i ) = - i
13	12	oveq1i	⊢ ( ( ∗ ‘ i ) · ( 𝐴 , 𝐵 ) ) = ( - i · ( 𝐴 , 𝐵 ) )
14	11 13	eqtrdi	⊢ ( ( ( 𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 , ( i · 𝐵 ) ) = ( - i · ( 𝐴 , 𝐵 ) ) )