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 ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) ) → ( ( 𝐴 𝐺 𝐵 ) 𝑃 𝐶 ) = ( ( 𝐴 𝑃 𝐶 ) + ( 𝐵 𝑃 𝐶 ) ) )