ip0i

Description: A slight variant of Equation 6.46 of Ponnusamy p. 362, where J is either 1 or -1 to represent +-1. (Contributed by NM, 23-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}$
	ip1i.a	$⊢ A \in X$
	ip1i.b	$⊢ B \in X$
	ip1i.c	$⊢ C \in X$
	ip1i.6	$⊢ N = {norm}_{CV} (U)$
	ip0i.j	$⊢ J \in ℂ$
Assertion	ip0i	$⊢ ({N ((A G B) G (J S C))}^{2} - {N ((A G B) G (-J S C))}^{2}) + {N ((A G (-1 S B)) G (J S C))}^{2} - {N ((A G (-1 S B)) G (-J S C))}^{2} = 2 ({N (A G (J S C))}^{2} - {N (A G (-J S C))}^{2})$

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		ip1i.a	$⊢ A \in X$
7		ip1i.b	$⊢ B \in X$
8		ip1i.c	$⊢ C \in X$
9		ip1i.6	$⊢ N = {norm}_{CV} (U)$
10		ip0i.j	$⊢ J \in ℂ$
11		2cn	$⊢ 2 \in ℂ$
12	5	phnvi	$⊢ U \in NrmCVec$
13	1 3	nvscl	$⊢ (U \in NrmCVec \land J \in ℂ \land C \in X) \to J S C \in X$
14	12 10 8 13	mp3an	$⊢ J S C \in X$
15	1 2	nvgcl	$⊢ (U \in NrmCVec \land A \in X \land J S C \in X) \to A G (J S C) \in X$
16	12 6 14 15	mp3an	$⊢ A G (J S C) \in X$
17	1 9 12 16	nvcli	$⊢ N (A G (J S C)) \in ℝ$
18	17	recni	$⊢ N (A G (J S C)) \in ℂ$
19	18	sqcli	$⊢ {N (A G (J S C))}^{2} \in ℂ$
20	10	negcli	$⊢ - J \in ℂ$
21	1 3	nvscl	$⊢ (U \in NrmCVec \land - J \in ℂ \land C \in X) \to -J S C \in X$
22	12 20 8 21	mp3an	$⊢ -J S C \in X$
23	1 2	nvgcl	$⊢ (U \in NrmCVec \land A \in X \land -J S C \in X) \to A G (-J S C) \in X$
24	12 6 22 23	mp3an	$⊢ A G (-J S C) \in X$
25	1 9 12 24	nvcli	$⊢ N (A G (-J S C)) \in ℝ$
26	25	recni	$⊢ N (A G (-J S C)) \in ℂ$
27	26	sqcli	$⊢ {N (A G (-J S C))}^{2} \in ℂ$
28	11 19 27	subdii	$⊢ 2 ({N (A G (J S C))}^{2} - {N (A G (-J S C))}^{2}) = 2 {N (A G (J S C))}^{2} - 2 {N (A G (-J S C))}^{2}$
29	11 19	mulcli	$⊢ 2 {N (A G (J S C))}^{2} \in ℂ$
30	11 27	mulcli	$⊢ 2 {N (A G (-J S C))}^{2} \in ℂ$
31	1 9 12 7	nvcli	$⊢ N (B) \in ℝ$
32	31	recni	$⊢ N (B) \in ℂ$
33	32	sqcli	$⊢ {N (B)}^{2} \in ℂ$
34	11 33	mulcli	$⊢ 2 {N (B)}^{2} \in ℂ$
35		pnpcan2	$⊢ (2 {N (A G (J S C))}^{2} \in ℂ \land 2 {N (A G (-J S C))}^{2} \in ℂ \land 2 {N (B)}^{2} \in ℂ) \to 2 {N (A G (J S C))}^{2} + 2 {N (B)}^{2} - (2 {N (A G (-J S C))}^{2} + 2 {N (B)}^{2}) = 2 {N (A G (J S C))}^{2} - 2 {N (A G (-J S C))}^{2}$
36	29 30 34 35	mp3an	$⊢ 2 {N (A G (J S C))}^{2} + 2 {N (B)}^{2} - (2 {N (A G (-J S C))}^{2} + 2 {N (B)}^{2}) = 2 {N (A G (J S C))}^{2} - 2 {N (A G (-J S C))}^{2}$
37	28 36	eqtr4i	$⊢ 2 ({N (A G (J S C))}^{2} - {N (A G (-J S C))}^{2}) = 2 {N (A G (J S C))}^{2} + 2 {N (B)}^{2} - (2 {N (A G (-J S C))}^{2} + 2 {N (B)}^{2})$
38		eqid	$⊢ 1^{st} (U) = 1^{st} (U)$
39	38	nvvc	$⊢ U \in NrmCVec \to 1^{st} (U) \in {CVec}_{OLD}$
40	2	vafval	$⊢ G = 1^{st} (1^{st} (U))$
41	40	vcablo	$⊢ 1^{st} (U) \in {CVec}_{OLD} \to G \in AbelOp$
42	12 39 41	mp2b	$⊢ G \in AbelOp$
43	6 7 14	3pm3.2i	$⊢ (A \in X \land B \in X \land J S C \in X)$
44	1 2	bafval	$⊢ X = ran G$
45	44	ablo32	$⊢ (G \in AbelOp \land (A \in X \land B \in X \land J S C \in X)) \to (A G B) G (J S C) = (A G (J S C)) G B$
46	42 43 45	mp2an	$⊢ (A G B) G (J S C) = (A G (J S C)) G B$
47	46	fveq2i	$⊢ N ((A G B) G (J S C)) = N ((A G (J S C)) G B)$
48	47	oveq1i	$⊢ {N ((A G B) G (J S C))}^{2} = {N ((A G (J S C)) G B)}^{2}$
49		neg1cn	$⊢ - 1 \in ℂ$
50	1 3	nvscl	$⊢ (U \in NrmCVec \land - 1 \in ℂ \land B \in X) \to -1 S B \in X$
51	12 49 7 50	mp3an	$⊢ -1 S B \in X$
52	6 51 14	3pm3.2i	$⊢ (A \in X \land -1 S B \in X \land J S C \in X)$
53	44	ablo32	$⊢ (G \in AbelOp \land (A \in X \land -1 S B \in X \land J S C \in X)) \to (A G (-1 S B)) G (J S C) = (A G (J S C)) G (-1 S B)$
54	42 52 53	mp2an	$⊢ (A G (-1 S B)) G (J S C) = (A G (J S C)) G (-1 S B)$
55	54	fveq2i	$⊢ N ((A G (-1 S B)) G (J S C)) = N ((A G (J S C)) G (-1 S B))$
56	55	oveq1i	$⊢ {N ((A G (-1 S B)) G (J S C))}^{2} = {N ((A G (J S C)) G (-1 S B))}^{2}$
57	48 56	oveq12i	$⊢ {N ((A G B) G (J S C))}^{2} + {N ((A G (-1 S B)) G (J S C))}^{2} = {N ((A G (J S C)) G B)}^{2} + {N ((A G (J S C)) G (-1 S B))}^{2}$
58	1 2 3 9	phpar	$⊢ (U \in {CPreHil}_{OLD} \land A G (J S C) \in X \land B \in X) \to {N ((A G (J S C)) G B)}^{2} + {N ((A G (J S C)) G (-1 S B))}^{2} = 2 ({N (A G (J S C))}^{2} + {N (B)}^{2})$
59	5 16 7 58	mp3an	$⊢ {N ((A G (J S C)) G B)}^{2} + {N ((A G (J S C)) G (-1 S B))}^{2} = 2 ({N (A G (J S C))}^{2} + {N (B)}^{2})$
60	11 19 33	adddii	$⊢ 2 ({N (A G (J S C))}^{2} + {N (B)}^{2}) = 2 {N (A G (J S C))}^{2} + 2 {N (B)}^{2}$
61	57 59 60	3eqtri	$⊢ {N ((A G B) G (J S C))}^{2} + {N ((A G (-1 S B)) G (J S C))}^{2} = 2 {N (A G (J S C))}^{2} + 2 {N (B)}^{2}$
62	6 7 22	3pm3.2i	$⊢ (A \in X \land B \in X \land -J S C \in X)$
63	44	ablo32	$⊢ (G \in AbelOp \land (A \in X \land B \in X \land -J S C \in X)) \to (A G B) G (-J S C) = (A G (-J S C)) G B$
64	42 62 63	mp2an	$⊢ (A G B) G (-J S C) = (A G (-J S C)) G B$
65	64	fveq2i	$⊢ N ((A G B) G (-J S C)) = N ((A G (-J S C)) G B)$
66	65	oveq1i	$⊢ {N ((A G B) G (-J S C))}^{2} = {N ((A G (-J S C)) G B)}^{2}$
67	6 51 22	3pm3.2i	$⊢ (A \in X \land -1 S B \in X \land -J S C \in X)$
68	44	ablo32	$⊢ (G \in AbelOp \land (A \in X \land -1 S B \in X \land -J S C \in X)) \to (A G (-1 S B)) G (-J S C) = (A G (-J S C)) G (-1 S B)$
69	42 67 68	mp2an	$⊢ (A G (-1 S B)) G (-J S C) = (A G (-J S C)) G (-1 S B)$
70	69	fveq2i	$⊢ N ((A G (-1 S B)) G (-J S C)) = N ((A G (-J S C)) G (-1 S B))$
71	70	oveq1i	$⊢ {N ((A G (-1 S B)) G (-J S C))}^{2} = {N ((A G (-J S C)) G (-1 S B))}^{2}$
72	66 71	oveq12i	$⊢ {N ((A G B) G (-J S C))}^{2} + {N ((A G (-1 S B)) G (-J S C))}^{2} = {N ((A G (-J S C)) G B)}^{2} + {N ((A G (-J S C)) G (-1 S B))}^{2}$
73	1 2 3 9	phpar	$⊢ (U \in {CPreHil}_{OLD} \land A G (-J S C) \in X \land B \in X) \to {N ((A G (-J S C)) G B)}^{2} + {N ((A G (-J S C)) G (-1 S B))}^{2} = 2 ({N (A G (-J S C))}^{2} + {N (B)}^{2})$
74	5 24 7 73	mp3an	$⊢ {N ((A G (-J S C)) G B)}^{2} + {N ((A G (-J S C)) G (-1 S B))}^{2} = 2 ({N (A G (-J S C))}^{2} + {N (B)}^{2})$
75	11 27 33	adddii	$⊢ 2 ({N (A G (-J S C))}^{2} + {N (B)}^{2}) = 2 {N (A G (-J S C))}^{2} + 2 {N (B)}^{2}$
76	72 74 75	3eqtri	$⊢ {N ((A G B) G (-J S C))}^{2} + {N ((A G (-1 S B)) G (-J S C))}^{2} = 2 {N (A G (-J S C))}^{2} + 2 {N (B)}^{2}$
77	61 76	oveq12i	$⊢ {N ((A G B) G (J S C))}^{2} + {N ((A G (-1 S B)) G (J S C))}^{2} - ({N ((A G B) G (-J S C))}^{2} + {N ((A G (-1 S B)) G (-J S C))}^{2}) = 2 {N (A G (J S C))}^{2} + 2 {N (B)}^{2} - (2 {N (A G (-J S C))}^{2} + 2 {N (B)}^{2})$
78	1 2	nvgcl	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to A G B \in X$
79	12 6 7 78	mp3an	$⊢ A G B \in X$
80	1 2	nvgcl	$⊢ (U \in NrmCVec \land A G B \in X \land J S C \in X) \to (A G B) G (J S C) \in X$
81	12 79 14 80	mp3an	$⊢ (A G B) G (J S C) \in X$
82	1 9 12 81	nvcli	$⊢ N ((A G B) G (J S C)) \in ℝ$
83	82	recni	$⊢ N ((A G B) G (J S C)) \in ℂ$
84	83	sqcli	$⊢ {N ((A G B) G (J S C))}^{2} \in ℂ$
85	1 2	nvgcl	$⊢ (U \in NrmCVec \land A \in X \land -1 S B \in X) \to A G (-1 S B) \in X$
86	12 6 51 85	mp3an	$⊢ A G (-1 S B) \in X$
87	1 2	nvgcl	$⊢ (U \in NrmCVec \land A G (-1 S B) \in X \land J S C \in X) \to (A G (-1 S B)) G (J S C) \in X$
88	12 86 14 87	mp3an	$⊢ (A G (-1 S B)) G (J S C) \in X$
89	1 9 12 88	nvcli	$⊢ N ((A G (-1 S B)) G (J S C)) \in ℝ$
90	89	recni	$⊢ N ((A G (-1 S B)) G (J S C)) \in ℂ$
91	90	sqcli	$⊢ {N ((A G (-1 S B)) G (J S C))}^{2} \in ℂ$
92	1 2	nvgcl	$⊢ (U \in NrmCVec \land A G B \in X \land -J S C \in X) \to (A G B) G (-J S C) \in X$
93	12 79 22 92	mp3an	$⊢ (A G B) G (-J S C) \in X$
94	1 9 12 93	nvcli	$⊢ N ((A G B) G (-J S C)) \in ℝ$
95	94	recni	$⊢ N ((A G B) G (-J S C)) \in ℂ$
96	95	sqcli	$⊢ {N ((A G B) G (-J S C))}^{2} \in ℂ$
97	1 2	nvgcl	$⊢ (U \in NrmCVec \land A G (-1 S B) \in X \land -J S C \in X) \to (A G (-1 S B)) G (-J S C) \in X$
98	12 86 22 97	mp3an	$⊢ (A G (-1 S B)) G (-J S C) \in X$
99	1 9 12 98	nvcli	$⊢ N ((A G (-1 S B)) G (-J S C)) \in ℝ$
100	99	recni	$⊢ N ((A G (-1 S B)) G (-J S C)) \in ℂ$
101	100	sqcli	$⊢ {N ((A G (-1 S B)) G (-J S C))}^{2} \in ℂ$
102	84 91 96 101	addsub4i	$⊢ {N ((A G B) G (J S C))}^{2} + {N ((A G (-1 S B)) G (J S C))}^{2} - ({N ((A G B) G (-J S C))}^{2} + {N ((A G (-1 S B)) G (-J S C))}^{2}) = ({N ((A G B) G (J S C))}^{2} - {N ((A G B) G (-J S C))}^{2}) + {N ((A G (-1 S B)) G (J S C))}^{2} - {N ((A G (-1 S B)) G (-J S C))}^{2}$
103	37 77 102	3eqtr2ri	$⊢ ({N ((A G B) G (J S C))}^{2} - {N ((A G B) G (-J S C))}^{2}) + {N ((A G (-1 S B)) G (J S C))}^{2} - {N ((A G (-1 S B)) G (-J S C))}^{2} = 2 ({N (A G (J S C))}^{2} - {N (A G (-J S C))}^{2})$

Metamath Proof Explorer

Theorem ip0i

Proof