Metamath Proof Explorer

Theorem dipass

Description: Associative law for inner product. Equation I2 of Ponnusamy p. 363. (Contributed by NM, 25-Aug-2007) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 ipass.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 ipass.4 ⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
3 ipass.7 ⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
4 fveq2 ⊢ ( 𝑈 = if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( BaseSet ‘ 𝑈 ) = ( BaseSet ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) )
5 1 4 eqtrid ⊢ ( 𝑈 = if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → 𝑋 = ( BaseSet ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) )
6 5 eleq2d ⊢ ( 𝑈 = if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( 𝐵 ∈ 𝑋 ↔ 𝐵 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ) )
7 5 eleq2d ⊢ ( 𝑈 = if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( 𝐶 ∈ 𝑋 ↔ 𝐶 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ) )
8 6 7 3anbi23d ⊢ ( 𝑈 = if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ↔ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ∧ 𝐶 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ) ) )
9 fveq2 ⊢ ( 𝑈 = if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( ·𝑠OLD ‘ 𝑈 ) = ( ·𝑠OLD ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) )
10 2 9 eqtrid ⊢ ( 𝑈 = if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → 𝑆 = ( ·𝑠OLD ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) )
11 10 oveqd ⊢ ( 𝑈 = if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( 𝐴 𝑆 𝐵 ) = ( 𝐴 ( ·𝑠OLD ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝐵 ) )
12 11 oveq1d ⊢ ( 𝑈 = if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( ( 𝐴 𝑆 𝐵 ) 𝑃 𝐶 ) = ( ( 𝐴 ( ·𝑠OLD ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝐵 ) 𝑃 𝐶 ) )
13 fveq2 ⊢ ( 𝑈 = if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( ·𝑖OLD ‘ 𝑈 ) = ( ·𝑖OLD ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) )
14 3 13 eqtrid ⊢ ( 𝑈 = if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → 𝑃 = ( ·𝑖OLD ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) )
15 14 oveqd ⊢ ( 𝑈 = if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( ( 𝐴 ( ·𝑠OLD ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝐵 ) 𝑃 𝐶 ) = ( ( 𝐴 ( ·𝑠OLD ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝐵 ) ( ·𝑖OLD ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝐶 ) )
16 12 15 eqtrd ⊢ ( 𝑈 = if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( ( 𝐴 𝑆 𝐵 ) 𝑃 𝐶 ) = ( ( 𝐴 ( ·𝑠OLD ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝐵 ) ( ·𝑖OLD ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝐶 ) )
17 14 oveqd ⊢ ( 𝑈 = if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( 𝐵 𝑃 𝐶 ) = ( 𝐵 ( ·𝑖OLD ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝐶 ) )
18 17 oveq2d ⊢ ( 𝑈 = if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( 𝐴 · ( 𝐵 𝑃 𝐶 ) ) = ( 𝐴 · ( 𝐵 ( ·𝑖OLD ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝐶 ) ) )
19 16 18 eqeq12d ⊢ ( 𝑈 = if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( ( ( 𝐴 𝑆 𝐵 ) 𝑃 𝐶 ) = ( 𝐴 · ( 𝐵 𝑃 𝐶 ) ) ↔ ( ( 𝐴 ( ·𝑠OLD ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝐵 ) ( ·𝑖OLD ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝐶 ) = ( 𝐴 · ( 𝐵 ( ·𝑖OLD ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝐶 ) ) ) )
20 8 19 imbi12d ⊢ ( 𝑈 = if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( ( 𝐴 𝑆 𝐵 ) 𝑃 𝐶 ) = ( 𝐴 · ( 𝐵 𝑃 𝐶 ) ) ) ↔ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ∧ 𝐶 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ) → ( ( 𝐴 ( ·𝑠OLD ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝐵 ) ( ·𝑖OLD ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝐶 ) = ( 𝐴 · ( 𝐵 ( ·𝑖OLD ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝐶 ) ) ) ) )
21 eqid ⊢ ( BaseSet ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) = ( BaseSet ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) )
22 eqid ⊢ ( +𝑣 ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) = ( +𝑣 ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) )
23 eqid ⊢ ( ·𝑠OLD ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) = ( ·𝑠OLD ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) )
24 eqid ⊢ ( ·𝑖OLD ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) = ( ·𝑖OLD ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) )
25 elimphu ⊢ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ∈ CPreHilOLD
26 21 22 23 24 25 ipassi ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ∧ 𝐶 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ) → ( ( 𝐴 ( ·𝑠OLD ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝐵 ) ( ·𝑖OLD ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝐶 ) = ( 𝐴 · ( 𝐵 ( ·𝑖OLD ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝐶 ) ) )
27 20 26 dedth ⊢ ( 𝑈 ∈ CPreHilOLD → ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( ( 𝐴 𝑆 𝐵 ) 𝑃 𝐶 ) = ( 𝐴 · ( 𝐵 𝑃 𝐶 ) ) ) )
28 27 imp ⊢ ( ( 𝑈 ∈ CPreHilOLD ∧ ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝑆 𝐵 ) 𝑃 𝐶 ) = ( 𝐴 · ( 𝐵 𝑃 𝐶 ) ) )