Theorem ipasslem11

Description: Lemma for ipassi . Show the inner product associative law for all complex numbers. (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
	ipasslem11.a	⊢ 𝐴 ∈ 𝑋
	ipasslem11.b	⊢ 𝐵 ∈ 𝑋
Assertion	ipasslem11	⊢ ( 𝐶 ∈ ℂ → ( ( 𝐶 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) )

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		ipasslem11.a	⊢ 𝐴 ∈ 𝑋
7		ipasslem11.b	⊢ 𝐵 ∈ 𝑋
8		cnre	⊢ ( 𝐶 ∈ ℂ → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝐶 = ( 𝑥 + ( i · 𝑦 ) ) )
9		ax-icn	⊢ i ∈ ℂ
10		recn	⊢ ( 𝑦 ∈ ℝ → 𝑦 ∈ ℂ )
11		mulcom	⊢ ( ( i ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( i · 𝑦 ) = ( 𝑦 · i ) )
12	9 10 11	sylancr	⊢ ( 𝑦 ∈ ℝ → ( i · 𝑦 ) = ( 𝑦 · i ) )
13	12	adantl	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( i · 𝑦 ) = ( 𝑦 · i ) )
14	13	oveq2d	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝑥 + ( i · 𝑦 ) ) = ( 𝑥 + ( 𝑦 · i ) ) )
15	14	eqeq2d	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝐶 = ( 𝑥 + ( i · 𝑦 ) ) ↔ 𝐶 = ( 𝑥 + ( 𝑦 · i ) ) ) )
16		recn	⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℂ )
17	5	phnvi	⊢ 𝑈 ∈ NrmCVec
18	1 3	nvscl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑥 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( 𝑥 𝑆 𝐴 ) ∈ 𝑋 )
19	17 6 18	mp3an13	⊢ ( 𝑥 ∈ ℂ → ( 𝑥 𝑆 𝐴 ) ∈ 𝑋 )
20	16 19	syl	⊢ ( 𝑥 ∈ ℝ → ( 𝑥 𝑆 𝐴 ) ∈ 𝑋 )
21		mulcl	⊢ ( ( 𝑦 ∈ ℂ ∧ i ∈ ℂ ) → ( 𝑦 · i ) ∈ ℂ )
22	10 9 21	sylancl	⊢ ( 𝑦 ∈ ℝ → ( 𝑦 · i ) ∈ ℂ )
23	1 3	nvscl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑦 · i ) ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑦 · i ) 𝑆 𝐴 ) ∈ 𝑋 )
24	17 6 23	mp3an13	⊢ ( ( 𝑦 · i ) ∈ ℂ → ( ( 𝑦 · i ) 𝑆 𝐴 ) ∈ 𝑋 )
25	22 24	syl	⊢ ( 𝑦 ∈ ℝ → ( ( 𝑦 · i ) 𝑆 𝐴 ) ∈ 𝑋 )
26	1 2 3 4 5	ipdiri	⊢ ( ( ( 𝑥 𝑆 𝐴 ) ∈ 𝑋 ∧ ( ( 𝑦 · i ) 𝑆 𝐴 ) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( 𝑥 𝑆 𝐴 ) 𝐺 ( ( 𝑦 · i ) 𝑆 𝐴 ) ) 𝑃 𝐵 ) = ( ( ( 𝑥 𝑆 𝐴 ) 𝑃 𝐵 ) + ( ( ( 𝑦 · i ) 𝑆 𝐴 ) 𝑃 𝐵 ) ) )
27	7 26	mp3an3	⊢ ( ( ( 𝑥 𝑆 𝐴 ) ∈ 𝑋 ∧ ( ( 𝑦 · i ) 𝑆 𝐴 ) ∈ 𝑋 ) → ( ( ( 𝑥 𝑆 𝐴 ) 𝐺 ( ( 𝑦 · i ) 𝑆 𝐴 ) ) 𝑃 𝐵 ) = ( ( ( 𝑥 𝑆 𝐴 ) 𝑃 𝐵 ) + ( ( ( 𝑦 · i ) 𝑆 𝐴 ) 𝑃 𝐵 ) ) )
28	20 25 27	syl2an	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( ( 𝑥 𝑆 𝐴 ) 𝐺 ( ( 𝑦 · i ) 𝑆 𝐴 ) ) 𝑃 𝐵 ) = ( ( ( 𝑥 𝑆 𝐴 ) 𝑃 𝐵 ) + ( ( ( 𝑦 · i ) 𝑆 𝐴 ) 𝑃 𝐵 ) ) )
29	1 2 3 4 5 6 7	ipasslem9	⊢ ( 𝑥 ∈ ℝ → ( ( 𝑥 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝑥 · ( 𝐴 𝑃 𝐵 ) ) )
30	1 3	nvscl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ i ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( i 𝑆 𝐴 ) ∈ 𝑋 )
31	17 9 6 30	mp3an	⊢ ( i 𝑆 𝐴 ) ∈ 𝑋
32	1 2 3 4 5 31 7	ipasslem9	⊢ ( 𝑦 ∈ ℝ → ( ( 𝑦 𝑆 ( i 𝑆 𝐴 ) ) 𝑃 𝐵 ) = ( 𝑦 · ( ( i 𝑆 𝐴 ) 𝑃 𝐵 ) ) )
33	1 3	nvsass	⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑦 ∈ ℂ ∧ i ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) ) → ( ( 𝑦 · i ) 𝑆 𝐴 ) = ( 𝑦 𝑆 ( i 𝑆 𝐴 ) ) )
34	17 33	mpan	⊢ ( ( 𝑦 ∈ ℂ ∧ i ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑦 · i ) 𝑆 𝐴 ) = ( 𝑦 𝑆 ( i 𝑆 𝐴 ) ) )
35	9 6 34	mp3an23	⊢ ( 𝑦 ∈ ℂ → ( ( 𝑦 · i ) 𝑆 𝐴 ) = ( 𝑦 𝑆 ( i 𝑆 𝐴 ) ) )
36	10 35	syl	⊢ ( 𝑦 ∈ ℝ → ( ( 𝑦 · i ) 𝑆 𝐴 ) = ( 𝑦 𝑆 ( i 𝑆 𝐴 ) ) )
37	36	oveq1d	⊢ ( 𝑦 ∈ ℝ → ( ( ( 𝑦 · i ) 𝑆 𝐴 ) 𝑃 𝐵 ) = ( ( 𝑦 𝑆 ( i 𝑆 𝐴 ) ) 𝑃 𝐵 ) )
38	1 4	dipcl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑃 𝐵 ) ∈ ℂ )
39	17 6 7 38	mp3an	⊢ ( 𝐴 𝑃 𝐵 ) ∈ ℂ
40		mulass	⊢ ( ( 𝑦 ∈ ℂ ∧ i ∈ ℂ ∧ ( 𝐴 𝑃 𝐵 ) ∈ ℂ ) → ( ( 𝑦 · i ) · ( 𝐴 𝑃 𝐵 ) ) = ( 𝑦 · ( i · ( 𝐴 𝑃 𝐵 ) ) ) )
41	9 39 40	mp3an23	⊢ ( 𝑦 ∈ ℂ → ( ( 𝑦 · i ) · ( 𝐴 𝑃 𝐵 ) ) = ( 𝑦 · ( i · ( 𝐴 𝑃 𝐵 ) ) ) )
42	10 41	syl	⊢ ( 𝑦 ∈ ℝ → ( ( 𝑦 · i ) · ( 𝐴 𝑃 𝐵 ) ) = ( 𝑦 · ( i · ( 𝐴 𝑃 𝐵 ) ) ) )
43		eqid	⊢ ( normCV ‘ 𝑈 ) = ( normCV ‘ 𝑈 )
44	1 2 3 4 5 6 7 43	ipasslem10	⊢ ( ( i 𝑆 𝐴 ) 𝑃 𝐵 ) = ( i · ( 𝐴 𝑃 𝐵 ) )
45	44	oveq2i	⊢ ( 𝑦 · ( ( i 𝑆 𝐴 ) 𝑃 𝐵 ) ) = ( 𝑦 · ( i · ( 𝐴 𝑃 𝐵 ) ) )
46	42 45	eqtr4di	⊢ ( 𝑦 ∈ ℝ → ( ( 𝑦 · i ) · ( 𝐴 𝑃 𝐵 ) ) = ( 𝑦 · ( ( i 𝑆 𝐴 ) 𝑃 𝐵 ) ) )
47	32 37 46	3eqtr4d	⊢ ( 𝑦 ∈ ℝ → ( ( ( 𝑦 · i ) 𝑆 𝐴 ) 𝑃 𝐵 ) = ( ( 𝑦 · i ) · ( 𝐴 𝑃 𝐵 ) ) )
48	29 47	oveqan12d	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( ( 𝑥 𝑆 𝐴 ) 𝑃 𝐵 ) + ( ( ( 𝑦 · i ) 𝑆 𝐴 ) 𝑃 𝐵 ) ) = ( ( 𝑥 · ( 𝐴 𝑃 𝐵 ) ) + ( ( 𝑦 · i ) · ( 𝐴 𝑃 𝐵 ) ) ) )
49	28 48	eqtrd	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( ( 𝑥 𝑆 𝐴 ) 𝐺 ( ( 𝑦 · i ) 𝑆 𝐴 ) ) 𝑃 𝐵 ) = ( ( 𝑥 · ( 𝐴 𝑃 𝐵 ) ) + ( ( 𝑦 · i ) · ( 𝐴 𝑃 𝐵 ) ) ) )
50	1 2 3	nvdir	⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑥 ∈ ℂ ∧ ( 𝑦 · i ) ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) ) → ( ( 𝑥 + ( 𝑦 · i ) ) 𝑆 𝐴 ) = ( ( 𝑥 𝑆 𝐴 ) 𝐺 ( ( 𝑦 · i ) 𝑆 𝐴 ) ) )
51	17 50	mpan	⊢ ( ( 𝑥 ∈ ℂ ∧ ( 𝑦 · i ) ∈ ℂ ∧ 𝐴 ∈ 𝑋 ) → ( ( 𝑥 + ( 𝑦 · i ) ) 𝑆 𝐴 ) = ( ( 𝑥 𝑆 𝐴 ) 𝐺 ( ( 𝑦 · i ) 𝑆 𝐴 ) ) )
52	6 51	mp3an3	⊢ ( ( 𝑥 ∈ ℂ ∧ ( 𝑦 · i ) ∈ ℂ ) → ( ( 𝑥 + ( 𝑦 · i ) ) 𝑆 𝐴 ) = ( ( 𝑥 𝑆 𝐴 ) 𝐺 ( ( 𝑦 · i ) 𝑆 𝐴 ) ) )
53	16 22 52	syl2an	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( 𝑥 + ( 𝑦 · i ) ) 𝑆 𝐴 ) = ( ( 𝑥 𝑆 𝐴 ) 𝐺 ( ( 𝑦 · i ) 𝑆 𝐴 ) ) )
54	53	oveq1d	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( ( 𝑥 + ( 𝑦 · i ) ) 𝑆 𝐴 ) 𝑃 𝐵 ) = ( ( ( 𝑥 𝑆 𝐴 ) 𝐺 ( ( 𝑦 · i ) 𝑆 𝐴 ) ) 𝑃 𝐵 ) )
55		adddir	⊢ ( ( 𝑥 ∈ ℂ ∧ ( 𝑦 · i ) ∈ ℂ ∧ ( 𝐴 𝑃 𝐵 ) ∈ ℂ ) → ( ( 𝑥 + ( 𝑦 · i ) ) · ( 𝐴 𝑃 𝐵 ) ) = ( ( 𝑥 · ( 𝐴 𝑃 𝐵 ) ) + ( ( 𝑦 · i ) · ( 𝐴 𝑃 𝐵 ) ) ) )
56	39 55	mp3an3	⊢ ( ( 𝑥 ∈ ℂ ∧ ( 𝑦 · i ) ∈ ℂ ) → ( ( 𝑥 + ( 𝑦 · i ) ) · ( 𝐴 𝑃 𝐵 ) ) = ( ( 𝑥 · ( 𝐴 𝑃 𝐵 ) ) + ( ( 𝑦 · i ) · ( 𝐴 𝑃 𝐵 ) ) ) )
57	16 22 56	syl2an	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( 𝑥 + ( 𝑦 · i ) ) · ( 𝐴 𝑃 𝐵 ) ) = ( ( 𝑥 · ( 𝐴 𝑃 𝐵 ) ) + ( ( 𝑦 · i ) · ( 𝐴 𝑃 𝐵 ) ) ) )
58	49 54 57	3eqtr4d	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( ( 𝑥 + ( 𝑦 · i ) ) 𝑆 𝐴 ) 𝑃 𝐵 ) = ( ( 𝑥 + ( 𝑦 · i ) ) · ( 𝐴 𝑃 𝐵 ) ) )
59		oveq1	⊢ ( 𝐶 = ( 𝑥 + ( 𝑦 · i ) ) → ( 𝐶 𝑆 𝐴 ) = ( ( 𝑥 + ( 𝑦 · i ) ) 𝑆 𝐴 ) )
60	59	oveq1d	⊢ ( 𝐶 = ( 𝑥 + ( 𝑦 · i ) ) → ( ( 𝐶 𝑆 𝐴 ) 𝑃 𝐵 ) = ( ( ( 𝑥 + ( 𝑦 · i ) ) 𝑆 𝐴 ) 𝑃 𝐵 ) )
61		oveq1	⊢ ( 𝐶 = ( 𝑥 + ( 𝑦 · i ) ) → ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) = ( ( 𝑥 + ( 𝑦 · i ) ) · ( 𝐴 𝑃 𝐵 ) ) )
62	60 61	eqeq12d	⊢ ( 𝐶 = ( 𝑥 + ( 𝑦 · i ) ) → ( ( ( 𝐶 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ↔ ( ( ( 𝑥 + ( 𝑦 · i ) ) 𝑆 𝐴 ) 𝑃 𝐵 ) = ( ( 𝑥 + ( 𝑦 · i ) ) · ( 𝐴 𝑃 𝐵 ) ) ) )
63	58 62	syl5ibrcom	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝐶 = ( 𝑥 + ( 𝑦 · i ) ) → ( ( 𝐶 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) )
64	15 63	sylbid	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝐶 = ( 𝑥 + ( i · 𝑦 ) ) → ( ( 𝐶 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) ) )
65	64	rexlimivv	⊢ ( ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝐶 = ( 𝑥 + ( i · 𝑦 ) ) → ( ( 𝐶 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) )
66	8 65	syl	⊢ ( 𝐶 ∈ ℂ → ( ( 𝐶 𝑆 𝐴 ) 𝑃 𝐵 ) = ( 𝐶 · ( 𝐴 𝑃 𝐵 ) ) )