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 30919

Description: Lemma for ip1i 30920. (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 30909	. . . . . 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 30801	. . . . . 6 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (4 · (𝐴𝑃𝐶)) = ((((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2)))))
11	2, 3, 4, 10	mp3an 1470	. . . . 5 ⊢ (4 · (𝐴𝑃𝐶)) = ((((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2))))
12	11	oveq2i 7371	. . . 4 ⊢ (2 · (4 · (𝐴𝑃𝐶))) = (2 · ((((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2)))))
13		2cn 12251	. . . . 5 ⊢ 2 ∈ ℂ
14		4cn 12261	. . . . 5 ⊢ 4 ∈ ℂ
15	5, 9	dipcl 30805	. . . . . 6 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (𝐴𝑃𝐶) ∈ ℂ)
16	2, 3, 4, 15	mp3an 1470	. . . . 5 ⊢ (𝐴𝑃𝐶) ∈ ℂ
17	13, 14, 16	mul12i 11336	. . . 4 ⊢ (2 · (4 · (𝐴𝑃𝐶))) = (4 · (2 · (𝐴𝑃𝐶)))
18	5, 6	nvgcl 30713	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (𝐴𝐺𝐶) ∈ 𝑋)
19	2, 3, 4, 18	mp3an 1470	. . . . . . . . . . 11 ⊢ (𝐴𝐺𝐶) ∈ 𝑋
20	5, 8, 2, 19	nvcli 30755	. . . . . . . . . 10 ⊢ (𝑁‘(𝐴𝐺𝐶)) ∈ ℝ
21	20	resqcli 14143	. . . . . . . . 9 ⊢ ((𝑁‘(𝐴𝐺𝐶))↑2) ∈ ℝ
22	21	recni 11154	. . . . . . . 8 ⊢ ((𝑁‘(𝐴𝐺𝐶))↑2) ∈ ℂ
23		ax-1cn 11091	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℂ
24	23	negcli 11457	. . . . . . . . . . . . 13 ⊢ -1 ∈ ℂ
25	5, 7	nvscl 30719	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ NrmCVec ∧ -1 ∈ ℂ ∧ 𝐶 ∈ 𝑋) → (-1𝑆𝐶) ∈ 𝑋)
26	2, 24, 4, 25	mp3an 1470	. . . . . . . . . . . 12 ⊢ (-1𝑆𝐶) ∈ 𝑋
27	5, 6	nvgcl 30713	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ (-1𝑆𝐶) ∈ 𝑋) → (𝐴𝐺(-1𝑆𝐶)) ∈ 𝑋)
28	2, 3, 26, 27	mp3an 1470	. . . . . . . . . . 11 ⊢ (𝐴𝐺(-1𝑆𝐶)) ∈ 𝑋
29	5, 8, 2, 28	nvcli 30755	. . . . . . . . . 10 ⊢ (𝑁‘(𝐴𝐺(-1𝑆𝐶))) ∈ ℝ
30	29	resqcli 14143	. . . . . . . . 9 ⊢ ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2) ∈ ℝ
31	30	recni 11154	. . . . . . . 8 ⊢ ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2) ∈ ℂ
32	22, 31	subcli 11465	. . . . . . 7 ⊢ (((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2)) ∈ ℂ
33		ax-icn 11092	. . . . . . . 8 ⊢ i ∈ ℂ
34	5, 7	nvscl 30719	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ i ∈ ℂ ∧ 𝐶 ∈ 𝑋) → (i𝑆𝐶) ∈ 𝑋)
35	2, 33, 4, 34	mp3an 1470	. . . . . . . . . . . . 13 ⊢ (i𝑆𝐶) ∈ 𝑋
36	5, 6	nvgcl 30713	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ (i𝑆𝐶) ∈ 𝑋) → (𝐴𝐺(i𝑆𝐶)) ∈ 𝑋)
37	2, 3, 35, 36	mp3an 1470	. . . . . . . . . . . 12 ⊢ (𝐴𝐺(i𝑆𝐶)) ∈ 𝑋
38	5, 8, 2, 37	nvcli 30755	. . . . . . . . . . 11 ⊢ (𝑁‘(𝐴𝐺(i𝑆𝐶))) ∈ ℝ
39	38	resqcli 14143	. . . . . . . . . 10 ⊢ ((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) ∈ ℝ
40	39	recni 11154	. . . . . . . . 9 ⊢ ((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) ∈ ℂ
41	33	negcli 11457	. . . . . . . . . . . . . 14 ⊢ -i ∈ ℂ
42	5, 7	nvscl 30719	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ -i ∈ ℂ ∧ 𝐶 ∈ 𝑋) → (-i𝑆𝐶) ∈ 𝑋)
43	2, 41, 4, 42	mp3an 1470	. . . . . . . . . . . . 13 ⊢ (-i𝑆𝐶) ∈ 𝑋
44	5, 6	nvgcl 30713	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ (-i𝑆𝐶) ∈ 𝑋) → (𝐴𝐺(-i𝑆𝐶)) ∈ 𝑋)
45	2, 3, 43, 44	mp3an 1470	. . . . . . . . . . . 12 ⊢ (𝐴𝐺(-i𝑆𝐶)) ∈ 𝑋
46	5, 8, 2, 45	nvcli 30755	. . . . . . . . . . 11 ⊢ (𝑁‘(𝐴𝐺(-i𝑆𝐶))) ∈ ℝ
47	46	resqcli 14143	. . . . . . . . . 10 ⊢ ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2) ∈ ℝ
48	47	recni 11154	. . . . . . . . 9 ⊢ ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2) ∈ ℂ
49	40, 48	subcli 11465	. . . . . . . 8 ⊢ (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2)) ∈ ℂ
50	33, 49	mulcli 11147	. . . . . . 7 ⊢ (i · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2))) ∈ ℂ
51	13, 32, 50	adddii 11152	. . . . . 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 30918	. . . . . . . 8 ⊢ ((((𝑁‘((𝐴𝐺𝐵)𝐺(1𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2)) + (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(1𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2))) = (2 · (((𝑁‘(𝐴𝐺(1𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2)))
54	5, 7	nvsid 30720	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐶 ∈ 𝑋) → (1𝑆𝐶) = 𝐶)
55	2, 4, 54	mp2an 699	. . . . . . . . . . . . 13 ⊢ (1𝑆𝐶) = 𝐶
56	55	oveq2i 7371	. . . . . . . . . . . 12 ⊢ ((𝐴𝐺𝐵)𝐺(1𝑆𝐶)) = ((𝐴𝐺𝐵)𝐺𝐶)
57	56	fveq2i 6834	. . . . . . . . . . 11 ⊢ (𝑁‘((𝐴𝐺𝐵)𝐺(1𝑆𝐶))) = (𝑁‘((𝐴𝐺𝐵)𝐺𝐶))
58	57	oveq1i 7370	. . . . . . . . . 10 ⊢ ((𝑁‘((𝐴𝐺𝐵)𝐺(1𝑆𝐶)))↑2) = ((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2)
59	58	oveq1i 7370	. . . . . . . . 9 ⊢ (((𝑁‘((𝐴𝐺𝐵)𝐺(1𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2)) = (((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2))
60	55	oveq2i 7371	. . . . . . . . . . . 12 ⊢ ((𝐴𝐺(-1𝑆𝐵))𝐺(1𝑆𝐶)) = ((𝐴𝐺(-1𝑆𝐵))𝐺𝐶)
61	60	fveq2i 6834	. . . . . . . . . . 11 ⊢ (𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(1𝑆𝐶))) = (𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))
62	61	oveq1i 7370	. . . . . . . . . 10 ⊢ ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(1𝑆𝐶)))↑2) = ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))↑2)
63	62	oveq1i 7370	. . . . . . . . 9 ⊢ (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(1𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2)) = (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2))
64	59, 63	oveq12i 7372	. . . . . . . 8 ⊢ ((((𝑁‘((𝐴𝐺𝐵)𝐺(1𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2)) + (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(1𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2))) = ((((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2)) + (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2)))
65	55	oveq2i 7371	. . . . . . . . . . . 12 ⊢ (𝐴𝐺(1𝑆𝐶)) = (𝐴𝐺𝐶)
66	65	fveq2i 6834	. . . . . . . . . . 11 ⊢ (𝑁‘(𝐴𝐺(1𝑆𝐶))) = (𝑁‘(𝐴𝐺𝐶))
67	66	oveq1i 7370	. . . . . . . . . 10 ⊢ ((𝑁‘(𝐴𝐺(1𝑆𝐶)))↑2) = ((𝑁‘(𝐴𝐺𝐶))↑2)
68	67	oveq1i 7370	. . . . . . . . 9 ⊢ (((𝑁‘(𝐴𝐺(1𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2)) = (((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2))
69	68	oveq2i 7371	. . . . . . . 8 ⊢ (2 · (((𝑁‘(𝐴𝐺(1𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2))) = (2 · (((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2)))
70	53, 64, 69	3eqtr3i 2772	. . . . . . 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 30918	. . . . . . . . 9 ⊢ ((((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2)) + (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2))) = (2 · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2)))
72	71	oveq2i 7371	. . . . . . . 8 ⊢ (i · ((((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2)) + (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2)))) = (i · (2 · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2))))
73	5, 6	nvgcl 30713	. . . . . . . . . . . . . . 15 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐺𝐵) ∈ 𝑋)
74	2, 3, 52, 73	mp3an 1470	. . . . . . . . . . . . . 14 ⊢ (𝐴𝐺𝐵) ∈ 𝑋
75	5, 6	nvgcl 30713	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺𝐵) ∈ 𝑋 ∧ (i𝑆𝐶) ∈ 𝑋) → ((𝐴𝐺𝐵)𝐺(i𝑆𝐶)) ∈ 𝑋)
76	2, 74, 35, 75	mp3an 1470	. . . . . . . . . . . . 13 ⊢ ((𝐴𝐺𝐵)𝐺(i𝑆𝐶)) ∈ 𝑋
77	5, 8, 2, 76	nvcli 30755	. . . . . . . . . . . 12 ⊢ (𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶))) ∈ ℝ
78	77	resqcli 14143	. . . . . . . . . . 11 ⊢ ((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) ∈ ℝ
79	78	recni 11154	. . . . . . . . . 10 ⊢ ((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) ∈ ℂ
80	5, 6	nvgcl 30713	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺𝐵) ∈ 𝑋 ∧ (-i𝑆𝐶) ∈ 𝑋) → ((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)) ∈ 𝑋)
81	2, 74, 43, 80	mp3an 1470	. . . . . . . . . . . . 13 ⊢ ((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)) ∈ 𝑋
82	5, 8, 2, 81	nvcli 30755	. . . . . . . . . . . 12 ⊢ (𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶))) ∈ ℝ
83	82	resqcli 14143	. . . . . . . . . . 11 ⊢ ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2) ∈ ℝ
84	83	recni 11154	. . . . . . . . . 10 ⊢ ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2) ∈ ℂ
85	79, 84	subcli 11465	. . . . . . . . 9 ⊢ (((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2)) ∈ ℂ
86	5, 7	nvscl 30719	. . . . . . . . . . . . . . . 16 ⊢ ((𝑈 ∈ NrmCVec ∧ -1 ∈ ℂ ∧ 𝐵 ∈ 𝑋) → (-1𝑆𝐵) ∈ 𝑋)
87	2, 24, 52, 86	mp3an 1470	. . . . . . . . . . . . . . 15 ⊢ (-1𝑆𝐵) ∈ 𝑋
88	5, 6	nvgcl 30713	. . . . . . . . . . . . . . 15 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ (-1𝑆𝐵) ∈ 𝑋) → (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋)
89	2, 3, 87, 88	mp3an 1470	. . . . . . . . . . . . . 14 ⊢ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋
90	5, 6	nvgcl 30713	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋 ∧ (i𝑆𝐶) ∈ 𝑋) → ((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)) ∈ 𝑋)
91	2, 89, 35, 90	mp3an 1470	. . . . . . . . . . . . 13 ⊢ ((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)) ∈ 𝑋
92	5, 8, 2, 91	nvcli 30755	. . . . . . . . . . . 12 ⊢ (𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶))) ∈ ℝ
93	92	resqcli 14143	. . . . . . . . . . 11 ⊢ ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) ∈ ℝ
94	93	recni 11154	. . . . . . . . . 10 ⊢ ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) ∈ ℂ
95	5, 6	nvgcl 30713	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋 ∧ (-i𝑆𝐶) ∈ 𝑋) → ((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)) ∈ 𝑋)
96	2, 89, 43, 95	mp3an 1470	. . . . . . . . . . . . 13 ⊢ ((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)) ∈ 𝑋
97	5, 8, 2, 96	nvcli 30755	. . . . . . . . . . . 12 ⊢ (𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶))) ∈ ℝ
98	97	resqcli 14143	. . . . . . . . . . 11 ⊢ ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2) ∈ ℝ
99	98	recni 11154	. . . . . . . . . 10 ⊢ ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2) ∈ ℂ
100	94, 99	subcli 11465	. . . . . . . . 9 ⊢ (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2)) ∈ ℂ
101	33, 85, 100	adddii 11152	. . . . . . . 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 11336	. . . . . . . 8 ⊢ (i · (2 · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2)))) = (2 · (i · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2))))
103	72, 101, 102	3eqtr3i 2772	. . . . . . 7 ⊢ ((i · (((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2))) + (i · (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2)))) = (2 · (i · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2))))
104	70, 103	oveq12i 7372	. . . . . 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 2767	. . . . 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 30713	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺𝐵) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → ((𝐴𝐺𝐵)𝐺𝐶) ∈ 𝑋)
107	2, 74, 4, 106	mp3an 1470	. . . . . . . . . 10 ⊢ ((𝐴𝐺𝐵)𝐺𝐶) ∈ 𝑋
108	5, 8, 2, 107	nvcli 30755	. . . . . . . . 9 ⊢ (𝑁‘((𝐴𝐺𝐵)𝐺𝐶)) ∈ ℝ
109	108	resqcli 14143	. . . . . . . 8 ⊢ ((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) ∈ ℝ
110	109	recni 11154	. . . . . . 7 ⊢ ((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) ∈ ℂ
111	5, 6	nvgcl 30713	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺𝐵) ∈ 𝑋 ∧ (-1𝑆𝐶) ∈ 𝑋) → ((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)) ∈ 𝑋)
112	2, 74, 26, 111	mp3an 1470	. . . . . . . . . 10 ⊢ ((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)) ∈ 𝑋
113	5, 8, 2, 112	nvcli 30755	. . . . . . . . 9 ⊢ (𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶))) ∈ ℝ
114	113	resqcli 14143	. . . . . . . 8 ⊢ ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2) ∈ ℝ
115	114	recni 11154	. . . . . . 7 ⊢ ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2) ∈ ℂ
116	110, 115	subcli 11465	. . . . . 6 ⊢ (((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2)) ∈ ℂ
117	5, 6	nvgcl 30713	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → ((𝐴𝐺(-1𝑆𝐵))𝐺𝐶) ∈ 𝑋)
118	2, 89, 4, 117	mp3an 1470	. . . . . . . . . 10 ⊢ ((𝐴𝐺(-1𝑆𝐵))𝐺𝐶) ∈ 𝑋
119	5, 8, 2, 118	nvcli 30755	. . . . . . . . 9 ⊢ (𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶)) ∈ ℝ
120	119	resqcli 14143	. . . . . . . 8 ⊢ ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))↑2) ∈ ℝ
121	120	recni 11154	. . . . . . 7 ⊢ ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))↑2) ∈ ℂ
122	5, 6	nvgcl 30713	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋 ∧ (-1𝑆𝐶) ∈ 𝑋) → ((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)) ∈ 𝑋)
123	2, 89, 26, 122	mp3an 1470	. . . . . . . . . 10 ⊢ ((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)) ∈ 𝑋
124	5, 8, 2, 123	nvcli 30755	. . . . . . . . 9 ⊢ (𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶))) ∈ ℝ
125	124	resqcli 14143	. . . . . . . 8 ⊢ ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2) ∈ ℝ
126	125	recni 11154	. . . . . . 7 ⊢ ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2) ∈ ℂ
127	121, 126	subcli 11465	. . . . . 6 ⊢ (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2)) ∈ ℂ
128	33, 85	mulcli 11147	. . . . . 6 ⊢ (i · (((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2))) ∈ ℂ
129	33, 100	mulcli 11147	. . . . . 6 ⊢ (i · (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2))) ∈ ℂ
130	116, 127, 128, 129	add4i 11366	. . . . 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 30805	. . . . . . . 8 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺𝐵) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → ((𝐴𝐺𝐵)𝑃𝐶) ∈ ℂ)
132	2, 74, 4, 131	mp3an 1470	. . . . . . 7 ⊢ ((𝐴𝐺𝐵)𝑃𝐶) ∈ ℂ
133	5, 9	dipcl 30805	. . . . . . . 8 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶) ∈ ℂ)
134	2, 89, 4, 133	mp3an 1470	. . . . . . 7 ⊢ ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶) ∈ ℂ
135	14, 132, 134	adddii 11152	. . . . . 6 ⊢ (4 · (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶))) = ((4 · ((𝐴𝐺𝐵)𝑃𝐶)) + (4 · ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶)))
136	5, 6, 7, 8, 9	4ipval2 30801	. . . . . . . 8 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺𝐵) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (4 · ((𝐴𝐺𝐵)𝑃𝐶)) = ((((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2)))))
137	2, 74, 4, 136	mp3an 1470	. . . . . . 7 ⊢ (4 · ((𝐴𝐺𝐵)𝑃𝐶)) = ((((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2))))
138	5, 6, 7, 8, 9	4ipval2 30801	. . . . . . . 8 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (4 · ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶)) = ((((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2)))))
139	2, 89, 4, 138	mp3an 1470	. . . . . . 7 ⊢ (4 · ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶)) = ((((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2))))
140	137, 139	oveq12i 7372	. . . . . 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 2765	. . . . 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 2768	. . . 4 ⊢ (2 · ((((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2))))) = (4 · (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶)))
143	12, 17, 142	3eqtr3ri 2773	. . 3 ⊢ (4 · (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶))) = (4 · (2 · (𝐴𝑃𝐶)))
144	143	oveq1i 7370	. 2 ⊢ ((4 · (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶))) / 4) = ((4 · (2 · (𝐴𝑃𝐶))) / 4)
145	132, 134	addcli 11146	. . 3 ⊢ (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶)) ∈ ℂ
146		4ne0 12284	. . 3 ⊢ 4 ≠ 0
147	145, 14, 146	divcan3i 11896	. 2 ⊢ ((4 · (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶))) / 4) = (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶))
148	13, 16	mulcli 11147	. . 3 ⊢ (2 · (𝐴𝑃𝐶)) ∈ ℂ
149	148, 14, 146	divcan3i 11896	. 2 ⊢ ((4 · (2 · (𝐴𝑃𝐶))) / 4) = (2 · (𝐴𝑃𝐶))
150	144, 147, 149	3eqtr3i 2772	1 ⊢ (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶)) = (2 · (𝐴𝑃𝐶))

