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	$⊢ X = BaseSet (U)$
	ip1i.2	$⊢ G = +_{v} (U)$
	ip1i.4	$⊢ S = \cdot_{𝑠OLD} (U)$
	ip1i.7	$⊢ P = \cdot_{𝑖OLD} (U)$
	ip1i.9	$⊢ U \in {CPreHil}_{OLD}$
	ipasslem11.a	$⊢ A \in X$
	ipasslem11.b	$⊢ B \in X$
Assertion	ipasslem11	$⊢ C \in ℂ \to (C S A) P B = C (A P B)$

Proof

Step	Hyp	Ref	Expression
1		ip1i.1	$⊢ X = BaseSet (U)$
2		ip1i.2	$⊢ G = +_{v} (U)$
3		ip1i.4	$⊢ S = \cdot_{𝑠OLD} (U)$
4		ip1i.7	$⊢ P = \cdot_{𝑖OLD} (U)$
5		ip1i.9	$⊢ U \in {CPreHil}_{OLD}$
6		ipasslem11.a	$⊢ A \in X$
7		ipasslem11.b	$⊢ B \in X$
8		cnre	$⊢ C \in ℂ \to \exists x \in ℝ \exists y \in ℝ C = x + i y$
9		ax-icn	$⊢ i \in ℂ$
10		recn	$⊢ y \in ℝ \to y \in ℂ$
11		mulcom	$⊢ (i \in ℂ \land y \in ℂ) \to i y = y i$
12	9 10 11	sylancr	$⊢ y \in ℝ \to i y = y i$
13	12	adantl	$⊢ (x \in ℝ \land y \in ℝ) \to i y = y i$
14	13	oveq2d	$⊢ (x \in ℝ \land y \in ℝ) \to x + i y = x + y i$
15	14	eqeq2d	$⊢ (x \in ℝ \land y \in ℝ) \to (C = x + i y \leftrightarrow C = x + y i)$
16		recn	$⊢ x \in ℝ \to x \in ℂ$
17	5	phnvi	$⊢ U \in NrmCVec$
18	1 3	nvscl	$⊢ (U \in NrmCVec \land x \in ℂ \land A \in X) \to x S A \in X$
19	17 6 18	mp3an13	$⊢ x \in ℂ \to x S A \in X$
20	16 19	syl	$⊢ x \in ℝ \to x S A \in X$
21		mulcl	$⊢ (y \in ℂ \land i \in ℂ) \to y i \in ℂ$
22	10 9 21	sylancl	$⊢ y \in ℝ \to y i \in ℂ$
23	1 3	nvscl	$⊢ (U \in NrmCVec \land y i \in ℂ \land A \in X) \to y i S A \in X$
24	17 6 23	mp3an13	$⊢ y i \in ℂ \to y i S A \in X$
25	22 24	syl	$⊢ y \in ℝ \to y i S A \in X$
26	1 2 3 4 5	ipdiri	$⊢ (x S A \in X \land y i S A \in X \land B \in X) \to ((x S A) G (y i S A)) P B = ((x S A) P B) + ((y i S A) P B)$
27	7 26	mp3an3	$⊢ (x S A \in X \land y i S A \in X) \to ((x S A) G (y i S A)) P B = ((x S A) P B) + ((y i S A) P B)$
28	20 25 27	syl2an	$⊢ (x \in ℝ \land y \in ℝ) \to ((x S A) G (y i S A)) P B = ((x S A) P B) + ((y i S A) P B)$
29	1 2 3 4 5 6 7	ipasslem9	$⊢ x \in ℝ \to (x S A) P B = x (A P B)$
30	1 3	nvscl	$⊢ (U \in NrmCVec \land i \in ℂ \land A \in X) \to i S A \in X$
31	17 9 6 30	mp3an	$⊢ i S A \in X$
32	1 2 3 4 5 31 7	ipasslem9	$⊢ y \in ℝ \to (y S (i S A)) P B = y ((i S A) P B)$
33	1 3	nvsass	$⊢ (U \in NrmCVec \land (y \in ℂ \land i \in ℂ \land A \in X)) \to y i S A = y S (i S A)$
34	17 33	mpan	$⊢ (y \in ℂ \land i \in ℂ \land A \in X) \to y i S A = y S (i S A)$
35	9 6 34	mp3an23	$⊢ y \in ℂ \to y i S A = y S (i S A)$
36	10 35	syl	$⊢ y \in ℝ \to y i S A = y S (i S A)$
37	36	oveq1d	$⊢ y \in ℝ \to (y i S A) P B = (y S (i S A)) P B$
38	1 4	dipcl	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to A P B \in ℂ$
39	17 6 7 38	mp3an	$⊢ A P B \in ℂ$
40		mulass	$⊢ (y \in ℂ \land i \in ℂ \land A P B \in ℂ) \to y i (A P B) = y i (A P B)$
41	9 39 40	mp3an23	$⊢ y \in ℂ \to y i (A P B) = y i (A P B)$
42	10 41	syl	$⊢ y \in ℝ \to y i (A P B) = y i (A P B)$
43		eqid	$⊢ {norm}_{CV} (U) = {norm}_{CV} (U)$
44	1 2 3 4 5 6 7 43	ipasslem10	$⊢ (i S A) P B = i (A P B)$
45	44	oveq2i	$⊢ y ((i S A) P B) = y i (A P B)$
46	42 45	eqtr4di	$⊢ y \in ℝ \to y i (A P B) = y ((i S A) P B)$
47	32 37 46	3eqtr4d	$⊢ y \in ℝ \to (y i S A) P B = y i (A P B)$
48	29 47	oveqan12d	$⊢ (x \in ℝ \land y \in ℝ) \to ((x S A) P B) + ((y i S A) P B) = x (A P B) + y i (A P B)$
49	28 48	eqtrd	$⊢ (x \in ℝ \land y \in ℝ) \to ((x S A) G (y i S A)) P B = x (A P B) + y i (A P B)$
50	1 2 3	nvdir	$⊢ (U \in NrmCVec \land (x \in ℂ \land y i \in ℂ \land A \in X)) \to (x + y i) S A = (x S A) G (y i S A)$
51	17 50	mpan	$⊢ (x \in ℂ \land y i \in ℂ \land A \in X) \to (x + y i) S A = (x S A) G (y i S A)$
52	6 51	mp3an3	$⊢ (x \in ℂ \land y i \in ℂ) \to (x + y i) S A = (x S A) G (y i S A)$
53	16 22 52	syl2an	$⊢ (x \in ℝ \land y \in ℝ) \to (x + y i) S A = (x S A) G (y i S A)$
54	53	oveq1d	$⊢ (x \in ℝ \land y \in ℝ) \to ((x + y i) S A) P B = ((x S A) G (y i S A)) P B$
55		adddir	$⊢ (x \in ℂ \land y i \in ℂ \land A P B \in ℂ) \to (x + y i) (A P B) = x (A P B) + y i (A P B)$
56	39 55	mp3an3	$⊢ (x \in ℂ \land y i \in ℂ) \to (x + y i) (A P B) = x (A P B) + y i (A P B)$
57	16 22 56	syl2an	$⊢ (x \in ℝ \land y \in ℝ) \to (x + y i) (A P B) = x (A P B) + y i (A P B)$
58	49 54 57	3eqtr4d	$⊢ (x \in ℝ \land y \in ℝ) \to ((x + y i) S A) P B = (x + y i) (A P B)$
59		oveq1	$⊢ C = x + y i \to C S A = (x + y i) S A$
60	59	oveq1d	$⊢ C = x + y i \to (C S A) P B = ((x + y i) S A) P B$
61		oveq1	$⊢ C = x + y i \to C (A P B) = (x + y i) (A P B)$
62	60 61	eqeq12d	$⊢ C = x + y i \to ((C S A) P B = C (A P B) \leftrightarrow ((x + y i) S A) P B = (x + y i) (A P B))$
63	58 62	syl5ibrcom	$⊢ (x \in ℝ \land y \in ℝ) \to (C = x + y i \to (C S A) P B = C (A P B))$
64	15 63	sylbid	$⊢ (x \in ℝ \land y \in ℝ) \to (C = x + i y \to (C S A) P B = C (A P B))$
65	64	rexlimivv	$⊢ \exists x \in ℝ \exists y \in ℝ C = x + i y \to (C S A) P B = C (A P B)$
66	8 65	syl	$⊢ C \in ℂ \to (C S A) P B = C (A P B)$

Metamath Proof Explorer

Theorem ipasslem11

Proof