Metamath Proof Explorer

Theorem dipdir

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

Ref Expression
Hypotheses dipdir.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
dipdir.2 ⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
dipdir.7 ⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
Assertion dipdir ( ( 𝑈 ∈ CPreHilOLD ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝐺 𝐵 ) 𝑃 𝐶 ) = ( ( 𝐴 𝑃 𝐶 ) + ( 𝐵 𝑃 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 dipdir.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 dipdir.2 ⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
3 dipdir.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 5 eleq2d ⊢ ( 𝑈 = if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( 𝐶 ∈ 𝑋 ↔ 𝐶 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ) )
9 6 7 8 3anbi123d ⊢ ( 𝑈 = if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ↔ ( 𝐴 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ∧ 𝐵 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ∧ 𝐶 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ) ) )
10 fveq2 ⊢ ( 𝑈 = if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( +𝑣 ‘ 𝑈 ) = ( +𝑣 ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) )
11 2 10 eqtrid ⊢ ( 𝑈 = if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → 𝐺 = ( +𝑣 ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) )
12 11 oveqd ⊢ ( 𝑈 = if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( 𝐴 𝐺 𝐵 ) = ( 𝐴 ( +𝑣 ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝐵 ) )
13 12 oveq1d ⊢ ( 𝑈 = if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( ( 𝐴 𝐺 𝐵 ) 𝑃 𝐶 ) = ( ( 𝐴 ( +𝑣 ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝐵 ) 𝑃 𝐶 ) )
14 fveq2 ⊢ ( 𝑈 = if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( ·𝑖OLD ‘ 𝑈 ) = ( ·𝑖OLD ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) )
15 3 14 eqtrid ⊢ ( 𝑈 = if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → 𝑃 = ( ·𝑖OLD ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) )
16 15 oveqd ⊢ ( 𝑈 = if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( ( 𝐴 ( +𝑣 ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝐵 ) 𝑃 𝐶 ) = ( ( 𝐴 ( +𝑣 ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝐵 ) ( ·𝑖OLD ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝐶 ) )
17 13 16 eqtrd ⊢ ( 𝑈 = if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( ( 𝐴 𝐺 𝐵 ) 𝑃 𝐶 ) = ( ( 𝐴 ( +𝑣 ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝐵 ) ( ·𝑖OLD ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝐶 ) )
18 15 oveqd ⊢ ( 𝑈 = if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( 𝐴 𝑃 𝐶 ) = ( 𝐴 ( ·𝑖OLD ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝐶 ) )
19 15 oveqd ⊢ ( 𝑈 = if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( 𝐵 𝑃 𝐶 ) = ( 𝐵 ( ·𝑖OLD ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝐶 ) )
20 18 19 oveq12d ⊢ ( 𝑈 = if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( ( 𝐴 𝑃 𝐶 ) + ( 𝐵 𝑃 𝐶 ) ) = ( ( 𝐴 ( ·𝑖OLD ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝐶 ) + ( 𝐵 ( ·𝑖OLD ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝐶 ) ) )
21 17 20 eqeq12d ⊢ ( 𝑈 = if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( ( ( 𝐴 𝐺 𝐵 ) 𝑃 𝐶 ) = ( ( 𝐴 𝑃 𝐶 ) + ( 𝐵 𝑃 𝐶 ) ) ↔ ( ( 𝐴 ( +𝑣 ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝐵 ) ( ·𝑖OLD ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝐶 ) = ( ( 𝐴 ( ·𝑖OLD ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝐶 ) + ( 𝐵 ( ·𝑖OLD ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝐶 ) ) ) )
22 9 21 imbi12d ⊢ ( 𝑈 = if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) → ( ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( ( 𝐴 𝐺 𝐵 ) 𝑃 𝐶 ) = ( ( 𝐴 𝑃 𝐶 ) + ( 𝐵 𝑃 𝐶 ) ) ) ↔ ( ( 𝐴 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ∧ 𝐵 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ∧ 𝐶 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ) → ( ( 𝐴 ( +𝑣 ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝐵 ) ( ·𝑖OLD ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝐶 ) = ( ( 𝐴 ( ·𝑖OLD ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝐶 ) + ( 𝐵 ( ·𝑖OLD ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝐶 ) ) ) ) )
23 eqid ⊢ ( BaseSet ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) = ( BaseSet ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) )
24 eqid ⊢ ( +𝑣 ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) = ( +𝑣 ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) )
25 eqid ⊢ ( ·𝑠OLD ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) = ( ·𝑠OLD ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) )
26 eqid ⊢ ( ·𝑖OLD ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) = ( ·𝑖OLD ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) )
27 elimphu ⊢ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ∈ CPreHilOLD
28 23 24 25 26 27 ipdiri ⊢ ( ( 𝐴 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ∧ 𝐵 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ∧ 𝐶 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) ) → ( ( 𝐴 ( +𝑣 ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝐵 ) ( ·𝑖OLD ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝐶 ) = ( ( 𝐴 ( ·𝑖OLD ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝐶 ) + ( 𝐵 ( ·𝑖OLD ‘ if ( 𝑈 ∈ CPreHilOLD , 𝑈 , ⟨ ⟨ + , · ⟩ , abs ⟩ ) ) 𝐶 ) ) )
29 22 28 dedth ⊢ ( 𝑈 ∈ CPreHilOLD → ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( ( 𝐴 𝐺 𝐵 ) 𝑃 𝐶 ) = ( ( 𝐴 𝑃 𝐶 ) + ( 𝐵 𝑃 𝐶 ) ) ) )
30 29 imp ⊢ ( ( 𝑈 ∈ CPreHilOLD ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝐺 𝐵 ) 𝑃 𝐶 ) = ( ( 𝐴 𝑃 𝐶 ) + ( 𝐵 𝑃 𝐶 ) ) )