Metamath Proof Explorer

Theorem ipdiri

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

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

Proof

Step Hyp Ref Expression
1 ip1i.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 ip1i.2 ⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
3 ip1i.4 ⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
4 ip1i.7 ⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
5 ip1i.9 ⊢ 𝑈 ∈ CPreHilOLD
6 oveq1 ⊢ ( 𝐴 = if ( 𝐴 ∈ 𝑋 , 𝐴 , ( 0vec ‘ 𝑈 ) ) → ( 𝐴 𝐺 𝐵 ) = ( if ( 𝐴 ∈ 𝑋 , 𝐴 , ( 0vec ‘ 𝑈 ) ) 𝐺 𝐵 ) )
7 6 oveq1d ⊢ ( 𝐴 = if ( 𝐴 ∈ 𝑋 , 𝐴 , ( 0vec ‘ 𝑈 ) ) → ( ( 𝐴 𝐺 𝐵 ) 𝑃 𝐶 ) = ( ( if ( 𝐴 ∈ 𝑋 , 𝐴 , ( 0vec ‘ 𝑈 ) ) 𝐺 𝐵 ) 𝑃 𝐶 ) )
8 oveq1 ⊢ ( 𝐴 = if ( 𝐴 ∈ 𝑋 , 𝐴 , ( 0vec ‘ 𝑈 ) ) → ( 𝐴 𝑃 𝐶 ) = ( if ( 𝐴 ∈ 𝑋 , 𝐴 , ( 0vec ‘ 𝑈 ) ) 𝑃 𝐶 ) )
9 8 oveq1d ⊢ ( 𝐴 = if ( 𝐴 ∈ 𝑋 , 𝐴 , ( 0vec ‘ 𝑈 ) ) → ( ( 𝐴 𝑃 𝐶 ) + ( 𝐵 𝑃 𝐶 ) ) = ( ( if ( 𝐴 ∈ 𝑋 , 𝐴 , ( 0vec ‘ 𝑈 ) ) 𝑃 𝐶 ) + ( 𝐵 𝑃 𝐶 ) ) )
10 7 9 eqeq12d ⊢ ( 𝐴 = if ( 𝐴 ∈ 𝑋 , 𝐴 , ( 0vec ‘ 𝑈 ) ) → ( ( ( 𝐴 𝐺 𝐵 ) 𝑃 𝐶 ) = ( ( 𝐴 𝑃 𝐶 ) + ( 𝐵 𝑃 𝐶 ) ) ↔ ( ( if ( 𝐴 ∈ 𝑋 , 𝐴 , ( 0vec ‘ 𝑈 ) ) 𝐺 𝐵 ) 𝑃 𝐶 ) = ( ( if ( 𝐴 ∈ 𝑋 , 𝐴 , ( 0vec ‘ 𝑈 ) ) 𝑃 𝐶 ) + ( 𝐵 𝑃 𝐶 ) ) ) )
11 oveq2 ⊢ ( 𝐵 = if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) → ( if ( 𝐴 ∈ 𝑋 , 𝐴 , ( 0vec ‘ 𝑈 ) ) 𝐺 𝐵 ) = ( if ( 𝐴 ∈ 𝑋 , 𝐴 , ( 0vec ‘ 𝑈 ) ) 𝐺 if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) ) )
12 11 oveq1d ⊢ ( 𝐵 = if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) → ( ( if ( 𝐴 ∈ 𝑋 , 𝐴 , ( 0vec ‘ 𝑈 ) ) 𝐺 𝐵 ) 𝑃 𝐶 ) = ( ( if ( 𝐴 ∈ 𝑋 , 𝐴 , ( 0vec ‘ 𝑈 ) ) 𝐺 if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) ) 𝑃 𝐶 ) )
13 oveq1 ⊢ ( 𝐵 = if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) → ( 𝐵 𝑃 𝐶 ) = ( if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) 𝑃 𝐶 ) )
14 13 oveq2d ⊢ ( 𝐵 = if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) → ( ( if ( 𝐴 ∈ 𝑋 , 𝐴 , ( 0vec ‘ 𝑈 ) ) 𝑃 𝐶 ) + ( 𝐵 𝑃 𝐶 ) ) = ( ( if ( 𝐴 ∈ 𝑋 , 𝐴 , ( 0vec ‘ 𝑈 ) ) 𝑃 𝐶 ) + ( if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) 𝑃 𝐶 ) ) )
15 12 14 eqeq12d ⊢ ( 𝐵 = if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) → ( ( ( if ( 𝐴 ∈ 𝑋 , 𝐴 , ( 0vec ‘ 𝑈 ) ) 𝐺 𝐵 ) 𝑃 𝐶 ) = ( ( if ( 𝐴 ∈ 𝑋 , 𝐴 , ( 0vec ‘ 𝑈 ) ) 𝑃 𝐶 ) + ( 𝐵 𝑃 𝐶 ) ) ↔ ( ( if ( 𝐴 ∈ 𝑋 , 𝐴 , ( 0vec ‘ 𝑈 ) ) 𝐺 if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) ) 𝑃 𝐶 ) = ( ( if ( 𝐴 ∈ 𝑋 , 𝐴 , ( 0vec ‘ 𝑈 ) ) 𝑃 𝐶 ) + ( if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) 𝑃 𝐶 ) ) ) )
16 oveq2 ⊢ ( 𝐶 = if ( 𝐶 ∈ 𝑋 , 𝐶 , ( 0vec ‘ 𝑈 ) ) → ( ( if ( 𝐴 ∈ 𝑋 , 𝐴 , ( 0vec ‘ 𝑈 ) ) 𝐺 if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) ) 𝑃 𝐶 ) = ( ( if ( 𝐴 ∈ 𝑋 , 𝐴 , ( 0vec ‘ 𝑈 ) ) 𝐺 if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) ) 𝑃 if ( 𝐶 ∈ 𝑋 , 𝐶 , ( 0vec ‘ 𝑈 ) ) ) )
17 oveq2 ⊢ ( 𝐶 = if ( 𝐶 ∈ 𝑋 , 𝐶 , ( 0vec ‘ 𝑈 ) ) → ( if ( 𝐴 ∈ 𝑋 , 𝐴 , ( 0vec ‘ 𝑈 ) ) 𝑃 𝐶 ) = ( if ( 𝐴 ∈ 𝑋 , 𝐴 , ( 0vec ‘ 𝑈 ) ) 𝑃 if ( 𝐶 ∈ 𝑋 , 𝐶 , ( 0vec ‘ 𝑈 ) ) ) )
18 oveq2 ⊢ ( 𝐶 = if ( 𝐶 ∈ 𝑋 , 𝐶 , ( 0vec ‘ 𝑈 ) ) → ( if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) 𝑃 𝐶 ) = ( if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) 𝑃 if ( 𝐶 ∈ 𝑋 , 𝐶 , ( 0vec ‘ 𝑈 ) ) ) )
19 17 18 oveq12d ⊢ ( 𝐶 = if ( 𝐶 ∈ 𝑋 , 𝐶 , ( 0vec ‘ 𝑈 ) ) → ( ( if ( 𝐴 ∈ 𝑋 , 𝐴 , ( 0vec ‘ 𝑈 ) ) 𝑃 𝐶 ) + ( if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) 𝑃 𝐶 ) ) = ( ( if ( 𝐴 ∈ 𝑋 , 𝐴 , ( 0vec ‘ 𝑈 ) ) 𝑃 if ( 𝐶 ∈ 𝑋 , 𝐶 , ( 0vec ‘ 𝑈 ) ) ) + ( if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) 𝑃 if ( 𝐶 ∈ 𝑋 , 𝐶 , ( 0vec ‘ 𝑈 ) ) ) ) )
20 16 19 eqeq12d ⊢ ( 𝐶 = if ( 𝐶 ∈ 𝑋 , 𝐶 , ( 0vec ‘ 𝑈 ) ) → ( ( ( if ( 𝐴 ∈ 𝑋 , 𝐴 , ( 0vec ‘ 𝑈 ) ) 𝐺 if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) ) 𝑃 𝐶 ) = ( ( if ( 𝐴 ∈ 𝑋 , 𝐴 , ( 0vec ‘ 𝑈 ) ) 𝑃 𝐶 ) + ( if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) 𝑃 𝐶 ) ) ↔ ( ( if ( 𝐴 ∈ 𝑋 , 𝐴 , ( 0vec ‘ 𝑈 ) ) 𝐺 if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) ) 𝑃 if ( 𝐶 ∈ 𝑋 , 𝐶 , ( 0vec ‘ 𝑈 ) ) ) = ( ( if ( 𝐴 ∈ 𝑋 , 𝐴 , ( 0vec ‘ 𝑈 ) ) 𝑃 if ( 𝐶 ∈ 𝑋 , 𝐶 , ( 0vec ‘ 𝑈 ) ) ) + ( if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) 𝑃 if ( 𝐶 ∈ 𝑋 , 𝐶 , ( 0vec ‘ 𝑈 ) ) ) ) ) )
21 eqid ⊢ ( 0vec ‘ 𝑈 ) = ( 0vec ‘ 𝑈 )
22 1 21 5 elimph ⊢ if ( 𝐴 ∈ 𝑋 , 𝐴 , ( 0vec ‘ 𝑈 ) ) ∈ 𝑋
23 1 21 5 elimph ⊢ if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) ∈ 𝑋
24 1 21 5 elimph ⊢ if ( 𝐶 ∈ 𝑋 , 𝐶 , ( 0vec ‘ 𝑈 ) ) ∈ 𝑋
25 1 2 3 4 5 22 23 24 ipdirilem ⊢ ( ( if ( 𝐴 ∈ 𝑋 , 𝐴 , ( 0vec ‘ 𝑈 ) ) 𝐺 if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) ) 𝑃 if ( 𝐶 ∈ 𝑋 , 𝐶 , ( 0vec ‘ 𝑈 ) ) ) = ( ( if ( 𝐴 ∈ 𝑋 , 𝐴 , ( 0vec ‘ 𝑈 ) ) 𝑃 if ( 𝐶 ∈ 𝑋 , 𝐶 , ( 0vec ‘ 𝑈 ) ) ) + ( if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) 𝑃 if ( 𝐶 ∈ 𝑋 , 𝐶 , ( 0vec ‘ 𝑈 ) ) ) )
26 10 15 20 25 dedth3h ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( ( 𝐴 𝐺 𝐵 ) 𝑃 𝐶 ) = ( ( 𝐴 𝑃 𝐶 ) + ( 𝐵 𝑃 𝐶 ) ) )