MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ip1ilem Structured version   Visualization version   GIF version

Theorem ip1ilem 29324
Description: Lemma for ip1i 29325. (Contributed by NM, 21-Apr-2007.) (New usage is discouraged.)
Hypotheses
Ref Expression
ip1i.1 𝑋 = (BaseSet‘𝑈)
ip1i.2 𝐺 = ( +𝑣𝑈)
ip1i.4 𝑆 = ( ·𝑠OLD𝑈)
ip1i.7 𝑃 = (·𝑖OLD𝑈)
ip1i.9 𝑈 ∈ CPreHilOLD
ip1i.a 𝐴𝑋
ip1i.b 𝐵𝑋
ip1i.c 𝐶𝑋
ip1i.6 𝑁 = (normCV𝑈)
ip0i.j 𝐽 ∈ ℂ
Assertion
Ref Expression
ip1ilem (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶)) = (2 · (𝐴𝑃𝐶))

Proof of Theorem ip1ilem
StepHypRef Expression
1 ip1i.9 . . . . . . 7 𝑈 ∈ CPreHilOLD
21phnvi 29314 . . . . . 6 𝑈 ∈ NrmCVec
3 ip1i.a . . . . . 6 𝐴𝑋
4 ip1i.c . . . . . 6 𝐶𝑋
5 ip1i.1 . . . . . . 7 𝑋 = (BaseSet‘𝑈)
6 ip1i.2 . . . . . . 7 𝐺 = ( +𝑣𝑈)
7 ip1i.4 . . . . . . 7 𝑆 = ( ·𝑠OLD𝑈)
8 ip1i.6 . . . . . . 7 𝑁 = (normCV𝑈)
9 ip1i.7 . . . . . . 7 𝑃 = (·𝑖OLD𝑈)
105, 6, 7, 8, 94ipval2 29206 . . . . . 6 ((𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐶𝑋) → (4 · (𝐴𝑃𝐶)) = ((((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2)))))
112, 3, 4, 10mp3an 1460 . . . . 5 (4 · (𝐴𝑃𝐶)) = ((((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2))))
1211oveq2i 7328 . . . 4 (2 · (4 · (𝐴𝑃𝐶))) = (2 · ((((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2)))))
13 2cn 12128 . . . . 5 2 ∈ ℂ
14 4cn 12138 . . . . 5 4 ∈ ℂ
155, 9dipcl 29210 . . . . . 6 ((𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐶𝑋) → (𝐴𝑃𝐶) ∈ ℂ)
162, 3, 4, 15mp3an 1460 . . . . 5 (𝐴𝑃𝐶) ∈ ℂ
1713, 14, 16mul12i 11250 . . . 4 (2 · (4 · (𝐴𝑃𝐶))) = (4 · (2 · (𝐴𝑃𝐶)))
185, 6nvgcl 29118 . . . . . . . . . . . 12 ((𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐶𝑋) → (𝐴𝐺𝐶) ∈ 𝑋)
192, 3, 4, 18mp3an 1460 . . . . . . . . . . 11 (𝐴𝐺𝐶) ∈ 𝑋
205, 8, 2, 19nvcli 29160 . . . . . . . . . 10 (𝑁‘(𝐴𝐺𝐶)) ∈ ℝ
2120resqcli 13983 . . . . . . . . 9 ((𝑁‘(𝐴𝐺𝐶))↑2) ∈ ℝ
2221recni 11069 . . . . . . . 8 ((𝑁‘(𝐴𝐺𝐶))↑2) ∈ ℂ
23 ax-1cn 11009 . . . . . . . . . . . . . 14 1 ∈ ℂ
2423negcli 11369 . . . . . . . . . . . . 13 -1 ∈ ℂ
255, 7nvscl 29124 . . . . . . . . . . . . 13 ((𝑈 ∈ NrmCVec ∧ -1 ∈ ℂ ∧ 𝐶𝑋) → (-1𝑆𝐶) ∈ 𝑋)
262, 24, 4, 25mp3an 1460 . . . . . . . . . . . 12 (-1𝑆𝐶) ∈ 𝑋
275, 6nvgcl 29118 . . . . . . . . . . . 12 ((𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ∧ (-1𝑆𝐶) ∈ 𝑋) → (𝐴𝐺(-1𝑆𝐶)) ∈ 𝑋)
282, 3, 26, 27mp3an 1460 . . . . . . . . . . 11 (𝐴𝐺(-1𝑆𝐶)) ∈ 𝑋
295, 8, 2, 28nvcli 29160 . . . . . . . . . 10 (𝑁‘(𝐴𝐺(-1𝑆𝐶))) ∈ ℝ
3029resqcli 13983 . . . . . . . . 9 ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2) ∈ ℝ
3130recni 11069 . . . . . . . 8 ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2) ∈ ℂ
3222, 31subcli 11377 . . . . . . 7 (((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2)) ∈ ℂ
33 ax-icn 11010 . . . . . . . 8 i ∈ ℂ
345, 7nvscl 29124 . . . . . . . . . . . . . 14 ((𝑈 ∈ NrmCVec ∧ i ∈ ℂ ∧ 𝐶𝑋) → (i𝑆𝐶) ∈ 𝑋)
352, 33, 4, 34mp3an 1460 . . . . . . . . . . . . 13 (i𝑆𝐶) ∈ 𝑋
365, 6nvgcl 29118 . . . . . . . . . . . . 13 ((𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ∧ (i𝑆𝐶) ∈ 𝑋) → (𝐴𝐺(i𝑆𝐶)) ∈ 𝑋)
372, 3, 35, 36mp3an 1460 . . . . . . . . . . . 12 (𝐴𝐺(i𝑆𝐶)) ∈ 𝑋
385, 8, 2, 37nvcli 29160 . . . . . . . . . . 11 (𝑁‘(𝐴𝐺(i𝑆𝐶))) ∈ ℝ
3938resqcli 13983 . . . . . . . . . 10 ((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) ∈ ℝ
4039recni 11069 . . . . . . . . 9 ((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) ∈ ℂ
4133negcli 11369 . . . . . . . . . . . . . 14 -i ∈ ℂ
425, 7nvscl 29124 . . . . . . . . . . . . . 14 ((𝑈 ∈ NrmCVec ∧ -i ∈ ℂ ∧ 𝐶𝑋) → (-i𝑆𝐶) ∈ 𝑋)
432, 41, 4, 42mp3an 1460 . . . . . . . . . . . . 13 (-i𝑆𝐶) ∈ 𝑋
445, 6nvgcl 29118 . . . . . . . . . . . . 13 ((𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ∧ (-i𝑆𝐶) ∈ 𝑋) → (𝐴𝐺(-i𝑆𝐶)) ∈ 𝑋)
452, 3, 43, 44mp3an 1460 . . . . . . . . . . . 12 (𝐴𝐺(-i𝑆𝐶)) ∈ 𝑋
465, 8, 2, 45nvcli 29160 . . . . . . . . . . 11 (𝑁‘(𝐴𝐺(-i𝑆𝐶))) ∈ ℝ
4746resqcli 13983 . . . . . . . . . 10 ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2) ∈ ℝ
4847recni 11069 . . . . . . . . 9 ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2) ∈ ℂ
4940, 48subcli 11377 . . . . . . . 8 (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2)) ∈ ℂ
5033, 49mulcli 11062 . . . . . . 7 (i · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2))) ∈ ℂ
5113, 32, 50adddii 11067 . . . . . 6 (2 · ((((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2))))) = ((2 · (((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2))) + (2 · (i · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2)))))
52 ip1i.b . . . . . . . . 9 𝐵𝑋
535, 6, 7, 9, 1, 3, 52, 4, 8, 23ip0i 29323 . . . . . . . 8 ((((𝑁‘((𝐴𝐺𝐵)𝐺(1𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2)) + (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(1𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2))) = (2 · (((𝑁‘(𝐴𝐺(1𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2)))
545, 7nvsid 29125 . . . . . . . . . . . . . 14 ((𝑈 ∈ NrmCVec ∧ 𝐶𝑋) → (1𝑆𝐶) = 𝐶)
552, 4, 54mp2an 689 . . . . . . . . . . . . 13 (1𝑆𝐶) = 𝐶
5655oveq2i 7328 . . . . . . . . . . . 12 ((𝐴𝐺𝐵)𝐺(1𝑆𝐶)) = ((𝐴𝐺𝐵)𝐺𝐶)
5756fveq2i 6815 . . . . . . . . . . 11 (𝑁‘((𝐴𝐺𝐵)𝐺(1𝑆𝐶))) = (𝑁‘((𝐴𝐺𝐵)𝐺𝐶))
5857oveq1i 7327 . . . . . . . . . 10 ((𝑁‘((𝐴𝐺𝐵)𝐺(1𝑆𝐶)))↑2) = ((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2)
5958oveq1i 7327 . . . . . . . . 9 (((𝑁‘((𝐴𝐺𝐵)𝐺(1𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2)) = (((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2))
6055oveq2i 7328 . . . . . . . . . . . 12 ((𝐴𝐺(-1𝑆𝐵))𝐺(1𝑆𝐶)) = ((𝐴𝐺(-1𝑆𝐵))𝐺𝐶)
6160fveq2i 6815 . . . . . . . . . . 11 (𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(1𝑆𝐶))) = (𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))
6261oveq1i 7327 . . . . . . . . . 10 ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(1𝑆𝐶)))↑2) = ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))↑2)
6362oveq1i 7327 . . . . . . . . 9 (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(1𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2)) = (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2))
6459, 63oveq12i 7329 . . . . . . . 8 ((((𝑁‘((𝐴𝐺𝐵)𝐺(1𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2)) + (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(1𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2))) = ((((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2)) + (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2)))
6555oveq2i 7328 . . . . . . . . . . . 12 (𝐴𝐺(1𝑆𝐶)) = (𝐴𝐺𝐶)
6665fveq2i 6815 . . . . . . . . . . 11 (𝑁‘(𝐴𝐺(1𝑆𝐶))) = (𝑁‘(𝐴𝐺𝐶))
6766oveq1i 7327 . . . . . . . . . 10 ((𝑁‘(𝐴𝐺(1𝑆𝐶)))↑2) = ((𝑁‘(𝐴𝐺𝐶))↑2)
6867oveq1i 7327 . . . . . . . . 9 (((𝑁‘(𝐴𝐺(1𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2)) = (((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2))
6968oveq2i 7328 . . . . . . . 8 (2 · (((𝑁‘(𝐴𝐺(1𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2))) = (2 · (((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2)))
7053, 64, 693eqtr3i 2773 . . . . . . 7 ((((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2)) + (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2))) = (2 · (((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2)))
715, 6, 7, 9, 1, 3, 52, 4, 8, 33ip0i 29323 . . . . . . . . 9 ((((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2)) + (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2))) = (2 · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2)))
7271oveq2i 7328 . . . . . . . 8 (i · ((((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2)) + (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2)))) = (i · (2 · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2))))
735, 6nvgcl 29118 . . . . . . . . . . . . . . 15 ((𝑈 ∈ NrmCVec ∧ 𝐴𝑋𝐵𝑋) → (𝐴𝐺𝐵) ∈ 𝑋)
742, 3, 52, 73mp3an 1460 . . . . . . . . . . . . . 14 (𝐴𝐺𝐵) ∈ 𝑋
755, 6nvgcl 29118 . . . . . . . . . . . . . 14 ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺𝐵) ∈ 𝑋 ∧ (i𝑆𝐶) ∈ 𝑋) → ((𝐴𝐺𝐵)𝐺(i𝑆𝐶)) ∈ 𝑋)
762, 74, 35, 75mp3an 1460 . . . . . . . . . . . . 13 ((𝐴𝐺𝐵)𝐺(i𝑆𝐶)) ∈ 𝑋
775, 8, 2, 76nvcli 29160 . . . . . . . . . . . 12 (𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶))) ∈ ℝ
7877resqcli 13983 . . . . . . . . . . 11 ((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) ∈ ℝ
7978recni 11069 . . . . . . . . . 10 ((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) ∈ ℂ
805, 6nvgcl 29118 . . . . . . . . . . . . . 14 ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺𝐵) ∈ 𝑋 ∧ (-i𝑆𝐶) ∈ 𝑋) → ((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)) ∈ 𝑋)
812, 74, 43, 80mp3an 1460 . . . . . . . . . . . . 13 ((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)) ∈ 𝑋
825, 8, 2, 81nvcli 29160 . . . . . . . . . . . 12 (𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶))) ∈ ℝ
8382resqcli 13983 . . . . . . . . . . 11 ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2) ∈ ℝ
8483recni 11069 . . . . . . . . . 10 ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2) ∈ ℂ
8579, 84subcli 11377 . . . . . . . . 9 (((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2)) ∈ ℂ
865, 7nvscl 29124 . . . . . . . . . . . . . . . 16 ((𝑈 ∈ NrmCVec ∧ -1 ∈ ℂ ∧ 𝐵𝑋) → (-1𝑆𝐵) ∈ 𝑋)
872, 24, 52, 86mp3an 1460 . . . . . . . . . . . . . . 15 (-1𝑆𝐵) ∈ 𝑋
885, 6nvgcl 29118 . . . . . . . . . . . . . . 15 ((𝑈 ∈ NrmCVec ∧ 𝐴𝑋 ∧ (-1𝑆𝐵) ∈ 𝑋) → (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋)
892, 3, 87, 88mp3an 1460 . . . . . . . . . . . . . 14 (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋
905, 6nvgcl 29118 . . . . . . . . . . . . . 14 ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋 ∧ (i𝑆𝐶) ∈ 𝑋) → ((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)) ∈ 𝑋)
912, 89, 35, 90mp3an 1460 . . . . . . . . . . . . 13 ((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)) ∈ 𝑋
925, 8, 2, 91nvcli 29160 . . . . . . . . . . . 12 (𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶))) ∈ ℝ
9392resqcli 13983 . . . . . . . . . . 11 ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) ∈ ℝ
9493recni 11069 . . . . . . . . . 10 ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) ∈ ℂ
955, 6nvgcl 29118 . . . . . . . . . . . . . 14 ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋 ∧ (-i𝑆𝐶) ∈ 𝑋) → ((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)) ∈ 𝑋)
962, 89, 43, 95mp3an 1460 . . . . . . . . . . . . 13 ((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)) ∈ 𝑋
975, 8, 2, 96nvcli 29160 . . . . . . . . . . . 12 (𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶))) ∈ ℝ
9897resqcli 13983 . . . . . . . . . . 11 ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2) ∈ ℝ
9998recni 11069 . . . . . . . . . 10 ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2) ∈ ℂ
10094, 99subcli 11377 . . . . . . . . 9 (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2)) ∈ ℂ
10133, 85, 100adddii 11067 . . . . . . . 8 (i · ((((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2)) + (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2)))) = ((i · (((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2))) + (i · (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2))))
10233, 13, 49mul12i 11250 . . . . . . . 8 (i · (2 · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2)))) = (2 · (i · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2))))
10372, 101, 1023eqtr3i 2773 . . . . . . 7 ((i · (((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2))) + (i · (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2)))) = (2 · (i · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2))))
10470, 103oveq12i 7329 . . . . . 6 (((((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2)) + (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2))) + ((i · (((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2))) + (i · (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2))))) = ((2 · (((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2))) + (2 · (i · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2)))))
10551, 104eqtr4i 2768 . . . . 5 (2 · ((((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2))))) = (((((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2)) + (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2))) + ((i · (((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2))) + (i · (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2)))))
1065, 6nvgcl 29118 . . . . . . . . . . 11 ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺𝐵) ∈ 𝑋𝐶𝑋) → ((𝐴𝐺𝐵)𝐺𝐶) ∈ 𝑋)
1072, 74, 4, 106mp3an 1460 . . . . . . . . . 10 ((𝐴𝐺𝐵)𝐺𝐶) ∈ 𝑋
1085, 8, 2, 107nvcli 29160 . . . . . . . . 9 (𝑁‘((𝐴𝐺𝐵)𝐺𝐶)) ∈ ℝ
109108resqcli 13983 . . . . . . . 8 ((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) ∈ ℝ
110109recni 11069 . . . . . . 7 ((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) ∈ ℂ
1115, 6nvgcl 29118 . . . . . . . . . . 11 ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺𝐵) ∈ 𝑋 ∧ (-1𝑆𝐶) ∈ 𝑋) → ((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)) ∈ 𝑋)
1122, 74, 26, 111mp3an 1460 . . . . . . . . . 10 ((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)) ∈ 𝑋
1135, 8, 2, 112nvcli 29160 . . . . . . . . 9 (𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶))) ∈ ℝ
114113resqcli 13983 . . . . . . . 8 ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2) ∈ ℝ
115114recni 11069 . . . . . . 7 ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2) ∈ ℂ
116110, 115subcli 11377 . . . . . 6 (((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2)) ∈ ℂ
1175, 6nvgcl 29118 . . . . . . . . . . 11 ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋𝐶𝑋) → ((𝐴𝐺(-1𝑆𝐵))𝐺𝐶) ∈ 𝑋)
1182, 89, 4, 117mp3an 1460 . . . . . . . . . 10 ((𝐴𝐺(-1𝑆𝐵))𝐺𝐶) ∈ 𝑋
1195, 8, 2, 118nvcli 29160 . . . . . . . . 9 (𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶)) ∈ ℝ
120119resqcli 13983 . . . . . . . 8 ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))↑2) ∈ ℝ
121120recni 11069 . . . . . . 7 ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))↑2) ∈ ℂ
1225, 6nvgcl 29118 . . . . . . . . . . 11 ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋 ∧ (-1𝑆𝐶) ∈ 𝑋) → ((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)) ∈ 𝑋)
1232, 89, 26, 122mp3an 1460 . . . . . . . . . 10 ((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)) ∈ 𝑋
1245, 8, 2, 123nvcli 29160 . . . . . . . . 9 (𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶))) ∈ ℝ
125124resqcli 13983 . . . . . . . 8 ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2) ∈ ℝ
126125recni 11069 . . . . . . 7 ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2) ∈ ℂ
127121, 126subcli 11377 . . . . . 6 (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2)) ∈ ℂ
12833, 85mulcli 11062 . . . . . 6 (i · (((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2))) ∈ ℂ
12933, 100mulcli 11062 . . . . . 6 (i · (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2))) ∈ ℂ
130116, 127, 128, 129add4i 11279 . . . . 5 (((((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2)) + (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2))) + ((i · (((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2))) + (i · (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2))))) = (((((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2)))) + ((((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2)))))
1315, 9dipcl 29210 . . . . . . . 8 ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺𝐵) ∈ 𝑋𝐶𝑋) → ((𝐴𝐺𝐵)𝑃𝐶) ∈ ℂ)
1322, 74, 4, 131mp3an 1460 . . . . . . 7 ((𝐴𝐺𝐵)𝑃𝐶) ∈ ℂ
1335, 9dipcl 29210 . . . . . . . 8 ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋𝐶𝑋) → ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶) ∈ ℂ)
1342, 89, 4, 133mp3an 1460 . . . . . . 7 ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶) ∈ ℂ
13514, 132, 134adddii 11067 . . . . . 6 (4 · (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶))) = ((4 · ((𝐴𝐺𝐵)𝑃𝐶)) + (4 · ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶)))
1365, 6, 7, 8, 94ipval2 29206 . . . . . . . 8 ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺𝐵) ∈ 𝑋𝐶𝑋) → (4 · ((𝐴𝐺𝐵)𝑃𝐶)) = ((((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2)))))
1372, 74, 4, 136mp3an 1460 . . . . . . 7 (4 · ((𝐴𝐺𝐵)𝑃𝐶)) = ((((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2))))
1385, 6, 7, 8, 94ipval2 29206 . . . . . . . 8 ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋𝐶𝑋) → (4 · ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶)) = ((((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2)))))
1392, 89, 4, 138mp3an 1460 . . . . . . 7 (4 · ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶)) = ((((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2))))
140137, 139oveq12i 7329 . . . . . 6 ((4 · ((𝐴𝐺𝐵)𝑃𝐶)) + (4 · ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶))) = (((((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2)))) + ((((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2)))))
141135, 140eqtr2i 2766 . . . . 5 (((((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2)))) + ((((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2))))) = (4 · (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶)))
142105, 130, 1413eqtri 2769 . . . 4 (2 · ((((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2))))) = (4 · (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶)))
14312, 17, 1423eqtr3ri 2774 . . 3 (4 · (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶))) = (4 · (2 · (𝐴𝑃𝐶)))
144143oveq1i 7327 . 2 ((4 · (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶))) / 4) = ((4 · (2 · (𝐴𝑃𝐶))) / 4)
145132, 134addcli 11061 . . 3 (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶)) ∈ ℂ
146 4ne0 12161 . . 3 4 ≠ 0
147145, 14, 146divcan3i 11801 . 2 ((4 · (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶))) / 4) = (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶))
14813, 16mulcli 11062 . . 3 (2 · (𝐴𝑃𝐶)) ∈ ℂ
149148, 14, 146divcan3i 11801 . 2 ((4 · (2 · (𝐴𝑃𝐶))) / 4) = (2 · (𝐴𝑃𝐶))
150144, 147, 1493eqtr3i 2773 1 (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶)) = (2 · (𝐴𝑃𝐶))
Colors of variables: wff setvar class
Syntax hints:   = wceq 1540  wcel 2105  cfv 6466  (class class class)co 7317  cc 10949  1c1 10952  ici 10953   + caddc 10954   · cmul 10956  cmin 11285  -cneg 11286   / cdiv 11712  2c2 12108  4c4 12110  cexp 13862  NrmCVeccnv 29082   +𝑣 cpv 29083  BaseSetcba 29084   ·𝑠OLD cns 29085  normCVcnmcv 29088  ·𝑖OLDcdip 29198  CPreHilOLDccphlo 29310
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2708  ax-rep 5224  ax-sep 5238  ax-nul 5245  ax-pow 5303  ax-pr 5367  ax-un 7630  ax-inf2 9477  ax-cnex 11007  ax-resscn 11008  ax-1cn 11009  ax-icn 11010  ax-addcl 11011  ax-addrcl 11012  ax-mulcl 11013  ax-mulrcl 11014  ax-mulcom 11015  ax-addass 11016  ax-mulass 11017  ax-distr 11018  ax-i2m1 11019  ax-1ne0 11020  ax-1rid 11021  ax-rnegex 11022  ax-rrecex 11023  ax-cnre 11024  ax-pre-lttri 11025  ax-pre-lttrn 11026  ax-pre-ltadd 11027  ax-pre-mulgt0 11028  ax-pre-sup 11029
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2887  df-ne 2942  df-nel 3048  df-ral 3063  df-rex 3072  df-rmo 3350  df-reu 3351  df-rab 3405  df-v 3443  df-sbc 3727  df-csb 3843  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-pss 3916  df-nul 4268  df-if 4472  df-pw 4547  df-sn 4572  df-pr 4574  df-op 4578  df-uni 4851  df-int 4893  df-iun 4939  df-br 5088  df-opab 5150  df-mpt 5171  df-tr 5205  df-id 5507  df-eprel 5513  df-po 5521  df-so 5522  df-fr 5563  df-se 5564  df-we 5565  df-xp 5614  df-rel 5615  df-cnv 5616  df-co 5617  df-dm 5618  df-rn 5619  df-res 5620  df-ima 5621  df-pred 6225  df-ord 6292  df-on 6293  df-lim 6294  df-suc 6295  df-iota 6418  df-fun 6468  df-fn 6469  df-f 6470  df-f1 6471  df-fo 6472  df-f1o 6473  df-fv 6474  df-isom 6475  df-riota 7274  df-ov 7320  df-oprab 7321  df-mpo 7322  df-om 7760  df-1st 7878  df-2nd 7879  df-frecs 8146  df-wrecs 8177  df-recs 8251  df-rdg 8290  df-1o 8346  df-er 8548  df-en 8784  df-dom 8785  df-sdom 8786  df-fin 8787  df-sup 9278  df-oi 9346  df-card 9775  df-pnf 11091  df-mnf 11092  df-xr 11093  df-ltxr 11094  df-le 11095  df-sub 11287  df-neg 11288  df-div 11713  df-nn 12054  df-2 12116  df-3 12117  df-4 12118  df-n0 12314  df-z 12400  df-uz 12663  df-rp 12811  df-fz 13320  df-fzo 13463  df-seq 13802  df-exp 13863  df-hash 14125  df-cj 14889  df-re 14890  df-im 14891  df-sqrt 15025  df-abs 15026  df-clim 15276  df-sum 15477  df-grpo 28991  df-ablo 29043  df-vc 29057  df-nv 29090  df-va 29093  df-ba 29094  df-sm 29095  df-0v 29096  df-nmcv 29098  df-dip 29199  df-ph 29311
This theorem is referenced by:  ip1i  29325
  Copyright terms: Public domain W3C validator