ipasslem5

Description: Lemma for ipassi . Show the inner product associative law for rational numbers. (Contributed by NM, 27-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}$
	ipasslem1.b	$⊢ B \in X$
Assertion	ipasslem5	$⊢ (C \in ℚ \land A \in X) \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		ipasslem1.b	$⊢ B \in X$
7		elq	$⊢ C \in ℚ \leftrightarrow \exists j \in ℤ \exists k \in ℕ C = \frac{j}{k}$
8		zcn	$⊢ j \in ℤ \to j \in ℂ$
9		nnrecre	$⊢ k \in ℕ \to \frac{1}{k} \in ℝ$
10	9	recnd	$⊢ k \in ℕ \to \frac{1}{k} \in ℂ$
11	5	phnvi	$⊢ U \in NrmCVec$
12	1 4	dipcl	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to A P B \in ℂ$
13	11 6 12	mp3an13	$⊢ A \in X \to A P B \in ℂ$
14		mulass	$⊢ (j \in ℂ \land \frac{1}{k} \in ℂ \land A P B \in ℂ) \to j (\frac{1}{k}) (A P B) = j (\frac{1}{k}) (A P B)$
15	8 10 13 14	syl3an	$⊢ (j \in ℤ \land k \in ℕ \land A \in X) \to j (\frac{1}{k}) (A P B) = j (\frac{1}{k}) (A P B)$
16	8	adantr	$⊢ (j \in ℤ \land k \in ℕ) \to j \in ℂ$
17		nncn	$⊢ k \in ℕ \to k \in ℂ$
18	17	adantl	$⊢ (j \in ℤ \land k \in ℕ) \to k \in ℂ$
19		nnne0	$⊢ k \in ℕ \to k \neq 0$
20	19	adantl	$⊢ (j \in ℤ \land k \in ℕ) \to k \neq 0$
21	16 18 20	divrecd	$⊢ (j \in ℤ \land k \in ℕ) \to \frac{j}{k} = j (\frac{1}{k})$
22	21	3adant3	$⊢ (j \in ℤ \land k \in ℕ \land A \in X) \to \frac{j}{k} = j (\frac{1}{k})$
23	22	oveq1d	$⊢ (j \in ℤ \land k \in ℕ \land A \in X) \to (\frac{j}{k}) (A P B) = j (\frac{1}{k}) (A P B)$
24	22	oveq1d	$⊢ (j \in ℤ \land k \in ℕ \land A \in X) \to (\frac{j}{k}) S A = j (\frac{1}{k}) S A$
25		id	$⊢ A \in X \to A \in X$
26	1 3	nvsass	$⊢ (U \in NrmCVec \land (j \in ℂ \land \frac{1}{k} \in ℂ \land A \in X)) \to j (\frac{1}{k}) S A = j S ((\frac{1}{k}) S A)$
27	11 26	mpan	$⊢ (j \in ℂ \land \frac{1}{k} \in ℂ \land A \in X) \to j (\frac{1}{k}) S A = j S ((\frac{1}{k}) S A)$
28	8 10 25 27	syl3an	$⊢ (j \in ℤ \land k \in ℕ \land A \in X) \to j (\frac{1}{k}) S A = j S ((\frac{1}{k}) S A)$
29	24 28	eqtrd	$⊢ (j \in ℤ \land k \in ℕ \land A \in X) \to (\frac{j}{k}) S A = j S ((\frac{1}{k}) S A)$
30	29	oveq1d	$⊢ (j \in ℤ \land k \in ℕ \land A \in X) \to ((\frac{j}{k}) S A) P B = (j S ((\frac{1}{k}) S A)) P B$
31	1 3	nvscl	$⊢ (U \in NrmCVec \land \frac{1}{k} \in ℂ \land A \in X) \to (\frac{1}{k}) S A \in X$
32	11 31	mp3an1	$⊢ (\frac{1}{k} \in ℂ \land A \in X) \to (\frac{1}{k}) S A \in X$
33	10 32	sylan	$⊢ (k \in ℕ \land A \in X) \to (\frac{1}{k}) S A \in X$
34	1 2 3 4 5 6	ipasslem3	$⊢ (j \in ℤ \land (\frac{1}{k}) S A \in X) \to (j S ((\frac{1}{k}) S A)) P B = j (((\frac{1}{k}) S A) P B)$
35	33 34	sylan2	$⊢ (j \in ℤ \land (k \in ℕ \land A \in X)) \to (j S ((\frac{1}{k}) S A)) P B = j (((\frac{1}{k}) S A) P B)$
36	35	3impb	$⊢ (j \in ℤ \land k \in ℕ \land A \in X) \to (j S ((\frac{1}{k}) S A)) P B = j (((\frac{1}{k}) S A) P B)$
37	1 2 3 4 5 6	ipasslem4	$⊢ (k \in ℕ \land A \in X) \to ((\frac{1}{k}) S A) P B = (\frac{1}{k}) (A P B)$
38	37	3adant1	$⊢ (j \in ℤ \land k \in ℕ \land A \in X) \to ((\frac{1}{k}) S A) P B = (\frac{1}{k}) (A P B)$
39	38	oveq2d	$⊢ (j \in ℤ \land k \in ℕ \land A \in X) \to j (((\frac{1}{k}) S A) P B) = j (\frac{1}{k}) (A P B)$
40	30 36 39	3eqtrd	$⊢ (j \in ℤ \land k \in ℕ \land A \in X) \to ((\frac{j}{k}) S A) P B = j (\frac{1}{k}) (A P B)$
41	15 23 40	3eqtr4rd	$⊢ (j \in ℤ \land k \in ℕ \land A \in X) \to ((\frac{j}{k}) S A) P B = (\frac{j}{k}) (A P B)$
42		oveq1	$⊢ C = \frac{j}{k} \to C S A = (\frac{j}{k}) S A$
43	42	oveq1d	$⊢ C = \frac{j}{k} \to (C S A) P B = ((\frac{j}{k}) S A) P B$
44		oveq1	$⊢ C = \frac{j}{k} \to C (A P B) = (\frac{j}{k}) (A P B)$
45	43 44	eqeq12d	$⊢ C = \frac{j}{k} \to ((C S A) P B = C (A P B) \leftrightarrow ((\frac{j}{k}) S A) P B = (\frac{j}{k}) (A P B))$
46	41 45	syl5ibrcom	$⊢ (j \in ℤ \land k \in ℕ \land A \in X) \to (C = \frac{j}{k} \to (C S A) P B = C (A P B))$
47	46	3expia	$⊢ (j \in ℤ \land k \in ℕ) \to (A \in X \to (C = \frac{j}{k} \to (C S A) P B = C (A P B)))$
48	47	com23	$⊢ (j \in ℤ \land k \in ℕ) \to (C = \frac{j}{k} \to (A \in X \to (C S A) P B = C (A P B)))$
49	48	rexlimivv	$⊢ \exists j \in ℤ \exists k \in ℕ C = \frac{j}{k} \to (A \in X \to (C S A) P B = C (A P B))$
50	7 49	sylbi	$⊢ C \in ℚ \to (A \in X \to (C S A) P B = C (A P B))$
51	50	imp	$⊢ (C \in ℚ \land A \in X) \to (C S A) P B = C (A P B)$

Metamath Proof Explorer

Theorem ipasslem5

Proof