dipassr

Description: "Associative" law for second argument of inner product (compare dipass ). (Contributed by NM, 22-Nov-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	ipass.1	$⊢ X = BaseSet (U)$
	ipass.4	$⊢ S = \cdot_{𝑠OLD} (U)$
	ipass.7	$⊢ P = \cdot_{𝑖OLD} (U)$
Assertion	dipassr	$⊢ (U \in {CPreHil}_{OLD} \land (A \in X \land B \in ℂ \land C \in X)) \to A P (B S C) = \overline{B} (A P C)$

Proof

Step	Hyp	Ref	Expression
1		ipass.1	$⊢ X = BaseSet (U)$
2		ipass.4	$⊢ S = \cdot_{𝑠OLD} (U)$
3		ipass.7	$⊢ P = \cdot_{𝑖OLD} (U)$
4		3anrot	$⊢ (A \in X \land B \in ℂ \land C \in X) \leftrightarrow (B \in ℂ \land C \in X \land A \in X)$
5	1 2 3	dipass	$⊢ (U \in {CPreHil}_{OLD} \land (B \in ℂ \land C \in X \land A \in X)) \to (B S C) P A = B (C P A)$
6	4 5	sylan2b	$⊢ (U \in {CPreHil}_{OLD} \land (A \in X \land B \in ℂ \land C \in X)) \to (B S C) P A = B (C P A)$
7	6	fveq2d	$⊢ (U \in {CPreHil}_{OLD} \land (A \in X \land B \in ℂ \land C \in X)) \to \overline{(B S C) P A} = \overline{B (C P A)}$
8		phnv	$⊢ U \in {CPreHil}_{OLD} \to U \in NrmCVec$
9		simpl	$⊢ (U \in NrmCVec \land (A \in X \land B \in ℂ \land C \in X)) \to U \in NrmCVec$
10	1 2	nvscl	$⊢ (U \in NrmCVec \land B \in ℂ \land C \in X) \to B S C \in X$
11	10	3adant3r1	$⊢ (U \in NrmCVec \land (A \in X \land B \in ℂ \land C \in X)) \to B S C \in X$
12		simpr1	$⊢ (U \in NrmCVec \land (A \in X \land B \in ℂ \land C \in X)) \to A \in X$
13	1 3	dipcj	$⊢ (U \in NrmCVec \land B S C \in X \land A \in X) \to \overline{(B S C) P A} = A P (B S C)$
14	9 11 12 13	syl3anc	$⊢ (U \in NrmCVec \land (A \in X \land B \in ℂ \land C \in X)) \to \overline{(B S C) P A} = A P (B S C)$
15	8 14	sylan	$⊢ (U \in {CPreHil}_{OLD} \land (A \in X \land B \in ℂ \land C \in X)) \to \overline{(B S C) P A} = A P (B S C)$
16		simpr2	$⊢ (U \in NrmCVec \land (A \in X \land B \in ℂ \land C \in X)) \to B \in ℂ$
17	1 3	dipcl	$⊢ (U \in NrmCVec \land C \in X \land A \in X) \to C P A \in ℂ$
18	17	3com23	$⊢ (U \in NrmCVec \land A \in X \land C \in X) \to C P A \in ℂ$
19	18	3adant3r2	$⊢ (U \in NrmCVec \land (A \in X \land B \in ℂ \land C \in X)) \to C P A \in ℂ$
20	16 19	cjmuld	$⊢ (U \in NrmCVec \land (A \in X \land B \in ℂ \land C \in X)) \to \overline{B (C P A)} = \overline{B} \overline{C P A}$
21	1 3	dipcj	$⊢ (U \in NrmCVec \land C \in X \land A \in X) \to \overline{C P A} = A P C$
22	21	3com23	$⊢ (U \in NrmCVec \land A \in X \land C \in X) \to \overline{C P A} = A P C$
23	22	3adant3r2	$⊢ (U \in NrmCVec \land (A \in X \land B \in ℂ \land C \in X)) \to \overline{C P A} = A P C$
24	23	oveq2d	$⊢ (U \in NrmCVec \land (A \in X \land B \in ℂ \land C \in X)) \to \overline{B} \overline{C P A} = \overline{B} (A P C)$
25	20 24	eqtrd	$⊢ (U \in NrmCVec \land (A \in X \land B \in ℂ \land C \in X)) \to \overline{B (C P A)} = \overline{B} (A P C)$
26	8 25	sylan	$⊢ (U \in {CPreHil}_{OLD} \land (A \in X \land B \in ℂ \land C \in X)) \to \overline{B (C P A)} = \overline{B} (A P C)$
27	7 15 26	3eqtr3d	$⊢ (U \in {CPreHil}_{OLD} \land (A \in X \land B \in ℂ \land C \in X)) \to A P (B S C) = \overline{B} (A P C)$

Metamath Proof Explorer

Theorem dipassr

Proof