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 30858

Description: Lemma for ip1i 30859. (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 30848	. . . . . 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 30740	. . . . . 6 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (4 · (𝐴𝑃𝐶)) = ((((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2)))))
11	2, 3, 4, 10	mp3an 1461	. . . . 5 ⊢ (4 · (𝐴𝑃𝐶)) = ((((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2))))
12	11	oveq2i 7459	. . . 4 ⊢ (2 · (4 · (𝐴𝑃𝐶))) = (2 · ((((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2)))))
13		2cn 12368	. . . . 5 ⊢ 2 ∈ ℂ
14		4cn 12378	. . . . 5 ⊢ 4 ∈ ℂ
15	5, 9	dipcl 30744	. . . . . 6 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (𝐴𝑃𝐶) ∈ ℂ)
16	2, 3, 4, 15	mp3an 1461	. . . . 5 ⊢ (𝐴𝑃𝐶) ∈ ℂ
17	13, 14, 16	mul12i 11485	. . . 4 ⊢ (2 · (4 · (𝐴𝑃𝐶))) = (4 · (2 · (𝐴𝑃𝐶)))
18	5, 6	nvgcl 30652	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (𝐴𝐺𝐶) ∈ 𝑋)
19	2, 3, 4, 18	mp3an 1461	. . . . . . . . . . 11 ⊢ (𝐴𝐺𝐶) ∈ 𝑋
20	5, 8, 2, 19	nvcli 30694	. . . . . . . . . 10 ⊢ (𝑁‘(𝐴𝐺𝐶)) ∈ ℝ
21	20	resqcli 14235	. . . . . . . . 9 ⊢ ((𝑁‘(𝐴𝐺𝐶))↑2) ∈ ℝ
22	21	recni 11304	. . . . . . . 8 ⊢ ((𝑁‘(𝐴𝐺𝐶))↑2) ∈ ℂ
23		ax-1cn 11242	. . . . . . . . . . . . . 14 ⊢ 1 ∈ ℂ
24	23	negcli 11604	. . . . . . . . . . . . 13 ⊢ -1 ∈ ℂ
25	5, 7	nvscl 30658	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ NrmCVec ∧ -1 ∈ ℂ ∧ 𝐶 ∈ 𝑋) → (-1𝑆𝐶) ∈ 𝑋)
26	2, 24, 4, 25	mp3an 1461	. . . . . . . . . . . 12 ⊢ (-1𝑆𝐶) ∈ 𝑋
27	5, 6	nvgcl 30652	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ (-1𝑆𝐶) ∈ 𝑋) → (𝐴𝐺(-1𝑆𝐶)) ∈ 𝑋)
28	2, 3, 26, 27	mp3an 1461	. . . . . . . . . . 11 ⊢ (𝐴𝐺(-1𝑆𝐶)) ∈ 𝑋
29	5, 8, 2, 28	nvcli 30694	. . . . . . . . . 10 ⊢ (𝑁‘(𝐴𝐺(-1𝑆𝐶))) ∈ ℝ
30	29	resqcli 14235	. . . . . . . . 9 ⊢ ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2) ∈ ℝ
31	30	recni 11304	. . . . . . . 8 ⊢ ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2) ∈ ℂ
32	22, 31	subcli 11612	. . . . . . 7 ⊢ (((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2)) ∈ ℂ
33		ax-icn 11243	. . . . . . . 8 ⊢ i ∈ ℂ
34	5, 7	nvscl 30658	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ i ∈ ℂ ∧ 𝐶 ∈ 𝑋) → (i𝑆𝐶) ∈ 𝑋)
35	2, 33, 4, 34	mp3an 1461	. . . . . . . . . . . . 13 ⊢ (i𝑆𝐶) ∈ 𝑋
36	5, 6	nvgcl 30652	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ (i𝑆𝐶) ∈ 𝑋) → (𝐴𝐺(i𝑆𝐶)) ∈ 𝑋)
37	2, 3, 35, 36	mp3an 1461	. . . . . . . . . . . 12 ⊢ (𝐴𝐺(i𝑆𝐶)) ∈ 𝑋
38	5, 8, 2, 37	nvcli 30694	. . . . . . . . . . 11 ⊢ (𝑁‘(𝐴𝐺(i𝑆𝐶))) ∈ ℝ
39	38	resqcli 14235	. . . . . . . . . 10 ⊢ ((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) ∈ ℝ
40	39	recni 11304	. . . . . . . . 9 ⊢ ((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) ∈ ℂ
41	33	negcli 11604	. . . . . . . . . . . . . 14 ⊢ -i ∈ ℂ
42	5, 7	nvscl 30658	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ -i ∈ ℂ ∧ 𝐶 ∈ 𝑋) → (-i𝑆𝐶) ∈ 𝑋)
43	2, 41, 4, 42	mp3an 1461	. . . . . . . . . . . . 13 ⊢ (-i𝑆𝐶) ∈ 𝑋
44	5, 6	nvgcl 30652	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ (-i𝑆𝐶) ∈ 𝑋) → (𝐴𝐺(-i𝑆𝐶)) ∈ 𝑋)
45	2, 3, 43, 44	mp3an 1461	. . . . . . . . . . . 12 ⊢ (𝐴𝐺(-i𝑆𝐶)) ∈ 𝑋
46	5, 8, 2, 45	nvcli 30694	. . . . . . . . . . 11 ⊢ (𝑁‘(𝐴𝐺(-i𝑆𝐶))) ∈ ℝ
47	46	resqcli 14235	. . . . . . . . . 10 ⊢ ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2) ∈ ℝ
48	47	recni 11304	. . . . . . . . 9 ⊢ ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2) ∈ ℂ
49	40, 48	subcli 11612	. . . . . . . 8 ⊢ (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2)) ∈ ℂ
50	33, 49	mulcli 11297	. . . . . . 7 ⊢ (i · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2))) ∈ ℂ
51	13, 32, 50	adddii 11302	. . . . . 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 30857	. . . . . . . 8 ⊢ ((((𝑁‘((𝐴𝐺𝐵)𝐺(1𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2)) + (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(1𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2))) = (2 · (((𝑁‘(𝐴𝐺(1𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2)))
54	5, 7	nvsid 30659	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐶 ∈ 𝑋) → (1𝑆𝐶) = 𝐶)
55	2, 4, 54	mp2an 691	. . . . . . . . . . . . 13 ⊢ (1𝑆𝐶) = 𝐶
56	55	oveq2i 7459	. . . . . . . . . . . 12 ⊢ ((𝐴𝐺𝐵)𝐺(1𝑆𝐶)) = ((𝐴𝐺𝐵)𝐺𝐶)
57	56	fveq2i 6923	. . . . . . . . . . 11 ⊢ (𝑁‘((𝐴𝐺𝐵)𝐺(1𝑆𝐶))) = (𝑁‘((𝐴𝐺𝐵)𝐺𝐶))
58	57	oveq1i 7458	. . . . . . . . . 10 ⊢ ((𝑁‘((𝐴𝐺𝐵)𝐺(1𝑆𝐶)))↑2) = ((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2)
59	58	oveq1i 7458	. . . . . . . . 9 ⊢ (((𝑁‘((𝐴𝐺𝐵)𝐺(1𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2)) = (((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2))
60	55	oveq2i 7459	. . . . . . . . . . . 12 ⊢ ((𝐴𝐺(-1𝑆𝐵))𝐺(1𝑆𝐶)) = ((𝐴𝐺(-1𝑆𝐵))𝐺𝐶)
61	60	fveq2i 6923	. . . . . . . . . . 11 ⊢ (𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(1𝑆𝐶))) = (𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))
62	61	oveq1i 7458	. . . . . . . . . 10 ⊢ ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(1𝑆𝐶)))↑2) = ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))↑2)
63	62	oveq1i 7458	. . . . . . . . 9 ⊢ (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(1𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2)) = (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2))
64	59, 63	oveq12i 7460	. . . . . . . 8 ⊢ ((((𝑁‘((𝐴𝐺𝐵)𝐺(1𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2)) + (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(1𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2))) = ((((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2)) + (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2)))
65	55	oveq2i 7459	. . . . . . . . . . . 12 ⊢ (𝐴𝐺(1𝑆𝐶)) = (𝐴𝐺𝐶)
66	65	fveq2i 6923	. . . . . . . . . . 11 ⊢ (𝑁‘(𝐴𝐺(1𝑆𝐶))) = (𝑁‘(𝐴𝐺𝐶))
67	66	oveq1i 7458	. . . . . . . . . 10 ⊢ ((𝑁‘(𝐴𝐺(1𝑆𝐶)))↑2) = ((𝑁‘(𝐴𝐺𝐶))↑2)
68	67	oveq1i 7458	. . . . . . . . 9 ⊢ (((𝑁‘(𝐴𝐺(1𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2)) = (((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2))
69	68	oveq2i 7459	. . . . . . . 8 ⊢ (2 · (((𝑁‘(𝐴𝐺(1𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2))) = (2 · (((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2)))
70	53, 64, 69	3eqtr3i 2776	. . . . . . 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 30857	. . . . . . . . 9 ⊢ ((((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2)) + (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2))) = (2 · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2)))
72	71	oveq2i 7459	. . . . . . . 8 ⊢ (i · ((((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2)) + (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2)))) = (i · (2 · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2))))
73	5, 6	nvgcl 30652	. . . . . . . . . . . . . . 15 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐺𝐵) ∈ 𝑋)
74	2, 3, 52, 73	mp3an 1461	. . . . . . . . . . . . . 14 ⊢ (𝐴𝐺𝐵) ∈ 𝑋
75	5, 6	nvgcl 30652	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺𝐵) ∈ 𝑋 ∧ (i𝑆𝐶) ∈ 𝑋) → ((𝐴𝐺𝐵)𝐺(i𝑆𝐶)) ∈ 𝑋)
76	2, 74, 35, 75	mp3an 1461	. . . . . . . . . . . . 13 ⊢ ((𝐴𝐺𝐵)𝐺(i𝑆𝐶)) ∈ 𝑋
77	5, 8, 2, 76	nvcli 30694	. . . . . . . . . . . 12 ⊢ (𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶))) ∈ ℝ
78	77	resqcli 14235	. . . . . . . . . . 11 ⊢ ((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) ∈ ℝ
79	78	recni 11304	. . . . . . . . . 10 ⊢ ((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) ∈ ℂ
80	5, 6	nvgcl 30652	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺𝐵) ∈ 𝑋 ∧ (-i𝑆𝐶) ∈ 𝑋) → ((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)) ∈ 𝑋)
81	2, 74, 43, 80	mp3an 1461	. . . . . . . . . . . . 13 ⊢ ((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)) ∈ 𝑋
82	5, 8, 2, 81	nvcli 30694	. . . . . . . . . . . 12 ⊢ (𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶))) ∈ ℝ
83	82	resqcli 14235	. . . . . . . . . . 11 ⊢ ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2) ∈ ℝ
84	83	recni 11304	. . . . . . . . . 10 ⊢ ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2) ∈ ℂ
85	79, 84	subcli 11612	. . . . . . . . 9 ⊢ (((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2)) ∈ ℂ
86	5, 7	nvscl 30658	. . . . . . . . . . . . . . . 16 ⊢ ((𝑈 ∈ NrmCVec ∧ -1 ∈ ℂ ∧ 𝐵 ∈ 𝑋) → (-1𝑆𝐵) ∈ 𝑋)
87	2, 24, 52, 86	mp3an 1461	. . . . . . . . . . . . . . 15 ⊢ (-1𝑆𝐵) ∈ 𝑋
88	5, 6	nvgcl 30652	. . . . . . . . . . . . . . 15 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ (-1𝑆𝐵) ∈ 𝑋) → (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋)
89	2, 3, 87, 88	mp3an 1461	. . . . . . . . . . . . . 14 ⊢ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋
90	5, 6	nvgcl 30652	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋 ∧ (i𝑆𝐶) ∈ 𝑋) → ((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)) ∈ 𝑋)
91	2, 89, 35, 90	mp3an 1461	. . . . . . . . . . . . 13 ⊢ ((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)) ∈ 𝑋
92	5, 8, 2, 91	nvcli 30694	. . . . . . . . . . . 12 ⊢ (𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶))) ∈ ℝ
93	92	resqcli 14235	. . . . . . . . . . 11 ⊢ ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) ∈ ℝ
94	93	recni 11304	. . . . . . . . . 10 ⊢ ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) ∈ ℂ
95	5, 6	nvgcl 30652	. . . . . . . . . . . . . 14 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋 ∧ (-i𝑆𝐶) ∈ 𝑋) → ((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)) ∈ 𝑋)
96	2, 89, 43, 95	mp3an 1461	. . . . . . . . . . . . 13 ⊢ ((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)) ∈ 𝑋
97	5, 8, 2, 96	nvcli 30694	. . . . . . . . . . . 12 ⊢ (𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶))) ∈ ℝ
98	97	resqcli 14235	. . . . . . . . . . 11 ⊢ ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2) ∈ ℝ
99	98	recni 11304	. . . . . . . . . 10 ⊢ ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2) ∈ ℂ
100	94, 99	subcli 11612	. . . . . . . . 9 ⊢ (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2)) ∈ ℂ
101	33, 85, 100	adddii 11302	. . . . . . . 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 11485	. . . . . . . 8 ⊢ (i · (2 · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2)))) = (2 · (i · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2))))
103	72, 101, 102	3eqtr3i 2776	. . . . . . 7 ⊢ ((i · (((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2))) + (i · (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2)))) = (2 · (i · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2))))
104	70, 103	oveq12i 7460	. . . . . 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 2771	. . . . 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 30652	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺𝐵) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → ((𝐴𝐺𝐵)𝐺𝐶) ∈ 𝑋)
107	2, 74, 4, 106	mp3an 1461	. . . . . . . . . 10 ⊢ ((𝐴𝐺𝐵)𝐺𝐶) ∈ 𝑋
108	5, 8, 2, 107	nvcli 30694	. . . . . . . . 9 ⊢ (𝑁‘((𝐴𝐺𝐵)𝐺𝐶)) ∈ ℝ
109	108	resqcli 14235	. . . . . . . 8 ⊢ ((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) ∈ ℝ
110	109	recni 11304	. . . . . . 7 ⊢ ((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) ∈ ℂ
111	5, 6	nvgcl 30652	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺𝐵) ∈ 𝑋 ∧ (-1𝑆𝐶) ∈ 𝑋) → ((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)) ∈ 𝑋)
112	2, 74, 26, 111	mp3an 1461	. . . . . . . . . 10 ⊢ ((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)) ∈ 𝑋
113	5, 8, 2, 112	nvcli 30694	. . . . . . . . 9 ⊢ (𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶))) ∈ ℝ
114	113	resqcli 14235	. . . . . . . 8 ⊢ ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2) ∈ ℝ
115	114	recni 11304	. . . . . . 7 ⊢ ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2) ∈ ℂ
116	110, 115	subcli 11612	. . . . . 6 ⊢ (((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2)) ∈ ℂ
117	5, 6	nvgcl 30652	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → ((𝐴𝐺(-1𝑆𝐵))𝐺𝐶) ∈ 𝑋)
118	2, 89, 4, 117	mp3an 1461	. . . . . . . . . 10 ⊢ ((𝐴𝐺(-1𝑆𝐵))𝐺𝐶) ∈ 𝑋
119	5, 8, 2, 118	nvcli 30694	. . . . . . . . 9 ⊢ (𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶)) ∈ ℝ
120	119	resqcli 14235	. . . . . . . 8 ⊢ ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))↑2) ∈ ℝ
121	120	recni 11304	. . . . . . 7 ⊢ ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))↑2) ∈ ℂ
122	5, 6	nvgcl 30652	. . . . . . . . . . 11 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋 ∧ (-1𝑆𝐶) ∈ 𝑋) → ((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)) ∈ 𝑋)
123	2, 89, 26, 122	mp3an 1461	. . . . . . . . . 10 ⊢ ((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)) ∈ 𝑋
124	5, 8, 2, 123	nvcli 30694	. . . . . . . . 9 ⊢ (𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶))) ∈ ℝ
125	124	resqcli 14235	. . . . . . . 8 ⊢ ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2) ∈ ℝ
126	125	recni 11304	. . . . . . 7 ⊢ ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2) ∈ ℂ
127	121, 126	subcli 11612	. . . . . 6 ⊢ (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2)) ∈ ℂ
128	33, 85	mulcli 11297	. . . . . 6 ⊢ (i · (((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2))) ∈ ℂ
129	33, 100	mulcli 11297	. . . . . 6 ⊢ (i · (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2))) ∈ ℂ
130	116, 127, 128, 129	add4i 11514	. . . . 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 30744	. . . . . . . 8 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺𝐵) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → ((𝐴𝐺𝐵)𝑃𝐶) ∈ ℂ)
132	2, 74, 4, 131	mp3an 1461	. . . . . . 7 ⊢ ((𝐴𝐺𝐵)𝑃𝐶) ∈ ℂ
133	5, 9	dipcl 30744	. . . . . . . 8 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶) ∈ ℂ)
134	2, 89, 4, 133	mp3an 1461	. . . . . . 7 ⊢ ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶) ∈ ℂ
135	14, 132, 134	adddii 11302	. . . . . 6 ⊢ (4 · (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶))) = ((4 · ((𝐴𝐺𝐵)𝑃𝐶)) + (4 · ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶)))
136	5, 6, 7, 8, 9	4ipval2 30740	. . . . . . . 8 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺𝐵) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (4 · ((𝐴𝐺𝐵)𝑃𝐶)) = ((((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2)))))
137	2, 74, 4, 136	mp3an 1461	. . . . . . 7 ⊢ (4 · ((𝐴𝐺𝐵)𝑃𝐶)) = ((((𝑁‘((𝐴𝐺𝐵)𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘((𝐴𝐺𝐵)𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-i𝑆𝐶)))↑2))))
138	5, 6, 7, 8, 9	4ipval2 30740	. . . . . . . 8 ⊢ ((𝑈 ∈ NrmCVec ∧ (𝐴𝐺(-1𝑆𝐵)) ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → (4 · ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶)) = ((((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2)))))
139	2, 89, 4, 138	mp3an 1461	. . . . . . 7 ⊢ (4 · ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶)) = ((((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺𝐶))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(i𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-i𝑆𝐶)))↑2))))
140	137, 139	oveq12i 7460	. . . . . 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 2769	. . . . 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 2772	. . . 4 ⊢ (2 · ((((𝑁‘(𝐴𝐺𝐶))↑2) − ((𝑁‘(𝐴𝐺(-1𝑆𝐶)))↑2)) + (i · (((𝑁‘(𝐴𝐺(i𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-i𝑆𝐶)))↑2))))) = (4 · (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶)))
143	12, 17, 142	3eqtr3ri 2777	. . 3 ⊢ (4 · (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶))) = (4 · (2 · (𝐴𝑃𝐶)))
144	143	oveq1i 7458	. 2 ⊢ ((4 · (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶))) / 4) = ((4 · (2 · (𝐴𝑃𝐶))) / 4)
145	132, 134	addcli 11296	. . 3 ⊢ (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶)) ∈ ℂ
146		4ne0 12401	. . 3 ⊢ 4 ≠ 0
147	145, 14, 146	divcan3i 12040	. 2 ⊢ ((4 · (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶))) / 4) = (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶))
148	13, 16	mulcli 11297	. . 3 ⊢ (2 · (𝐴𝑃𝐶)) ∈ ℂ
149	148, 14, 146	divcan3i 12040	. 2 ⊢ ((4 · (2 · (𝐴𝑃𝐶))) / 4) = (2 · (𝐴𝑃𝐶))
150	144, 147, 149	3eqtr3i 2776	1 ⊢ (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶)) = (2 · (𝐴𝑃𝐶))

