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	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
	ip1i.2	⊢ 𝐺 = ( +_𝑣 ‘ 𝑈 )
	ip1i.4	⊢ 𝑆 = ( ·_𝑠OLD ‘ 𝑈 )
	ip1i.7	⊢ 𝑃 = ( ·_𝑖OLD ‘ 𝑈 )
	ip1i.9	⊢ 𝑈 ∈ CPreHil_OLD
	ip1i.a	⊢ 𝐴 ∈ 𝑋
	ip1i.b	⊢ 𝐵 ∈ 𝑋
	ip1i.c	⊢ 𝐶 ∈ 𝑋
	ip1i.6	⊢ 𝑁 = ( norm_CV ‘ 𝑈 )
	ip0i.j	⊢ 𝐽 ∈ ℂ
Assertion	ip0i	⊢ ( ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) + ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) = ( 2 · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) )

Proof

Step	Hyp	Ref	Expression
1		ip1i.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		ip1i.2	⊢ 𝐺 = ( +_𝑣 ‘ 𝑈 )
3		ip1i.4	⊢ 𝑆 = ( ·_𝑠OLD ‘ 𝑈 )
4		ip1i.7	⊢ 𝑃 = ( ·_𝑖OLD ‘ 𝑈 )
5		ip1i.9	⊢ 𝑈 ∈ CPreHil_OLD
6		ip1i.a	⊢ 𝐴 ∈ 𝑋
7		ip1i.b	⊢ 𝐵 ∈ 𝑋
8		ip1i.c	⊢ 𝐶 ∈ 𝑋
9		ip1i.6	⊢ 𝑁 = ( norm_CV ‘ 𝑈 )
10		ip0i.j	⊢ 𝐽 ∈ ℂ
11		2cn	⊢ 2 ∈ ℂ
12	5	phnvi	⊢ 𝑈 ∈ NrmCVec
13	1 3	nvscl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐽 ∈ ℂ ∧ 𝐶 ∈ 𝑋 ) → ( 𝐽 𝑆 𝐶 ) ∈ 𝑋 )
14	12 10 8 13	mp3an	⊢ ( 𝐽 𝑆 𝐶 ) ∈ 𝑋
15	1 2	nvgcl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ ( 𝐽 𝑆 𝐶 ) ∈ 𝑋 ) → ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) ∈ 𝑋 )
16	12 6 14 15	mp3an	⊢ ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) ∈ 𝑋
17	1 9 12 16	nvcli	⊢ ( 𝑁 ‘ ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ∈ ℝ
18	17	recni	⊢ ( 𝑁 ‘ ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ∈ ℂ
19	18	sqcli	⊢ ( ( 𝑁 ‘ ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ∈ ℂ
20	10	negcli	⊢ - 𝐽 ∈ ℂ
21	1 3	nvscl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ - 𝐽 ∈ ℂ ∧ 𝐶 ∈ 𝑋 ) → ( - 𝐽 𝑆 𝐶 ) ∈ 𝑋 )
22	12 20 8 21	mp3an	⊢ ( - 𝐽 𝑆 𝐶 ) ∈ 𝑋
23	1 2	nvgcl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ ( - 𝐽 𝑆 𝐶 ) ∈ 𝑋 ) → ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ∈ 𝑋 )
24	12 6 22 23	mp3an	⊢ ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ∈ 𝑋
25	1 9 12 24	nvcli	⊢ ( 𝑁 ‘ ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ∈ ℝ
26	25	recni	⊢ ( 𝑁 ‘ ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ∈ ℂ
27	26	sqcli	⊢ ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ∈ ℂ
28	11 19 27	subdii	⊢ ( 2 · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) = ( ( 2 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) − ( 2 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) )
29	11 19	mulcli	⊢ ( 2 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) ∈ ℂ
30	11 27	mulcli	⊢ ( 2 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) ∈ ℂ
31	1 9 12 7	nvcli	⊢ ( 𝑁 ‘ 𝐵 ) ∈ ℝ
32	31	recni	⊢ ( 𝑁 ‘ 𝐵 ) ∈ ℂ
33	32	sqcli	⊢ ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ∈ ℂ
34	11 33	mulcli	⊢ ( 2 · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ∈ ℂ
35		pnpcan2	⊢ ( ( ( 2 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) ∈ ℂ ∧ ( 2 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) ∈ ℂ ∧ ( 2 · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ∈ ℂ ) → ( ( ( 2 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) + ( 2 · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) − ( ( 2 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) + ( 2 · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) ) = ( ( 2 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) − ( 2 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) )
36	29 30 34 35	mp3an	⊢ ( ( ( 2 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) + ( 2 · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) − ( ( 2 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) + ( 2 · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) ) = ( ( 2 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) − ( 2 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) )
37	28 36	eqtr4i	⊢ ( 2 · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) = ( ( ( 2 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) + ( 2 · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) − ( ( 2 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) + ( 2 · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) )
38		eqid	⊢ ( 1^st ‘ 𝑈 ) = ( 1^st ‘ 𝑈 )
39	38	nvvc	⊢ ( 𝑈 ∈ NrmCVec → ( 1^st ‘ 𝑈 ) ∈ CVec_OLD )
40	2	vafval	⊢ 𝐺 = ( 1^st ‘ ( 1^st ‘ 𝑈 ) )
41	40	vcablo	⊢ ( ( 1^st ‘ 𝑈 ) ∈ CVec_OLD → 𝐺 ∈ AbelOp )
42	12 39 41	mp2b	⊢ 𝐺 ∈ AbelOp
43	6 7 14	3pm3.2i	⊢ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( 𝐽 𝑆 𝐶 ) ∈ 𝑋 )
44	1 2	bafval	⊢ 𝑋 = ran 𝐺
45	44	ablo32	⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( 𝐽 𝑆 𝐶 ) ∈ 𝑋 ) ) → ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) = ( ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) 𝐺 𝐵 ) )
46	42 43 45	mp2an	⊢ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) = ( ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) 𝐺 𝐵 )
47	46	fveq2i	⊢ ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) = ( 𝑁 ‘ ( ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) 𝐺 𝐵 ) )
48	47	oveq1i	⊢ ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) = ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) 𝐺 𝐵 ) ) ↑ 2 )
49		neg1cn	⊢ - 1 ∈ ℂ
50	1 3	nvscl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ - 1 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ) → ( - 1 𝑆 𝐵 ) ∈ 𝑋 )
51	12 49 7 50	mp3an	⊢ ( - 1 𝑆 𝐵 ) ∈ 𝑋
52	6 51 14	3pm3.2i	⊢ ( 𝐴 ∈ 𝑋 ∧ ( - 1 𝑆 𝐵 ) ∈ 𝑋 ∧ ( 𝐽 𝑆 𝐶 ) ∈ 𝑋 )
53	44	ablo32	⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴 ∈ 𝑋 ∧ ( - 1 𝑆 𝐵 ) ∈ 𝑋 ∧ ( 𝐽 𝑆 𝐶 ) ∈ 𝑋 ) ) → ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) = ( ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) 𝐺 ( - 1 𝑆 𝐵 ) ) )
54	42 52 53	mp2an	⊢ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) = ( ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) 𝐺 ( - 1 𝑆 𝐵 ) )
55	54	fveq2i	⊢ ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) = ( 𝑁 ‘ ( ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) 𝐺 ( - 1 𝑆 𝐵 ) ) )
56	55	oveq1i	⊢ ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) = ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 )
57	48 56	oveq12i	⊢ ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) = ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) 𝐺 𝐵 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) )
58	1 2 3 9	phpar	⊢ ( ( 𝑈 ∈ CPreHil_OLD ∧ ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) 𝐺 𝐵 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) + ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) )
59	5 16 7 58	mp3an	⊢ ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) 𝐺 𝐵 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) + ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) )
60	11 19 33	adddii	⊢ ( 2 · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) + ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) = ( ( 2 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) + ( 2 · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) )
61	57 59 60	3eqtri	⊢ ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) = ( ( 2 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) + ( 2 · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) )
62	6 7 22	3pm3.2i	⊢ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( - 𝐽 𝑆 𝐶 ) ∈ 𝑋 )
63	44	ablo32	⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ ( - 𝐽 𝑆 𝐶 ) ∈ 𝑋 ) ) → ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) = ( ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) 𝐺 𝐵 ) )
64	42 62 63	mp2an	⊢ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) = ( ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) 𝐺 𝐵 )
65	64	fveq2i	⊢ ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) = ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) 𝐺 𝐵 ) )
66	65	oveq1i	⊢ ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) = ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) 𝐺 𝐵 ) ) ↑ 2 )
67	6 51 22	3pm3.2i	⊢ ( 𝐴 ∈ 𝑋 ∧ ( - 1 𝑆 𝐵 ) ∈ 𝑋 ∧ ( - 𝐽 𝑆 𝐶 ) ∈ 𝑋 )
68	44	ablo32	⊢ ( ( 𝐺 ∈ AbelOp ∧ ( 𝐴 ∈ 𝑋 ∧ ( - 1 𝑆 𝐵 ) ∈ 𝑋 ∧ ( - 𝐽 𝑆 𝐶 ) ∈ 𝑋 ) ) → ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) = ( ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) 𝐺 ( - 1 𝑆 𝐵 ) ) )
69	42 67 68	mp2an	⊢ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) = ( ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) 𝐺 ( - 1 𝑆 𝐵 ) )
70	69	fveq2i	⊢ ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) = ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) 𝐺 ( - 1 𝑆 𝐵 ) ) )
71	70	oveq1i	⊢ ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) = ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 )
72	66 71	oveq12i	⊢ ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) = ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) 𝐺 𝐵 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) )
73	1 2 3 9	phpar	⊢ ( ( 𝑈 ∈ CPreHil_OLD ∧ ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) 𝐺 𝐵 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) + ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) )
74	5 24 7 73	mp3an	⊢ ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) 𝐺 𝐵 ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) 𝐺 ( - 1 𝑆 𝐵 ) ) ) ↑ 2 ) ) = ( 2 · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) + ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) )
75	11 27 33	adddii	⊢ ( 2 · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) + ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) = ( ( 2 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) + ( 2 · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) )
76	72 74 75	3eqtri	⊢ ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) = ( ( 2 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) + ( 2 · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) )
77	61 76	oveq12i	⊢ ( ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) − ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) = ( ( ( 2 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) + ( 2 · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) − ( ( 2 · ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) + ( 2 · ( ( 𝑁 ‘ 𝐵 ) ↑ 2 ) ) ) )
78	1 2	nvgcl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 )
79	12 6 7 78	mp3an	⊢ ( 𝐴 𝐺 𝐵 ) ∈ 𝑋
80	1 2	nvgcl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 ∧ ( 𝐽 𝑆 𝐶 ) ∈ 𝑋 ) → ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) ∈ 𝑋 )
81	12 79 14 80	mp3an	⊢ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) ∈ 𝑋
82	1 9 12 81	nvcli	⊢ ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ∈ ℝ
83	82	recni	⊢ ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ∈ ℂ
84	83	sqcli	⊢ ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ∈ ℂ
85	1 2	nvgcl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ ( - 1 𝑆 𝐵 ) ∈ 𝑋 ) → ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ∈ 𝑋 )
86	12 6 51 85	mp3an	⊢ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ∈ 𝑋
87	1 2	nvgcl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ∈ 𝑋 ∧ ( 𝐽 𝑆 𝐶 ) ∈ 𝑋 ) → ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) ∈ 𝑋 )
88	12 86 14 87	mp3an	⊢ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) ∈ 𝑋
89	1 9 12 88	nvcli	⊢ ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ∈ ℝ
90	89	recni	⊢ ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ∈ ℂ
91	90	sqcli	⊢ ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ∈ ℂ
92	1 2	nvgcl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 ∧ ( - 𝐽 𝑆 𝐶 ) ∈ 𝑋 ) → ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ∈ 𝑋 )
93	12 79 22 92	mp3an	⊢ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ∈ 𝑋
94	1 9 12 93	nvcli	⊢ ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ∈ ℝ
95	94	recni	⊢ ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ∈ ℂ
96	95	sqcli	⊢ ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ∈ ℂ
97	1 2	nvgcl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) ∈ 𝑋 ∧ ( - 𝐽 𝑆 𝐶 ) ∈ 𝑋 ) → ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ∈ 𝑋 )
98	12 86 22 97	mp3an	⊢ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ∈ 𝑋
99	1 9 12 98	nvcli	⊢ ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ∈ ℝ
100	99	recni	⊢ ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ∈ ℂ
101	100	sqcli	⊢ ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ∈ ℂ
102	84 91 96 101	addsub4i	⊢ ( ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) − ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) + ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) = ( ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) + ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) )
103	37 77 102	3eqtr2ri	⊢ ( ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 𝐵 ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) + ( ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( ( 𝐴 𝐺 ( - 1 𝑆 𝐵 ) ) 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) ) = ( 2 · ( ( ( 𝑁 ‘ ( 𝐴 𝐺 ( 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) − ( ( 𝑁 ‘ ( 𝐴 𝐺 ( - 𝐽 𝑆 𝐶 ) ) ) ↑ 2 ) ) )

Metamath Proof Explorer

Theorem ip0i

Proof