ip1ilem - Metamath Proof Explorer

	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	⊢ 𝑈 ∈ CPreHil_OLD
ip1i.a	⊢ 𝐴 ∈ 𝑋
ip1i.b	⊢ 𝐵 ∈ 𝑋
ip1i.c	⊢ 𝐶 ∈ 𝑋
ip1i.6	⊢ 𝑁 = (norm_CV‘𝑈)
ip0i.j	⊢ 𝐽 ∈ ℂ

**Assertion**
Ref	Expression
ip1ilem	⊢ (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶)) = (2 · (𝐴𝑃𝐶))

**Proof of Theorem ip1ilem**
Step	Hyp	Ref	Expression
1		ip1i.9	. . . . . . 7 ⊢ 𝑈 ∈ CPreHil_OLD
2	1	phnvi 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 ⊢ 𝑁 = (norm_CV‘𝑈)
9		ip1i.7	. . . . . . 7 ⊢ 𝑃 = (·_𝑖OLD‘𝑈)
10	5, 6, 7, 8, 9	4ipval2 29206	. . . . . 6 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (4 · (𝐴𝑃𝐶)) = ((((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2)))))
11	2, 3, 4, 10	mp3an 1460	. . . . 5 ⊢ (4 · (𝐴𝑃𝐶)) = ((((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2))))
12	11	oveq2i 7328	. . . 4 ⊢ (2 · (4 · (𝐴𝑃𝐶))) = (2 · ((((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2)))))
13		2cn 12128	. . . . 5 ⊢ 2 ∈ ℂ
14		4cn 12138	. . . . 5 ⊢ 4 ∈ ℂ
15	5, 9	dipcl 29210	. . . . . 6 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (𝐴𝑃𝐶) ∈ ℂ)
16	2, 3, 4, 15	mp3an 1460	. . . . 5 ⊢ (𝐴𝑃𝐶) ∈ ℂ
17	13, 14, 16	mul12i 11250	. . . 4 ⊢ (2 · (4 · (𝐴𝑃𝐶))) = (4 · (2 · (𝐴𝑃𝐶)))
18	5, 6	nvgcl 29118	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (𝐴𝐺𝐶) ∈ 𝑋)
19	2, 3, 4, 18	mp3an 1460	. . . . . . . . . . 11 ⊢ (𝐴𝐺𝐶) ∈ 𝑋
20	5, 8, 2, 19	nvcli 29160	. . . . . . . . . 10 ⊢ (𝑁‘(𝐴𝐺𝐶)) ∈ ℝ
21	20	resqcli 13983	. . . . . . . . 9 ⊢ ((𝑁‘(𝐴𝐺𝐶))↑2) ∈ ℝ
22	21	recni 11069	. . . . . . . 8 ⊢ ((𝑁‘(𝐴𝐺𝐶))↑2) ∈ ℂ
23		ax-1cn 11009	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℂ
24	23	negcli 11369	. . . . . . . . . . . . 13 ⊢ -1 ∈ ℂ
25	5, 7	nvscl 29124	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ NrmCVec ∧ -1 ∈ ℂ ∧ 𝐶 ∈ 𝑋) → (-1𝑆𝐶) ∈ 𝑋)
26	2, 24, 4, 25	mp3an 1460	. . . . . . . . . . . 12 ⊢ (-1𝑆𝐶) ∈ 𝑋
27	5, 6	nvgcl 29118	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ (-1𝑆𝐶) ∈ 𝑋) → (𝐴𝐺(-1𝑆𝐶)) ∈ 𝑋)
28	2, 3, 26, 27	mp3an 1460	. . . . . . . . . . 11 ⊢ (𝐴𝐺(-1𝑆𝐶)) ∈ 𝑋
29	5, 8, 2, 28	nvcli 29160	. . . . . . . . . 10 ⊢ (𝑁‘(𝐴𝐺(-1𝑆𝐶))) ∈ ℝ
30	29	resqcli 13983	. . . . . . . . 9 ⊢ ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2) ∈ ℝ
31	30	recni 11069	. . . . . . . 8 ⊢ ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2) ∈ ℂ
32	22, 31	subcli 11377	. . . . . . 7 ⊢ (((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2)) ∈ ℂ
33		ax-icn 11010	. . . . . . . 8 ⊢ i ∈ ℂ
34	5, 7	nvscl 29124	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ i ∈ ℂ ∧ 𝐶 ∈ 𝑋) → (i𝑆𝐶) ∈ 𝑋)
35	2, 33, 4, 34	mp3an 1460	. . . . . . . . . . . . 13 ⊢ (i𝑆𝐶) ∈ 𝑋
36	5, 6	nvgcl 29118	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ (i𝑆𝐶) ∈ 𝑋) → (𝐴𝐺(i𝑆𝐶)) ∈ 𝑋)
37	2, 3, 35, 36	mp3an 1460	. . . . . . . . . . . 12 ⊢ (𝐴𝐺(i𝑆𝐶)) ∈ 𝑋
38	5, 8, 2, 37	nvcli 29160	. . . . . . . . . . 11 ⊢ (𝑁‘(𝐴𝐺(i𝑆𝐶))) ∈ ℝ
39	38	resqcli 13983	. . . . . . . . . 10 ⊢ ((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) ∈ ℝ
40	39	recni 11069	. . . . . . . . 9 ⊢ ((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) ∈ ℂ
41	33	negcli 11369	. . . . . . . . . . . . . 14 ⊢ -i ∈ ℂ
42	5, 7	nvscl 29124	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ -i ∈ ℂ ∧ 𝐶 ∈ 𝑋) → (-i𝑆𝐶) ∈ 𝑋)
43	2, 41, 4, 42	mp3an 1460	. . . . . . . . . . . . 13 ⊢ (-i𝑆𝐶) ∈ 𝑋
44	5, 6	nvgcl 29118	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ (-i𝑆𝐶) ∈ 𝑋) → (𝐴𝐺(-i𝑆𝐶)) ∈ 𝑋)
45	2, 3, 43, 44	mp3an 1460	. . . . . . . . . . . 12 ⊢ (𝐴𝐺(-i𝑆𝐶)) ∈ 𝑋
46	5, 8, 2, 45	nvcli 29160	. . . . . . . . . . 11 ⊢ (𝑁‘(𝐴𝐺(-i𝑆𝐶))) ∈ ℝ
47	46	resqcli 13983	. . . . . . . . . 10 ⊢ ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2) ∈ ℝ
48	47	recni 11069	. . . . . . . . 9 ⊢ ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2) ∈ ℂ
49	40, 48	subcli 11377	. . . . . . . 8 ⊢ (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2)) ∈ ℂ
50	33, 49	mulcli 11062	. . . . . . 7 ⊢ (i · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2))) ∈ ℂ
51	13, 32, 50	adddii 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 ⊢ 𝐵 ∈ 𝑋
53	5, 6, 7, 9, 1, 3, 52, 4, 8, 23	ip0i 29323	. . . . . . . 8 ⊢ ((((𝑁‘((𝐴𝐺𝐵)𝐺(1𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2)) + (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(1𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2))) = (2 · (((𝑁‘(𝐴𝐺(1𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2)))
54	5, 7	nvsid 29125	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐶 ∈ 𝑋) → (1𝑆𝐶) = 𝐶)
55	2, 4, 54	mp2an 689	. . . . . . . . . . . . 13 ⊢ (1𝑆𝐶) = 𝐶
56	55	oveq2i 7328	. . . . . . . . . . . 12 ⊢ ((𝐴𝐺𝐵)𝐺(1𝑆𝐶)) = ((𝐴𝐺𝐵)𝐺𝐶)
57	56	fveq2i 6815	. . . . . . . . . . 11 ⊢ (𝑁‘((𝐴𝐺𝐵)𝐺(1𝑆𝐶))) = (𝑁‘((𝐴𝐺𝐵)𝐺𝐶))
58	57	oveq1i 7327	. . . . . . . . . 10 ⊢ ((𝑁‘((𝐴𝐺𝐵)𝐺(1𝑆𝐶)))↑2) = ((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2)
59	58	oveq1i 7327	. . . . . . . . 9 ⊢ (((𝑁‘((𝐴𝐺𝐵)𝐺(1𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2)) = (((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2))
60	55	oveq2i 7328	. . . . . . . . . . . 12 ⊢ ((𝐴𝐺(-1𝑆𝐵))𝐺(1𝑆𝐶)) = ((𝐴𝐺(-1𝑆𝐵))𝐺𝐶)
61	60	fveq2i 6815	. . . . . . . . . . 11 ⊢ (𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(1𝑆𝐶))) = (𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))
62	61	oveq1i 7327	. . . . . . . . . 10 ⊢ ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(1𝑆𝐶)))↑2) = ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))↑2)
63	62	oveq1i 7327	. . . . . . . . 9 ⊢ (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(1𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2)) = (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2))
64	59, 63	oveq12i 7329	. . . . . . . 8 ⊢ ((((𝑁‘((𝐴𝐺𝐵)𝐺(1𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2)) + (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(1𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2))) = ((((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2)) + (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2)))
65	55	oveq2i 7328	. . . . . . . . . . . 12 ⊢ (𝐴𝐺(1𝑆𝐶)) = (𝐴𝐺𝐶)
66	65	fveq2i 6815	. . . . . . . . . . 11 ⊢ (𝑁‘(𝐴𝐺(1𝑆𝐶))) = (𝑁‘(𝐴𝐺𝐶))
67	66	oveq1i 7327	. . . . . . . . . 10 ⊢ ((𝑁‘(𝐴𝐺(1𝑆𝐶)))↑2) = ((𝑁‘(𝐴𝐺𝐶))↑2)
68	67	oveq1i 7327	. . . . . . . . 9 ⊢ (((𝑁‘(𝐴𝐺(1𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2)) = (((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2))
69	68	oveq2i 7328	. . . . . . . 8 ⊢ (2 · (((𝑁‘(𝐴𝐺(1𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2))) = (2 · (((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2)))
70	53, 64, 69	3eqtr3i 2773	. . . . . . 7 ⊢ ((((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2)) + (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2))) = (2 · (((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2)))
71	5, 6, 7, 9, 1, 3, 52, 4, 8, 33	ip0i 29323	. . . . . . . . 9 ⊢ ((((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2)) + (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2))) = (2 · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2)))
72	71	oveq2i 7328	. . . . . . . 8 ⊢ (i · ((((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2)) + (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2)))) = (i · (2 · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2))))
73	5, 6	nvgcl 29118	. . . . . . . . . . . . . . 15 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐺𝐵) ∈ 𝑋)
74	2, 3, 52, 73	mp3an 1460	. . . . . . . . . . . . . 14 ⊢ (𝐴𝐺𝐵) ∈ 𝑋
75	5, 6	nvgcl 29118	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺𝐵) ∈ 𝑋 ∧ (i𝑆𝐶) ∈ 𝑋) → ((𝐴𝐺𝐵)𝐺(i𝑆𝐶)) ∈ 𝑋)
76	2, 74, 35, 75	mp3an 1460	. . . . . . . . . . . . 13 ⊢ ((𝐴𝐺𝐵)𝐺(i𝑆𝐶)) ∈ 𝑋
77	5, 8, 2, 76	nvcli 29160	. . . . . . . . . . . 12 ⊢ (𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶))) ∈ ℝ
78	77	resqcli 13983	. . . . . . . . . . 11 ⊢ ((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) ∈ ℝ
79	78	recni 11069	. . . . . . . . . 10 ⊢ ((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) ∈ ℂ
80	5, 6	nvgcl 29118	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺𝐵) ∈ 𝑋 ∧ (-i𝑆𝐶) ∈ 𝑋) → ((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)) ∈ 𝑋)
81	2, 74, 43, 80	mp3an 1460	. . . . . . . . . . . . 13 ⊢ ((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)) ∈ 𝑋
82	5, 8, 2, 81	nvcli 29160	. . . . . . . . . . . 12 ⊢ (𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶))) ∈ ℝ
83	82	resqcli 13983	. . . . . . . . . . 11 ⊢ ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2) ∈ ℝ
84	83	recni 11069	. . . . . . . . . 10 ⊢ ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2) ∈ ℂ
85	79, 84	subcli 11377	. . . . . . . . 9 ⊢ (((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2)) ∈ ℂ
86	5, 7	nvscl 29124	. . . . . . . . . . . . . . . 16 ⊢ ((𝑈 ∈ NrmCVec ∧ -1 ∈ ℂ ∧ 𝐵 ∈ 𝑋) → (-1𝑆𝐵) ∈ 𝑋)
87	2, 24, 52, 86	mp3an 1460	. . . . . . . . . . . . . . 15 ⊢ (-1𝑆𝐵) ∈ 𝑋
88	5, 6	nvgcl 29118	. . . . . . . . . . . . . . 15 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ (-1𝑆𝐵) ∈ 𝑋) → (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋)
89	2, 3, 87, 88	mp3an 1460	. . . . . . . . . . . . . 14 ⊢ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋
90	5, 6	nvgcl 29118	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋 ∧ (i𝑆𝐶) ∈ 𝑋) → ((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)) ∈ 𝑋)
91	2, 89, 35, 90	mp3an 1460	. . . . . . . . . . . . 13 ⊢ ((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)) ∈ 𝑋
92	5, 8, 2, 91	nvcli 29160	. . . . . . . . . . . 12 ⊢ (𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶))) ∈ ℝ
93	92	resqcli 13983	. . . . . . . . . . 11 ⊢ ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) ∈ ℝ
94	93	recni 11069	. . . . . . . . . 10 ⊢ ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) ∈ ℂ
95	5, 6	nvgcl 29118	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋 ∧ (-i𝑆𝐶) ∈ 𝑋) → ((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)) ∈ 𝑋)
96	2, 89, 43, 95	mp3an 1460	. . . . . . . . . . . . 13 ⊢ ((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)) ∈ 𝑋
97	5, 8, 2, 96	nvcli 29160	. . . . . . . . . . . 12 ⊢ (𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶))) ∈ ℝ
98	97	resqcli 13983	. . . . . . . . . . 11 ⊢ ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2) ∈ ℝ
99	98	recni 11069	. . . . . . . . . 10 ⊢ ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2) ∈ ℂ
100	94, 99	subcli 11377	. . . . . . . . 9 ⊢ (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2)) ∈ ℂ
101	33, 85, 100	adddii 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))))
102	33, 13, 49	mul12i 11250	. . . . . . . 8 ⊢ (i · (2 · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2)))) = (2 · (i · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2))))
103	72, 101, 102	3eqtr3i 2773	. . . . . . 7 ⊢ ((i · (((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2))) + (i · (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2)))) = (2 · (i · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2))))
104	70, 103	oveq12i 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)))))
105	51, 104	eqtr4i 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)))))
106	5, 6	nvgcl 29118	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺𝐵) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → ((𝐴𝐺𝐵)𝐺𝐶) ∈ 𝑋)
107	2, 74, 4, 106	mp3an 1460	. . . . . . . . . 10 ⊢ ((𝐴𝐺𝐵)𝐺𝐶) ∈ 𝑋
108	5, 8, 2, 107	nvcli 29160	. . . . . . . . 9 ⊢ (𝑁‘((𝐴𝐺𝐵)𝐺𝐶)) ∈ ℝ
109	108	resqcli 13983	. . . . . . . 8 ⊢ ((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) ∈ ℝ
110	109	recni 11069	. . . . . . 7 ⊢ ((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) ∈ ℂ
111	5, 6	nvgcl 29118	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺𝐵) ∈ 𝑋 ∧ (-1𝑆𝐶) ∈ 𝑋) → ((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)) ∈ 𝑋)
112	2, 74, 26, 111	mp3an 1460	. . . . . . . . . 10 ⊢ ((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)) ∈ 𝑋
113	5, 8, 2, 112	nvcli 29160	. . . . . . . . 9 ⊢ (𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶))) ∈ ℝ
114	113	resqcli 13983	. . . . . . . 8 ⊢ ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2) ∈ ℝ
115	114	recni 11069	. . . . . . 7 ⊢ ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2) ∈ ℂ
116	110, 115	subcli 11377	. . . . . 6 ⊢ (((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2)) ∈ ℂ
117	5, 6	nvgcl 29118	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → ((𝐴𝐺(-1𝑆𝐵))𝐺𝐶) ∈ 𝑋)
118	2, 89, 4, 117	mp3an 1460	. . . . . . . . . 10 ⊢ ((𝐴𝐺(-1𝑆𝐵))𝐺𝐶) ∈ 𝑋
119	5, 8, 2, 118	nvcli 29160	. . . . . . . . 9 ⊢ (𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶)) ∈ ℝ
120	119	resqcli 13983	. . . . . . . 8 ⊢ ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))↑2) ∈ ℝ
121	120	recni 11069	. . . . . . 7 ⊢ ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))↑2) ∈ ℂ
122	5, 6	nvgcl 29118	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋 ∧ (-1𝑆𝐶) ∈ 𝑋) → ((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)) ∈ 𝑋)
123	2, 89, 26, 122	mp3an 1460	. . . . . . . . . 10 ⊢ ((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)) ∈ 𝑋
124	5, 8, 2, 123	nvcli 29160	. . . . . . . . 9 ⊢ (𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶))) ∈ ℝ
125	124	resqcli 13983	. . . . . . . 8 ⊢ ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2) ∈ ℝ
126	125	recni 11069	. . . . . . 7 ⊢ ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2) ∈ ℂ
127	121, 126	subcli 11377	. . . . . 6 ⊢ (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2)) ∈ ℂ
128	33, 85	mulcli 11062	. . . . . 6 ⊢ (i · (((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2))) ∈ ℂ
129	33, 100	mulcli 11062	. . . . . 6 ⊢ (i · (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2))) ∈ ℂ
130	116, 127, 128, 129	add4i 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)))))
131	5, 9	dipcl 29210	. . . . . . . 8 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺𝐵) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → ((𝐴𝐺𝐵)𝑃𝐶) ∈ ℂ)
132	2, 74, 4, 131	mp3an 1460	. . . . . . 7 ⊢ ((𝐴𝐺𝐵)𝑃𝐶) ∈ ℂ
133	5, 9	dipcl 29210	. . . . . . . 8 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶) ∈ ℂ)
134	2, 89, 4, 133	mp3an 1460	. . . . . . 7 ⊢ ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶) ∈ ℂ
135	14, 132, 134	adddii 11067	. . . . . 6 ⊢ (4 · (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶))) = ((4 · ((𝐴𝐺𝐵)𝑃𝐶)) + (4 · ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶)))
136	5, 6, 7, 8, 9	4ipval2 29206	. . . . . . . 8 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺𝐵) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (4 · ((𝐴𝐺𝐵)𝑃𝐶)) = ((((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2)))))
137	2, 74, 4, 136	mp3an 1460	. . . . . . 7 ⊢ (4 · ((𝐴𝐺𝐵)𝑃𝐶)) = ((((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2))))
138	5, 6, 7, 8, 9	4ipval2 29206	. . . . . . . 8 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (4 · ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶)) = ((((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2)))))
139	2, 89, 4, 138	mp3an 1460	. . . . . . 7 ⊢ (4 · ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶)) = ((((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2))))
140	137, 139	oveq12i 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)))))
141	135, 140	eqtr2i 2766	. . . . 5 ⊢ (((((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2)))) + ((((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2))))) = (4 · (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶)))
142	105, 130, 141	3eqtri 2769	. . . 4 ⊢ (2 · ((((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2))))) = (4 · (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶)))
143	12, 17, 142	3eqtr3ri 2774	. . 3 ⊢ (4 · (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶))) = (4 · (2 · (𝐴𝑃𝐶)))
144	143	oveq1i 7327	. 2 ⊢ ((4 · (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶))) / 4) = ((4 · (2 · (𝐴𝑃𝐶))) / 4)
145	132, 134	addcli 11061	. . 3 ⊢ (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶)) ∈ ℂ
146		4ne0 12161	. . 3 ⊢ 4 ≠ 0
147	145, 14, 146	divcan3i 11801	. 2 ⊢ ((4 · (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶))) / 4) = (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶))
148	13, 16	mulcli 11062	. . 3 ⊢ (2 · (𝐴𝑃𝐶)) ∈ ℂ
149	148, 14, 146	divcan3i 11801	. 2 ⊢ ((4 · (2 · (𝐴𝑃𝐶))) / 4) = (2 · (𝐴𝑃𝐶))
150	144, 147, 149	3eqtr3i 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 norm_CVcnmcv 29088 ·_𝑖OLDcdip 29198 CPreHil_OLDccphlo 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

W3C validator