Theorem dipassr2

Description: "Associative" law for inner product. Conjugate version of dipassr . (Contributed by NM, 23-Nov-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ipass.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
	ipass.4	⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
	ipass.7	⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
Assertion	dipassr2	⊢ ( ( 𝑈 ∈ CPreHilOLD ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝑃 ( ( ∗ ‘ 𝐵 ) 𝑆 𝐶 ) ) = ( 𝐵 · ( 𝐴 𝑃 𝐶 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ipass.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		ipass.4	⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
3		ipass.7	⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
4		cjcl	⊢ ( 𝐵 ∈ ℂ → ( ∗ ‘ 𝐵 ) ∈ ℂ )
5	1 2 3	dipassr	⊢ ( ( 𝑈 ∈ CPreHilOLD ∧ ( 𝐴 ∈ 𝑋 ∧ ( ∗ ‘ 𝐵 ) ∈ ℂ ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝑃 ( ( ∗ ‘ 𝐵 ) 𝑆 𝐶 ) ) = ( ( ∗ ‘ ( ∗ ‘ 𝐵 ) ) · ( 𝐴 𝑃 𝐶 ) ) )
6	4 5	syl3anr2	⊢ ( ( 𝑈 ∈ CPreHilOLD ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝑃 ( ( ∗ ‘ 𝐵 ) 𝑆 𝐶 ) ) = ( ( ∗ ‘ ( ∗ ‘ 𝐵 ) ) · ( 𝐴 𝑃 𝐶 ) ) )
7		cjcj	⊢ ( 𝐵 ∈ ℂ → ( ∗ ‘ ( ∗ ‘ 𝐵 ) ) = 𝐵 )
8	7	3ad2ant2	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋 ) → ( ∗ ‘ ( ∗ ‘ 𝐵 ) ) = 𝐵 )
9	8	adantl	⊢ ( ( 𝑈 ∈ CPreHilOLD ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋 ) ) → ( ∗ ‘ ( ∗ ‘ 𝐵 ) ) = 𝐵 )
10	9	oveq1d	⊢ ( ( 𝑈 ∈ CPreHilOLD ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋 ) ) → ( ( ∗ ‘ ( ∗ ‘ 𝐵 ) ) · ( 𝐴 𝑃 𝐶 ) ) = ( 𝐵 · ( 𝐴 𝑃 𝐶 ) ) )
11	6 10	eqtrd	⊢ ( ( 𝑈 ∈ CPreHilOLD ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝑃 ( ( ∗ ‘ 𝐵 ) 𝑆 𝐶 ) ) = ( 𝐵 · ( 𝐴 𝑃 𝐶 ) ) )