Colors of variables: wff setvar class

Syntax hints: = wceq 1548 ∈ wcel 2121 ‘cfv 6489 (class class class)co 7360 ℂcc 11031 1c1 11034 ici 11035 + caddc 11036 · cmul 11038 − cmin 11372 -cneg 11373 / cdiv 11802 2c2 12231 4c4 12233 ↑cexp 14018 NrmCVeccnv 30677 +_𝑣 cpv 30678 BaseSetcba 30679 ·_𝑠OLD cns 30680 norm_CVcnmcv 30683 ·_𝑖OLDcdip 30793 CPreHil_OLDccphlo 30905

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1975 ax-7 2016 ax-8 2123 ax-9 2131 ax-10 2154 ax-11 2170 ax-12 2191 ax-ext 2713 ax-rep 5202 ax-sep 5221 ax-nul 5231 ax-pow 5297 ax-pr 5365 ax-un 7682 ax-inf2 9557 ax-cnex 11089 ax-resscn 11090 ax-1cn 11091 ax-icn 11092 ax-addcl 11093 ax-addrcl 11094 ax-mulcl 11095 ax-mulrcl 11096 ax-mulcom 11097 ax-addass 11098 ax-mulass 11099 ax-distr 11100 ax-i2m1 11101 ax-1ne0 11102 ax-1rid 11103 ax-rnegex 11104 ax-rrecex 11105 ax-cnre 11106 ax-pre-lttri 11107 ax-pre-lttrn 11108 ax-pre-ltadd 11109 ax-pre-mulgt0 11110 ax-pre-sup 11111

