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

Metamath Proof Explorer

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 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋 ) ) → ( 𝐴 𝑃 ( ( ∗ ‘ 𝐵 ) 𝑆 𝐶 ) ) = ( 𝐵 · ( 𝐴 𝑃 𝐶 ) ) )