Theorem ipassi

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	ip1i.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
	ip1i.2	⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
	ip1i.4	⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 )
	ip1i.7	⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
	ip1i.9	⊢ 𝑈 ∈ CPreHilOLD
Assertion	ipassi	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( ( 𝐴 𝑆 𝐵 ) 𝑃 𝐶 ) = ( 𝐴 · ( 𝐵 𝑃 𝐶 ) ) )

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		oveq2	⊢ ( 𝐵 = if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) → ( 𝐴 𝑆 𝐵 ) = ( 𝐴 𝑆 if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) ) )
7	6	oveq1d	⊢ ( 𝐵 = if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) → ( ( 𝐴 𝑆 𝐵 ) 𝑃 𝐶 ) = ( ( 𝐴 𝑆 if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) ) 𝑃 𝐶 ) )
8		oveq1	⊢ ( 𝐵 = if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) → ( 𝐵 𝑃 𝐶 ) = ( if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) 𝑃 𝐶 ) )
9	8	oveq2d	⊢ ( 𝐵 = if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) → ( 𝐴 · ( 𝐵 𝑃 𝐶 ) ) = ( 𝐴 · ( if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) 𝑃 𝐶 ) ) )
10	7 9	eqeq12d	⊢ ( 𝐵 = if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) → ( ( ( 𝐴 𝑆 𝐵 ) 𝑃 𝐶 ) = ( 𝐴 · ( 𝐵 𝑃 𝐶 ) ) ↔ ( ( 𝐴 𝑆 if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) ) 𝑃 𝐶 ) = ( 𝐴 · ( if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) 𝑃 𝐶 ) ) ) )
11	10	imbi2d	⊢ ( 𝐵 = if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) → ( ( 𝐴 ∈ ℂ → ( ( 𝐴 𝑆 𝐵 ) 𝑃 𝐶 ) = ( 𝐴 · ( 𝐵 𝑃 𝐶 ) ) ) ↔ ( 𝐴 ∈ ℂ → ( ( 𝐴 𝑆 if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) ) 𝑃 𝐶 ) = ( 𝐴 · ( if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) 𝑃 𝐶 ) ) ) ) )
12		oveq2	⊢ ( 𝐶 = if ( 𝐶 ∈ 𝑋 , 𝐶 , ( 0vec ‘ 𝑈 ) ) → ( ( 𝐴 𝑆 if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) ) 𝑃 𝐶 ) = ( ( 𝐴 𝑆 if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) ) 𝑃 if ( 𝐶 ∈ 𝑋 , 𝐶 , ( 0vec ‘ 𝑈 ) ) ) )
13		oveq2	⊢ ( 𝐶 = if ( 𝐶 ∈ 𝑋 , 𝐶 , ( 0vec ‘ 𝑈 ) ) → ( if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) 𝑃 𝐶 ) = ( 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	15	imbi2d	⊢ ( 𝐶 = if ( 𝐶 ∈ 𝑋 , 𝐶 , ( 0vec ‘ 𝑈 ) ) → ( ( 𝐴 ∈ ℂ → ( ( 𝐴 𝑆 if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) ) 𝑃 𝐶 ) = ( 𝐴 · ( if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) 𝑃 𝐶 ) ) ) ↔ ( 𝐴 ∈ ℂ → ( ( 𝐴 𝑆 if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) ) 𝑃 if ( 𝐶 ∈ 𝑋 , 𝐶 , ( 0vec ‘ 𝑈 ) ) ) = ( 𝐴 · ( if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) 𝑃 if ( 𝐶 ∈ 𝑋 , 𝐶 , ( 0vec ‘ 𝑈 ) ) ) ) ) ) )
17		eqid	⊢ ( 0vec ‘ 𝑈 ) = ( 0vec ‘ 𝑈 )
18	1 17 5	elimph	⊢ if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) ∈ 𝑋
19	1 17 5	elimph	⊢ if ( 𝐶 ∈ 𝑋 , 𝐶 , ( 0vec ‘ 𝑈 ) ) ∈ 𝑋
20	1 2 3 4 5 18 19	ipasslem11	⊢ ( 𝐴 ∈ ℂ → ( ( 𝐴 𝑆 if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) ) 𝑃 if ( 𝐶 ∈ 𝑋 , 𝐶 , ( 0vec ‘ 𝑈 ) ) ) = ( 𝐴 · ( if ( 𝐵 ∈ 𝑋 , 𝐵 , ( 0vec ‘ 𝑈 ) ) 𝑃 if ( 𝐶 ∈ 𝑋 , 𝐶 , ( 0vec ‘ 𝑈 ) ) ) ) )
21	11 16 20	dedth2h	⊢ ( ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( 𝐴 ∈ ℂ → ( ( 𝐴 𝑆 𝐵 ) 𝑃 𝐶 ) = ( 𝐴 · ( 𝐵 𝑃 𝐶 ) ) ) )
22	21	com12	⊢ ( 𝐴 ∈ ℂ → ( ( 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( ( 𝐴 𝑆 𝐵 ) 𝑃 𝐶 ) = ( 𝐴 · ( 𝐵 𝑃 𝐶 ) ) ) )
23	22	3impib	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋 ) → ( ( 𝐴 𝑆 𝐵 ) 𝑃 𝐶 ) = ( 𝐴 · ( 𝐵 𝑃 𝐶 ) ) )