This theorem depends on definitions: df-bi 209 df-an 398 df-or 855 df-3or 1094 df-3an 1095 df-tru 1551 df-fal 1561 df-ex 1788 df-nf 1792 df-sb 2075 df-mo 2545 df-eu 2575 df-clab 2720 df-cleq 2733 df-clel 2816 df-nfc 2890 df-ne 2937 df-nel 3041 df-ral 3056 df-rex 3066 df-rmo 3346 df-reu 3347 df-rab 3394 df-v 3435 df-sbc 3726 df-csb 3834 df-dif 3888 df-un 3890 df-in 3892 df-ss 3902 df-pss 3905 df-nul 4265 df-if 4458 df-pw 4534 df-sn 4559 df-pr 4561 df-op 4565 df-uni 4842 df-int 4881 df-iun 4926 df-br 5076 df-opab 5138 df-mpt 5157 df-tr 5183 df-id 5516 df-eprel 5521 df-po 5529 df-so 5530 df-fr 5574 df-se 5575 df-we 5576 df-xp 5627 df-rel 5628 df-cnv 5629 df-co 5630 df-dm 5631 df-rn 5632 df-res 5633 df-ima 5634 df-pred 6256 df-ord 6317 df-on 6318 df-lim 6319 df-suc 6320 df-iota 6445 df-fun 6491 df-fn 6492 df-f 6493 df-f1 6494 df-fo 6495 df-f1o 6496 df-fv 6497 df-isom 6498 df-riota 7317 df-ov 7363 df-oprab 7364 df-mpo 7365 df-om 7811 df-1st 7935 df-2nd 7936 df-frecs 8225 df-wrecs 8256 df-recs 8305 df-rdg 8343 df-1o 8399 df-er 8637 df-en 8888 df-dom 8889 df-sdom 8890 df-fin 8891 df-sup 9349 df-oi 9419 df-card 9858 df-pnf 11176 df-mnf 11177 df-xr 11178 df-ltxr 11179 df-le 11180 df-sub 11374 df-neg 11375 df-div 11803 df-nn 12170 df-2 12239 df-3 12240 df-4 12241 df-n0 12433 df-z 12520 df-uz 12784 df-rp 12938 df-fz 13457 df-fzo 13604 df-seq 13959 df-exp 14019 df-hash 14288 df-cj 15056 df-re 15057 df-im 15058 df-sqrt 15192 df-abs 15193 df-clim 15445 df-sum 15644 df-grpo 30586 df-ablo 30638 df-vc 30652 df-nv 30685 df-va 30688 df-ba 30689 df-sm 30690 df-0v 30691 df-nmcv 30693 df-dip 30794 df-ph 30906

This theorem is referenced by: ip1i 30920

W3C validator