Colors of variables: wff setvar class

Syntax hints: = wceq 1537 ∈ wcel 2108 ‘cfv 6573 (class class class)co 7448 ℂcc 11182 1c1 11185 ici 11186 + caddc 11187 · cmul 11189 − cmin 11520 -cneg 11521 / cdiv 11947 2c2 12348 4c4 12350 ↑cexp 14112 NrmCVeccnv 30616 +_𝑣 cpv 30617 BaseSetcba 30618 ·_𝑠OLD cns 30619 norm_CVcnmcv 30622 ·_𝑖OLDcdip 30732 CPreHil_OLDccphlo 30844

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2158 ax-12 2178 ax-ext 2711 ax-rep 5303 ax-sep 5317 ax-nul 5324 ax-pow 5383 ax-pr 5447 ax-un 7770 ax-inf2 9710 ax-cnex 11240 ax-resscn 11241 ax-1cn 11242 ax-icn 11243 ax-addcl 11244 ax-addrcl 11245 ax-mulcl 11246 ax-mulrcl 11247 ax-mulcom 11248 ax-addass 11249 ax-mulass 11250 ax-distr 11251 ax-i2m1 11252 ax-1ne0 11253 ax-1rid 11254 ax-rnegex 11255 ax-rrecex 11256 ax-cnre 11257 ax-pre-lttri 11258 ax-pre-lttrn 11259 ax-pre-ltadd 11260 ax-pre-mulgt0 11261 ax-pre-sup 11262

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3or 1088 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-nfc 2895 df-ne 2947 df-nel 3053 df-ral 3068 df-rex 3077 df-rmo 3388 df-reu 3389 df-rab 3444 df-v 3490 df-sbc 3805 df-csb 3922 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-pss 3996 df-nul 4353 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-op 4655 df-uni 4932 df-int 4971 df-iun 5017 df-br 5167 df-opab 5229 df-mpt 5250 df-tr 5284 df-id 5593 df-eprel 5599 df-po 5607 df-so 5608 df-fr 5652 df-se 5653 df-we 5654 df-xp 5706 df-rel 5707 df-cnv 5708 df-co 5709 df-dm 5710 df-rn 5711 df-res 5712 df-ima 5713 df-pred 6332 df-ord 6398 df-on 6399 df-lim 6400 df-suc 6401 df-iota 6525 df-fun 6575 df-fn 6576 df-f 6577 df-f1 6578 df-fo 6579 df-f1o 6580 df-fv 6581 df-isom 6582 df-riota 7404 df-ov 7451 df-oprab 7452 df-mpo 7453 df-om 7904 df-1st 8030 df-2nd 8031 df-frecs 8322 df-wrecs 8353 df-recs 8427 df-rdg 8466 df-1o 8522 df-er 8763 df-en 9004 df-dom 9005 df-sdom 9006 df-fin 9007 df-sup 9511 df-oi 9579 df-card 10008 df-pnf 11326 df-mnf 11327 df-xr 11328 df-ltxr 11329 df-le 11330 df-sub 11522 df-neg 11523 df-div 11948 df-nn 12294 df-2 12356 df-3 12357 df-4 12358 df-n0 12554 df-z 12640 df-uz 12904 df-rp 13058 df-fz 13568 df-fzo 13712 df-seq 14053 df-exp 14113 df-hash 14380 df-cj 15148 df-re 15149 df-im 15150 df-sqrt 15284 df-abs 15285 df-clim 15534 df-sum 15735 df-grpo 30525 df-ablo 30577 df-vc 30591 df-nv 30624 df-va 30627 df-ba 30628 df-sm 30629 df-0v 30630 df-nmcv 30632 df-dip 30733 df-ph 30845

This theorem is referenced by: ip1i 30859

W3C validator