Theorem cphass

Description: Associative law for inner product. Equation I2 of Ponnusamy p. 363. See ipass , his5 . (Contributed by Mario Carneiro, 16-Oct-2015)

	Ref	Expression
Hypotheses	cphipcj.h	⊢ , = ( ·𝑖 ‘ 𝑊 )
	cphipcj.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
	cphass.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
	cphass.k	⊢ 𝐾 = ( Base ‘ 𝐹 )
	cphass.s	⊢ · = ( ·𝑠 ‘ 𝑊 )
Assertion	cphass	⊢ ( ( 𝑊 ∈ ℂ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		cphphl	⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ PreHil )
7		eqid	⊢ ( .r ‘ 𝐹 ) = ( .r ‘ 𝐹 )
8	3 1 2 4 5 7	ipass	⊢ ( ( 𝑊 ∈ PreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝐴 · 𝐵 ) , 𝐶 ) = ( 𝐴 ( .r ‘ 𝐹 ) ( 𝐵 , 𝐶 ) ) )
9	6 8	sylan	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝐴 · 𝐵 ) , 𝐶 ) = ( 𝐴 ( .r ‘ 𝐹 ) ( 𝐵 , 𝐶 ) ) )
10		cphclm	⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ ℂMod )
11	3	clmmul	⊢ ( 𝑊 ∈ ℂMod → · = ( .r ‘ 𝐹 ) )
12	10 11	syl	⊢ ( 𝑊 ∈ ℂPreHil → · = ( .r ‘ 𝐹 ) )
13	12	adantr	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → · = ( .r ‘ 𝐹 ) )
14	13	oveqd	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( 𝐴 · ( 𝐵 , 𝐶 ) ) = ( 𝐴 ( .r ‘ 𝐹 ) ( 𝐵 , 𝐶 ) ) )
15	9 14	eqtr4d	⊢ ( ( 𝑊 ∈ ℂPreHil ∧ ( 𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉 ) ) → ( ( 𝐴 · 𝐵 ) , 𝐶 ) = ( 𝐴 · ( 𝐵 , 𝐶 ) ) )