ipdirilem

Description: Lemma for ipdiri . (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}$
	ipdiri.8	$⊢ A \in X$
	ipdiri.9	$⊢ B \in X$
	ipdiri.10	$⊢ C \in X$
Assertion	ipdirilem	$⊢ (A G B) P C = (A P C) + (B P C)$

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		ipdiri.8	$⊢ A \in X$
7		ipdiri.9	$⊢ B \in X$
8		ipdiri.10	$⊢ C \in X$
9		2cn	$⊢ 2 \in ℂ$
10		2ne0	$⊢ 2 \neq 0$
11	9 10	recidi	$⊢ 2 (\frac{1}{2}) = 1$
12	11	oveq1i	$⊢ 2 (\frac{1}{2}) S (A G B) = 1 S (A G B)$
13	5	phnvi	$⊢ U \in NrmCVec$
14		halfcn	$⊢ \frac{1}{2} \in ℂ$
15	1 2	nvgcl	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to A G B \in X$
16	13 6 7 15	mp3an	$⊢ A G B \in X$
17	9 14 16	3pm3.2i	$⊢ (2 \in ℂ \land \frac{1}{2} \in ℂ \land A G B \in X)$
18	1 3	nvsass	$⊢ (U \in NrmCVec \land (2 \in ℂ \land \frac{1}{2} \in ℂ \land A G B \in X)) \to 2 (\frac{1}{2}) S (A G B) = 2 S ((\frac{1}{2}) S (A G B))$
19	13 17 18	mp2an	$⊢ 2 (\frac{1}{2}) S (A G B) = 2 S ((\frac{1}{2}) S (A G B))$
20	1 3	nvsid	$⊢ (U \in NrmCVec \land A G B \in X) \to 1 S (A G B) = A G B$
21	13 16 20	mp2an	$⊢ 1 S (A G B) = A G B$
22	12 19 21	3eqtr3i	$⊢ 2 S ((\frac{1}{2}) S (A G B)) = A G B$
23	22	oveq1i	$⊢ (2 S ((\frac{1}{2}) S (A G B))) P C = (A G B) P C$
24	1 3	nvscl	$⊢ (U \in NrmCVec \land \frac{1}{2} \in ℂ \land A G B \in X) \to (\frac{1}{2}) S (A G B) \in X$
25	13 14 16 24	mp3an	$⊢ (\frac{1}{2}) S (A G B) \in X$
26	1 2 3 4 5 25 8	ip2i	$⊢ (2 S ((\frac{1}{2}) S (A G B))) P C = 2 (((\frac{1}{2}) S (A G B)) P C)$
27	23 26	eqtr3i	$⊢ (A G B) P C = 2 (((\frac{1}{2}) S (A G B)) P C)$
28		neg1cn	$⊢ - 1 \in ℂ$
29	1 3	nvscl	$⊢ (U \in NrmCVec \land - 1 \in ℂ \land B \in X) \to -1 S B \in X$
30	13 28 7 29	mp3an	$⊢ -1 S B \in X$
31	1 2	nvgcl	$⊢ (U \in NrmCVec \land A \in X \land -1 S B \in X) \to A G (-1 S B) \in X$
32	13 6 30 31	mp3an	$⊢ A G (-1 S B) \in X$
33	1 3	nvscl	$⊢ (U \in NrmCVec \land \frac{1}{2} \in ℂ \land A G (-1 S B) \in X) \to (\frac{1}{2}) S (A G (-1 S B)) \in X$
34	13 14 32 33	mp3an	$⊢ (\frac{1}{2}) S (A G (-1 S B)) \in X$
35	1 2 3 4 5 25 34 8	ip1i	$⊢ ((((\frac{1}{2}) S (A G B)) G ((\frac{1}{2}) S (A G (-1 S B)))) P C) + ((((\frac{1}{2}) S (A G B)) G (-1 S ((\frac{1}{2}) S (A G (-1 S B))))) P C) = 2 (((\frac{1}{2}) S (A G B)) P C)$
36		eqid	$⊢ 1^{st} (U) = 1^{st} (U)$
37	36	nvvc	$⊢ U \in NrmCVec \to 1^{st} (U) \in {CVec}_{OLD}$
38	13 37	ax-mp	$⊢ 1^{st} (U) \in {CVec}_{OLD}$
39	2	vafval	$⊢ G = 1^{st} (1^{st} (U))$
40	39	vcablo	$⊢ 1^{st} (U) \in {CVec}_{OLD} \to G \in AbelOp$
41	38 40	ax-mp	$⊢ G \in AbelOp$
42	6 7	pm3.2i	$⊢ (A \in X \land B \in X)$
43	6 30	pm3.2i	$⊢ (A \in X \land -1 S B \in X)$
44	1 2	bafval	$⊢ X = ran G$
45	44	ablo4	$⊢ (G \in AbelOp \land (A \in X \land B \in X) \land (A \in X \land -1 S B \in X)) \to (A G B) G (A G (-1 S B)) = (A G A) G (B G (-1 S B))$
46	41 42 43 45	mp3an	$⊢ (A G B) G (A G (-1 S B)) = (A G A) G (B G (-1 S B))$
47	3	smfval	$⊢ S = 2^{nd} (1^{st} (U))$
48	39 47 44	vc2OLD	$⊢ (1^{st} (U) \in {CVec}_{OLD} \land A \in X) \to A G A = 2 S A$
49	38 6 48	mp2an	$⊢ A G A = 2 S A$
50		eqid	$⊢ 0_{vec} (U) = 0_{vec} (U)$
51	1 2 3 50	nvrinv	$⊢ (U \in NrmCVec \land B \in X) \to B G (-1 S B) = 0_{vec} (U)$
52	13 7 51	mp2an	$⊢ B G (-1 S B) = 0_{vec} (U)$
53	49 52	oveq12i	$⊢ (A G A) G (B G (-1 S B)) = (2 S A) G 0_{vec} (U)$
54	1 3	nvscl	$⊢ (U \in NrmCVec \land 2 \in ℂ \land A \in X) \to 2 S A \in X$
55	13 9 6 54	mp3an	$⊢ 2 S A \in X$
56	1 2 50	nv0rid	$⊢ (U \in NrmCVec \land 2 S A \in X) \to (2 S A) G 0_{vec} (U) = 2 S A$
57	13 55 56	mp2an	$⊢ (2 S A) G 0_{vec} (U) = 2 S A$
58	46 53 57	3eqtri	$⊢ (A G B) G (A G (-1 S B)) = 2 S A$
59	58	oveq2i	$⊢ (\frac{1}{2}) S ((A G B) G (A G (-1 S B))) = (\frac{1}{2}) S (2 S A)$
60	14 9 6	3pm3.2i	$⊢ (\frac{1}{2} \in ℂ \land 2 \in ℂ \land A \in X)$
61	1 3	nvsass	$⊢ (U \in NrmCVec \land (\frac{1}{2} \in ℂ \land 2 \in ℂ \land A \in X)) \to (\frac{1}{2}) \cdot 2 S A = (\frac{1}{2}) S (2 S A)$
62	13 60 61	mp2an	$⊢ (\frac{1}{2}) \cdot 2 S A = (\frac{1}{2}) S (2 S A)$
63	59 62	eqtr4i	$⊢ (\frac{1}{2}) S ((A G B) G (A G (-1 S B))) = (\frac{1}{2}) \cdot 2 S A$
64	14 16 32	3pm3.2i	$⊢ (\frac{1}{2} \in ℂ \land A G B \in X \land A G (-1 S B) \in X)$
65	1 2 3	nvdi	$⊢ (U \in NrmCVec \land (\frac{1}{2} \in ℂ \land A G B \in X \land A G (-1 S B) \in X)) \to (\frac{1}{2}) S ((A G B) G (A G (-1 S B))) = ((\frac{1}{2}) S (A G B)) G ((\frac{1}{2}) S (A G (-1 S B)))$
66	13 64 65	mp2an	$⊢ (\frac{1}{2}) S ((A G B) G (A G (-1 S B))) = ((\frac{1}{2}) S (A G B)) G ((\frac{1}{2}) S (A G (-1 S B)))$
67		ax-1cn	$⊢ 1 \in ℂ$
68	67 9 10	divcan1i	$⊢ (\frac{1}{2}) \cdot 2 = 1$
69	68	oveq1i	$⊢ (\frac{1}{2}) \cdot 2 S A = 1 S A$
70	1 3	nvsid	$⊢ (U \in NrmCVec \land A \in X) \to 1 S A = A$
71	13 6 70	mp2an	$⊢ 1 S A = A$
72	69 71	eqtri	$⊢ (\frac{1}{2}) \cdot 2 S A = A$
73	63 66 72	3eqtr3i	$⊢ ((\frac{1}{2}) S (A G B)) G ((\frac{1}{2}) S (A G (-1 S B))) = A$
74	73	oveq1i	$⊢ (((\frac{1}{2}) S (A G B)) G ((\frac{1}{2}) S (A G (-1 S B)))) P C = A P C$
75	28 14	mulcomi	$⊢ -1 (\frac{1}{2}) = (\frac{1}{2}) -1$
76	75	oveq1i	$⊢ -1 (\frac{1}{2}) S (A G (-1 S B)) = (\frac{1}{2}) -1 S (A G (-1 S B))$
77	28 14 32	3pm3.2i	$⊢ (- 1 \in ℂ \land \frac{1}{2} \in ℂ \land A G (-1 S B) \in X)$
78	1 3	nvsass	$⊢ (U \in NrmCVec \land (- 1 \in ℂ \land \frac{1}{2} \in ℂ \land A G (-1 S B) \in X)) \to -1 (\frac{1}{2}) S (A G (-1 S B)) = -1 S ((\frac{1}{2}) S (A G (-1 S B)))$
79	13 77 78	mp2an	$⊢ -1 (\frac{1}{2}) S (A G (-1 S B)) = -1 S ((\frac{1}{2}) S (A G (-1 S B)))$
80	14 28 32	3pm3.2i	$⊢ (\frac{1}{2} \in ℂ \land - 1 \in ℂ \land A G (-1 S B) \in X)$
81	1 3	nvsass	$⊢ (U \in NrmCVec \land (\frac{1}{2} \in ℂ \land - 1 \in ℂ \land A G (-1 S B) \in X)) \to (\frac{1}{2}) -1 S (A G (-1 S B)) = (\frac{1}{2}) S (-1 S (A G (-1 S B)))$
82	13 80 81	mp2an	$⊢ (\frac{1}{2}) -1 S (A G (-1 S B)) = (\frac{1}{2}) S (-1 S (A G (-1 S B)))$
83	28 6 30	3pm3.2i	$⊢ (- 1 \in ℂ \land A \in X \land -1 S B \in X)$
84	1 2 3	nvdi	$⊢ (U \in NrmCVec \land (- 1 \in ℂ \land A \in X \land -1 S B \in X)) \to -1 S (A G (-1 S B)) = (-1 S A) G (-1 S (-1 S B))$
85	13 83 84	mp2an	$⊢ -1 S (A G (-1 S B)) = (-1 S A) G (-1 S (-1 S B))$
86		neg1mulneg1e1	$⊢ -1 -1 = 1$
87	86	oveq1i	$⊢ -1 -1 S B = 1 S B$
88	28 28 7	3pm3.2i	$⊢ (- 1 \in ℂ \land - 1 \in ℂ \land B \in X)$
89	1 3	nvsass	$⊢ (U \in NrmCVec \land (- 1 \in ℂ \land - 1 \in ℂ \land B \in X)) \to -1 -1 S B = -1 S (-1 S B)$
90	13 88 89	mp2an	$⊢ -1 -1 S B = -1 S (-1 S B)$
91	1 3	nvsid	$⊢ (U \in NrmCVec \land B \in X) \to 1 S B = B$
92	13 7 91	mp2an	$⊢ 1 S B = B$
93	87 90 92	3eqtr3i	$⊢ -1 S (-1 S B) = B$
94	93	oveq2i	$⊢ (-1 S A) G (-1 S (-1 S B)) = (-1 S A) G B$
95	85 94	eqtri	$⊢ -1 S (A G (-1 S B)) = (-1 S A) G B$
96	95	oveq2i	$⊢ (\frac{1}{2}) S (-1 S (A G (-1 S B))) = (\frac{1}{2}) S ((-1 S A) G B)$
97	82 96	eqtri	$⊢ (\frac{1}{2}) -1 S (A G (-1 S B)) = (\frac{1}{2}) S ((-1 S A) G B)$
98	76 79 97	3eqtr3i	$⊢ -1 S ((\frac{1}{2}) S (A G (-1 S B))) = (\frac{1}{2}) S ((-1 S A) G B)$
99	98	oveq2i	$⊢ ((\frac{1}{2}) S (A G B)) G (-1 S ((\frac{1}{2}) S (A G (-1 S B)))) = ((\frac{1}{2}) S (A G B)) G ((\frac{1}{2}) S ((-1 S A) G B))$
100	1 3	nvscl	$⊢ (U \in NrmCVec \land - 1 \in ℂ \land A \in X) \to -1 S A \in X$
101	13 28 6 100	mp3an	$⊢ -1 S A \in X$
102	1 2	nvgcl	$⊢ (U \in NrmCVec \land -1 S A \in X \land B \in X) \to (-1 S A) G B \in X$
103	13 101 7 102	mp3an	$⊢ (-1 S A) G B \in X$
104	14 16 103	3pm3.2i	$⊢ (\frac{1}{2} \in ℂ \land A G B \in X \land (-1 S A) G B \in X)$
105	1 2 3	nvdi	$⊢ (U \in NrmCVec \land (\frac{1}{2} \in ℂ \land A G B \in X \land (-1 S A) G B \in X)) \to (\frac{1}{2}) S ((A G B) G ((-1 S A) G B)) = ((\frac{1}{2}) S (A G B)) G ((\frac{1}{2}) S ((-1 S A) G B))$
106	13 104 105	mp2an	$⊢ (\frac{1}{2}) S ((A G B) G ((-1 S A) G B)) = ((\frac{1}{2}) S (A G B)) G ((\frac{1}{2}) S ((-1 S A) G B))$
107	99 106	eqtr4i	$⊢ ((\frac{1}{2}) S (A G B)) G (-1 S ((\frac{1}{2}) S (A G (-1 S B)))) = (\frac{1}{2}) S ((A G B) G ((-1 S A) G B))$
108	101 7	pm3.2i	$⊢ (-1 S A \in X \land B \in X)$
109	44	ablo4	$⊢ (G \in AbelOp \land (A \in X \land B \in X) \land (-1 S A \in X \land B \in X)) \to (A G B) G ((-1 S A) G B) = (A G (-1 S A)) G (B G B)$
110	41 42 108 109	mp3an	$⊢ (A G B) G ((-1 S A) G B) = (A G (-1 S A)) G (B G B)$
111	1 2 3 50	nvrinv	$⊢ (U \in NrmCVec \land A \in X) \to A G (-1 S A) = 0_{vec} (U)$
112	13 6 111	mp2an	$⊢ A G (-1 S A) = 0_{vec} (U)$
113	112	oveq1i	$⊢ (A G (-1 S A)) G (B G B) = 0_{vec} (U) G (B G B)$
114	1 2	nvgcl	$⊢ (U \in NrmCVec \land B \in X \land B \in X) \to B G B \in X$
115	13 7 7 114	mp3an	$⊢ B G B \in X$
116	1 2 50	nv0lid	$⊢ (U \in NrmCVec \land B G B \in X) \to 0_{vec} (U) G (B G B) = B G B$
117	13 115 116	mp2an	$⊢ 0_{vec} (U) G (B G B) = B G B$
118	113 117	eqtri	$⊢ (A G (-1 S A)) G (B G B) = B G B$
119	39 47 44	vc2OLD	$⊢ (1^{st} (U) \in {CVec}_{OLD} \land B \in X) \to B G B = 2 S B$
120	38 7 119	mp2an	$⊢ B G B = 2 S B$
121	110 118 120	3eqtri	$⊢ (A G B) G ((-1 S A) G B) = 2 S B$
122	121	oveq2i	$⊢ (\frac{1}{2}) S ((A G B) G ((-1 S A) G B)) = (\frac{1}{2}) S (2 S B)$
123	14 9 7	3pm3.2i	$⊢ (\frac{1}{2} \in ℂ \land 2 \in ℂ \land B \in X)$
124	1 3	nvsass	$⊢ (U \in NrmCVec \land (\frac{1}{2} \in ℂ \land 2 \in ℂ \land B \in X)) \to (\frac{1}{2}) \cdot 2 S B = (\frac{1}{2}) S (2 S B)$
125	13 123 124	mp2an	$⊢ (\frac{1}{2}) \cdot 2 S B = (\frac{1}{2}) S (2 S B)$
126	68	oveq1i	$⊢ (\frac{1}{2}) \cdot 2 S B = 1 S B$
127	122 125 126	3eqtr2i	$⊢ (\frac{1}{2}) S ((A G B) G ((-1 S A) G B)) = 1 S B$
128	107 127 92	3eqtri	$⊢ ((\frac{1}{2}) S (A G B)) G (-1 S ((\frac{1}{2}) S (A G (-1 S B)))) = B$
129	128	oveq1i	$⊢ (((\frac{1}{2}) S (A G B)) G (-1 S ((\frac{1}{2}) S (A G (-1 S B))))) P C = B P C$
130	74 129	oveq12i	$⊢ ((((\frac{1}{2}) S (A G B)) G ((\frac{1}{2}) S (A G (-1 S B)))) P C) + ((((\frac{1}{2}) S (A G B)) G (-1 S ((\frac{1}{2}) S (A G (-1 S B))))) P C) = (A P C) + (B P C)$
131	27 35 130	3eqtr2i	$⊢ (A G B) P C = (A P C) + (B P C)$

Metamath Proof Explorer

Theorem ipdirilem

Proof