ip2dii

Description: Inner product of two sums. (Contributed by NM, 17-Apr-2008) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ip2dii.1	$⊢ X = BaseSet (U)$
	ip2dii.2	$⊢ G = +_{v} (U)$
	ip2dii.7	$⊢ P = \cdot_{𝑖OLD} (U)$
	ip2dii.u	$⊢ U \in {CPreHil}_{OLD}$
	ip2dii.a	$⊢ A \in X$
	ip2dii.b	$⊢ B \in X$
	ip2dii.c	$⊢ C \in X$
	ip2dii.d	$⊢ D \in X$
Assertion	ip2dii	$⊢ (A G B) P (C G D) = (A P C) + (B P D) + (A P D) + (B P C)$

Proof

Step	Hyp	Ref	Expression
1		ip2dii.1	$⊢ X = BaseSet (U)$
2		ip2dii.2	$⊢ G = +_{v} (U)$
3		ip2dii.7	$⊢ P = \cdot_{𝑖OLD} (U)$
4		ip2dii.u	$⊢ U \in {CPreHil}_{OLD}$
5		ip2dii.a	$⊢ A \in X$
6		ip2dii.b	$⊢ B \in X$
7		ip2dii.c	$⊢ C \in X$
8		ip2dii.d	$⊢ D \in X$
9	5 7 8	3pm3.2i	$⊢ (A \in X \land C \in X \land D \in X)$
10	1 2 3	dipdi	$⊢ (U \in {CPreHil}_{OLD} \land (A \in X \land C \in X \land D \in X)) \to A P (C G D) = (A P C) + (A P D)$
11	4 9 10	mp2an	$⊢ A P (C G D) = (A P C) + (A P D)$
12	6 7 8	3pm3.2i	$⊢ (B \in X \land C \in X \land D \in X)$
13	1 2 3	dipdi	$⊢ (U \in {CPreHil}_{OLD} \land (B \in X \land C \in X \land D \in X)) \to B P (C G D) = (B P C) + (B P D)$
14	4 12 13	mp2an	$⊢ B P (C G D) = (B P C) + (B P D)$
15	11 14	oveq12i	$⊢ (A P (C G D)) + (B P (C G D)) = (A P C) + (A P D) + (B P C) + (B P D)$
16	4	phnvi	$⊢ U \in NrmCVec$
17	1 2	nvgcl	$⊢ (U \in NrmCVec \land C \in X \land D \in X) \to C G D \in X$
18	16 7 8 17	mp3an	$⊢ C G D \in X$
19	5 6 18	3pm3.2i	$⊢ (A \in X \land B \in X \land C G D \in X)$
20	1 2 3	dipdir	$⊢ (U \in {CPreHil}_{OLD} \land (A \in X \land B \in X \land C G D \in X)) \to (A G B) P (C G D) = (A P (C G D)) + (B P (C G D))$
21	4 19 20	mp2an	$⊢ (A G B) P (C G D) = (A P (C G D)) + (B P (C G D))$
22	1 3	dipcl	$⊢ (U \in NrmCVec \land A \in X \land C \in X) \to A P C \in ℂ$
23	16 5 7 22	mp3an	$⊢ A P C \in ℂ$
24	1 3	dipcl	$⊢ (U \in NrmCVec \land B \in X \land D \in X) \to B P D \in ℂ$
25	16 6 8 24	mp3an	$⊢ B P D \in ℂ$
26	1 3	dipcl	$⊢ (U \in NrmCVec \land A \in X \land D \in X) \to A P D \in ℂ$
27	16 5 8 26	mp3an	$⊢ A P D \in ℂ$
28	1 3	dipcl	$⊢ (U \in NrmCVec \land B \in X \land C \in X) \to B P C \in ℂ$
29	16 6 7 28	mp3an	$⊢ B P C \in ℂ$
30	23 25 27 29	add42i	$⊢ (A P C) + (B P D) + (A P D) + (B P C) = (A P C) + (A P D) + (B P C) + (B P D)$
31	15 21 30	3eqtr4i	$⊢ (A G B) P (C G D) = (A P C) + (B P D) + (A P D) + (B P C)$

Metamath Proof Explorer

Theorem ip2dii

Proof