ip2i

Description: Equation 6.48 of Ponnusamy p. 362. (Contributed by NM, 26-Apr-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}$
	ip2i.8	$⊢ A \in X$
	ip2i.9	$⊢ B \in X$
Assertion	ip2i	$⊢ (2 S A) P B = 2 (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		ip2i.8	$⊢ A \in X$
7		ip2i.9	$⊢ B \in X$
8	5	phnvi	$⊢ U \in NrmCVec$
9	1 2	nvgcl	$⊢ (U \in NrmCVec \land A \in X \land A \in X) \to A G A \in X$
10	8 6 6 9	mp3an	$⊢ A G A \in X$
11	1 4	dipcl	$⊢ (U \in NrmCVec \land A G A \in X \land B \in X) \to (A G A) P B \in ℂ$
12	8 10 7 11	mp3an	$⊢ (A G A) P B \in ℂ$
13	12	addridi	$⊢ ((A G A) P B) + 0 = (A G A) P B$
14		eqid	$⊢ 0_{vec} (U) = 0_{vec} (U)$
15	1 2 3 14	nvrinv	$⊢ (U \in NrmCVec \land A \in X) \to A G (-1 S A) = 0_{vec} (U)$
16	8 6 15	mp2an	$⊢ A G (-1 S A) = 0_{vec} (U)$
17	16	oveq1i	$⊢ (A G (-1 S A)) P B = 0_{vec} (U) P B$
18	1 14 4	dip0l	$⊢ (U \in NrmCVec \land B \in X) \to 0_{vec} (U) P B = 0$
19	8 7 18	mp2an	$⊢ 0_{vec} (U) P B = 0$
20	17 19	eqtri	$⊢ (A G (-1 S A)) P B = 0$
21	20	oveq2i	$⊢ ((A G A) P B) + ((A G (-1 S A)) P B) = ((A G A) P B) + 0$
22		df-2	$⊢ 2 = 1 + 1$
23	22	oveq1i	$⊢ 2 S A = (1 + 1) S A$
24		ax-1cn	$⊢ 1 \in ℂ$
25	24 24 6	3pm3.2i	$⊢ (1 \in ℂ \land 1 \in ℂ \land A \in X)$
26	1 2 3	nvdir	$⊢ (U \in NrmCVec \land (1 \in ℂ \land 1 \in ℂ \land A \in X)) \to (1 + 1) S A = (1 S A) G (1 S A)$
27	8 25 26	mp2an	$⊢ (1 + 1) S A = (1 S A) G (1 S A)$
28	1 3	nvsid	$⊢ (U \in NrmCVec \land A \in X) \to 1 S A = A$
29	8 6 28	mp2an	$⊢ 1 S A = A$
30	29 29	oveq12i	$⊢ (1 S A) G (1 S A) = A G A$
31	27 30	eqtri	$⊢ (1 + 1) S A = A G A$
32	23 31	eqtri	$⊢ 2 S A = A G A$
33	32	oveq1i	$⊢ (2 S A) P B = (A G A) P B$
34	13 21 33	3eqtr4ri	$⊢ (2 S A) P B = ((A G A) P B) + ((A G (-1 S A)) P B)$
35	1 2 3 4 5 6 6 7	ip1i	$⊢ ((A G A) P B) + ((A G (-1 S A)) P B) = 2 (A P B)$
36	34 35	eqtri	$⊢ (2 S A) P B = 2 (A P B)$

Metamath Proof Explorer

Theorem ip2i

Proof