Hilbert Space Explorer

Hilbert Space Explorer

< Previous Next >
Related theorems
GIF version

Theorem pjclem4 5653

Description: Lemma for projection commutation theorem.

**Hypotheses**
Ref	Expression
pjclem1.1	⊢ G ∈ C_ℋ
pjclem1.2	⊢ H ∈ C_ℋ

**Assertion**
Ref	Expression
pjclem4	⊢ (((Proj ‘G) ∘ (Proj ‘H)) = ((Proj ‘H) ∘ (Proj ‘G)) → ((Proj ‘G) ∘ (Proj ‘H)) = (Proj ‘(G ∩ H)))

**Proof of Theorem pjclem4**
Step	Hyp	Ref	Expression
1		pjclem1.1	. . . . . . . 8 ⊢ G ∈ C_ℋ
2		pjclem1.2	. . . . . . . 8 ⊢ H ∈ C_ℋ
3	1, 2	chincl 5382	. . . . . . 7 ⊢ (G ∩ H) ∈ C_ℋ
4	3	pjv 5589	. . . . . 6 ⊢ (((((Proj ‘G) ∘ (Proj ‘H)) ‘x) ∈ (G ∩ H) ∧ (x −_v (((Proj ‘G) ∘ (Proj ‘H)) ‘x)) ∈ (⊥ ‘(G ∩ H))) → ((Proj ‘(G ∩ H)) ‘((((Proj ‘G) ∘ (Proj ‘H)) ‘x) +_v (x −_v (((Proj ‘G) ∘ (Proj ‘H)) ‘x)))) = (((Proj ‘G) ∘ (Proj ‘H)) ‘x))
5	1, 2	pjcocl 5629	. . . . . . . . 9 ⊢ (x ∈ ℋ → (((Proj ‘G) ∘ (Proj ‘H)) ‘x) ∈ G)
6	5	adantl 305	. . . . . . . 8 ⊢ ((((Proj ‘G) ∘ (Proj ‘H)) = ((Proj ‘H) ∘ (Proj ‘G)) ∧ x ∈ ℋ ) → (((Proj ‘G) ∘ (Proj ‘H)) ‘x) ∈ G)
7		fveq1 2831	. . . . . . . . . . 11 ⊢ (((Proj ‘G) ∘ (Proj ‘H)) = ((Proj ‘H) ∘ (Proj ‘G)) → (((Proj ‘G) ∘ (Proj ‘H)) ‘x) = (((Proj ‘H) ∘ (Proj ‘G)) ‘x))
8	7	eleq1d 1155	. . . . . . . . . 10 ⊢ (((Proj ‘G) ∘ (Proj ‘H)) = ((Proj ‘H) ∘ (Proj ‘G)) → ((((Proj ‘G) ∘ (Proj ‘H)) ‘x) ∈ H ↔ (((Proj ‘H) ∘ (Proj ‘G)) ‘x) ∈ H))
9	2, 1	pjcocl 5629	. . . . . . . . . 10 ⊢ (x ∈ ℋ → (((Proj ‘H) ∘ (Proj ‘G)) ‘x) ∈ H)
10	8, 9	syl5bir 184	. . . . . . . . 9 ⊢ (((Proj ‘G) ∘ (Proj ‘H)) = ((Proj ‘H) ∘ (Proj ‘G)) → (x ∈ ℋ → (((Proj ‘G) ∘ (Proj ‘H)) ‘x) ∈ H))
11	10	imp 277	. . . . . . . 8 ⊢ ((((Proj ‘G) ∘ (Proj ‘H)) = ((Proj ‘H) ∘ (Proj ‘G)) ∧ x ∈ ℋ ) → (((Proj ‘G) ∘ (Proj ‘H)) ‘x) ∈ H)
12	6, 11	jca 236	. . . . . . 7 ⊢ ((((Proj ‘G) ∘ (Proj ‘H)) = ((Proj ‘H) ∘ (Proj ‘G)) ∧ x ∈ ℋ ) → ((((Proj ‘G) ∘ (Proj ‘H)) ‘x) ∈ G ∧ (((Proj ‘G) ∘ (Proj ‘H)) ‘x) ∈ H))
13		elin 1635	. . . . . . 7 ⊢ ((((Proj ‘G) ∘ (Proj ‘H)) ‘x) ∈ (G ∩ H) ↔ ((((Proj ‘G) ∘ (Proj ‘H)) ‘x) ∈ G ∧ (((Proj ‘G) ∘ (Proj ‘H)) ‘x) ∈ H))
14	12, 13	sylibr 175	. . . . . 6 ⊢ ((((Proj ‘G) ∘ (Proj ‘H)) = ((Proj ‘H) ∘ (Proj ‘G)) ∧ x ∈ ℋ ) → (((Proj ‘G) ∘ (Proj ‘H)) ‘x) ∈ (G ∩ H))
15	1, 2	pjcohcl 5630	. . . . . . . . . 10 ⊢ (x ∈ ℋ → (((Proj ‘G) ∘ (Proj ‘H)) ‘x) ∈ ℋ )
16		hvsubclt 4998	. . . . . . . . . 10 ⊢ ((x ∈ ℋ ∧ (((Proj ‘G) ∘ (Proj ‘H)) ‘x) ∈ ℋ ) → (x −_v (((Proj ‘G) ∘ (Proj ‘H)) ‘x)) ∈ ℋ )
17	15, 16	mpdan 527	. . . . . . . . 9 ⊢ (x ∈ ℋ → (x −_v (((Proj ‘G) ∘ (Proj ‘H)) ‘x)) ∈ ℋ )
18	17	adantl 305	. . . . . . . 8 ⊢ ((((Proj ‘G) ∘ (Proj ‘H)) = ((Proj ‘H) ∘ (Proj ‘G)) ∧ x ∈ ℋ ) → (x −_v (((Proj ‘G) ∘ (Proj ‘H)) ‘x)) ∈ ℋ )
19		pm3.26 256	. . . . . . . . . . . . . . 15 ⊢ ((x ∈ ℋ ∧ y ∈ (G ∩ H)) → x ∈ ℋ )
20	15	adantr 306	. . . . . . . . . . . . . . 15 ⊢ ((x ∈ ℋ ∧ y ∈ (G ∩ H)) → (((Proj ‘G) ∘ (Proj ‘H)) ‘x) ∈ ℋ )
21	3	chel 5137	. . . . . . . . . . . . . . . 16 ⊢ (y ∈ (G ∩ H) → y ∈ ℋ )
22	21	adantl 305	. . . . . . . . . . . . . . 15 ⊢ ((x ∈ ℋ ∧ y ∈ (G ∩ H)) → y ∈ ℋ )
23	19, 20, 22	3jca 604	. . . . . . . . . . . . . 14 ⊢ ((x ∈ ℋ ∧ y ∈ (G ∩ H)) → (x ∈ ℋ ∧ (((Proj ‘G) ∘ (Proj ‘H)) ‘x) ∈ ℋ ∧ y ∈ ℋ ))
24	23	adantl 305	. . . . . . . . . . . . 13 ⊢ ((((Proj ‘G) ∘ (Proj ‘H)) = ((Proj ‘H) ∘ (Proj ‘G)) ∧ (x ∈ ℋ ∧ y ∈ (G ∩ H))) → (x ∈ ℋ ∧ (((Proj ‘G) ∘ (Proj ‘H)) ‘x) ∈ ℋ ∧ y ∈ ℋ ))
25		his2subt 5052	. . . . . . . . . . . . 13 ⊢ ((x ∈ ℋ ∧ (((Proj ‘G) ∘ (Proj ‘H)) ‘x) ∈ ℋ ∧ y ∈ ℋ ) → ((x −_v (((Proj ‘G) ∘ (Proj ‘H)) ‘x)) ·_i y) = ((x ·_i y) − ((((Proj ‘G) ∘ (Proj ‘H)) ‘x) ·_i y)))
26	24, 25	syl 12	. . . . . . . . . . . 12 ⊢ ((((Proj ‘G) ∘ (Proj ‘H)) = ((Proj ‘H) ∘ (Proj ‘G)) ∧ (x ∈ ℋ ∧ y ∈ (G ∩ H))) → ((x −_v (((Proj ‘G) ∘ (Proj ‘H)) ‘x)) ·_i y) = ((x ·_i y) − ((((Proj ‘G) ∘ (Proj ‘H)) ‘x) ·_i y)))
27	7	opreq1d 3012	. . . . . . . . . . . . . . 15 ⊢ (((Proj ‘G) ∘ (Proj ‘H)) = ((Proj ‘H) ∘ (Proj ‘G)) → ((((Proj ‘G) ∘ (Proj ‘H)) ‘x) ·_i y) = ((((Proj ‘H) ∘ (Proj ‘G)) ‘x) ·_i y))
28	2, 1	pjadjco 5631	. . . . . . . . . . . . . . . . 17 ⊢ ((x ∈ ℋ ∧ y ∈ ℋ ) → ((((Proj ‘H) ∘ (Proj ‘G)) ‘x) ·_i y) = (x ·_i (((Proj ‘G) ∘ (Proj ‘H)) ‘y)))
29	28, 21	sylan2 346	. . . . . . . . . . . . . . . 16 ⊢ ((x ∈ ℋ ∧ y ∈ (G ∩ H)) → ((((Proj ‘H) ∘ (Proj ‘G)) ‘x) ·_i y) = (x ·_i (((Proj ‘G) ∘ (Proj ‘H)) ‘y)))
30	1, 2	pjclem4a 5652	. . . . . . . . . . . . . . . . . 18 ⊢ (y ∈ (G ∩ H) → (((Proj ‘G) ∘ (Proj ‘H)) ‘y) = y)
31	30	opreq2d 3013	. . . . . . . . . . . . . . . . 17 ⊢ (y ∈ (G ∩ H) → (x ·_i (((Proj ‘G) ∘ (Proj ‘H)) ‘y)) = (x ·_i y))
32	31	adantl 305	. . . . . . . . . . . . . . . 16 ⊢ ((x ∈ ℋ ∧ y ∈ (G ∩ H)) → (x ·_i (((Proj ‘G) ∘ (Proj ‘H)) ‘y)) = (x ·_i y))
33	29, 32	eqtrd 1128	. . . . . . . . . . . . . . 15 ⊢ ((x ∈ ℋ ∧ y ∈ (G ∩ H)) → ((((Proj ‘H) ∘ (Proj ‘G)) ‘x) ·_i y) = (x ·_i y))
34	27, 33	sylan9eq 1144	. . . . . . . . . . . . . 14 ⊢ ((((Proj ‘G) ∘ (Proj ‘H)) = ((Proj ‘H) ∘ (Proj ‘G)) ∧ (x ∈ ℋ ∧ y ∈ (G ∩ H))) → ((((Proj ‘G) ∘ (Proj ‘H)) ‘x) ·_i y) = (x ·_i y))
35	34	opreq1d 3012	. . . . . . . . . . . . 13 ⊢ ((((Proj ‘G) ∘ (Proj ‘H)) = ((Proj ‘H) ∘ (Proj ‘G)) ∧ (x ∈ ℋ ∧ y ∈ (G ∩ H))) → (((((Proj ‘G) ∘ (Proj ‘H)) ‘x) ·_i y) − ((((Proj ‘G) ∘ (Proj ‘H)) ‘x) ·_i y)) = ((x ·_i y) − ((((Proj ‘G) ∘ (Proj ‘H)) ‘x) ·_i y)))
36	15, 21	anim12i 268	. . . . . . . . . . . . . . 15 ⊢ ((x ∈ ℋ ∧ y ∈ (G ∩ H)) → ((((Proj ‘G) ∘ (Proj ‘H)) ‘x) ∈ ℋ ∧ y ∈ ℋ ))
37	36	adantl 305	. . . . . . . . . . . . . 14 ⊢ ((((Proj ‘G) ∘ (Proj ‘H)) = ((Proj ‘H) ∘ (Proj ‘G)) ∧ (x ∈ ℋ ∧ y ∈ (G ∩ H))) → ((((Proj ‘G) ∘ (Proj ‘H)) ‘x) ∈ ℋ ∧ y ∈ ℋ ))
38		ax-hicl 5043	. . . . . . . . . . . . . 14 ⊢ (((((Proj ‘G) ∘ (Proj ‘H)) ‘x) ∈ ℋ ∧ y ∈ ℋ ) → ((((Proj ‘G) ∘ (Proj ‘H)) ‘x) ·_i y) ∈ ℂ)
39		subidt 4159	. . . . . . . . . . . . . 14 ⊢ (((((Proj ‘G) ∘ (Proj ‘H)) ‘x) ·_i y) ∈ ℂ → (((((Proj ‘G) ∘ (Proj ‘H)) ‘x) ·_i y) − ((((Proj ‘G) ∘ (Proj ‘H)) ‘x) ·_i y)) = 0)
40	37, 38, 39	3syl 21	. . . . . . . . . . . . 13 ⊢ ((((Proj ‘G) ∘ (Proj ‘H)) = ((Proj ‘H) ∘ (Proj ‘G)) ∧ (x ∈ ℋ ∧ y ∈ (G ∩ H))) → (((((Proj ‘G) ∘ (Proj ‘H)) ‘x) ·_i y) − ((((Proj ‘G) ∘ (Proj ‘H)) ‘x) ·_i y)) = 0)
41	35, 40	eqtr3d 1130	. . . . . . . . . . . 12 ⊢ ((((Proj ‘G) ∘ (Proj ‘H)) = ((Proj ‘H) ∘ (Proj ‘G)) ∧ (x ∈ ℋ ∧ y ∈ (G ∩ H))) → ((x ·_i y) − ((((Proj ‘G) ∘ (Proj ‘H)) ‘x) ·_i y)) = 0)
42	26, 41	eqtrd 1128	. . . . . . . . . . 11 ⊢ ((((Proj ‘G) ∘ (Proj ‘H)) = ((Proj ‘H) ∘ (Proj ‘G)) ∧ (x ∈ ℋ ∧ y ∈ (G ∩ H))) → ((x −_v (((Proj ‘G) ∘ (Proj ‘H)) ‘x)) ·_i y) = 0)
43	42	exp32 294	. . . . . . . . . 10 ⊢ (((Proj ‘G) ∘ (Proj ‘H)) = ((Proj ‘H) ∘ (Proj ‘G)) → (x ∈ ℋ → (y ∈ (G ∩ H) → ((x −_v (((Proj ‘G) ∘ (Proj ‘H)) ‘x)) ·_i y) = 0)))
44	43	imp 277	. . . . . . . . 9 ⊢ ((((Proj ‘G) ∘ (Proj ‘H)) = ((Proj ‘H) ∘ (Proj ‘G)) ∧ x ∈ ℋ ) → (y ∈ (G ∩ H) → ((x −_v (((Proj ‘G) ∘ (Proj ‘H)) ‘x)) ·_i y) = 0))
45	44	r19.21aiv 1259	. . . . . . . 8 ⊢ ((((Proj ‘G) ∘ (Proj ‘H)) = ((Proj ‘H) ∘ (Proj ‘G)) ∧ x ∈ ℋ ) → ∀y ∈ (G ∩ H)((x −_v (((Proj ‘G) ∘ (Proj ‘H)) ‘x)) ·_i y) = 0)
46	18, 45	jca 236	. . . . . . 7 ⊢ ((((Proj ‘G) ∘ (Proj ‘H)) = ((Proj ‘H) ∘ (Proj ‘G)) ∧ x ∈ ℋ ) → ((x −_v (((Proj ‘G) ∘ (Proj ‘H)) ‘x)) ∈ ℋ ∧ ∀y ∈ (G ∩ H)((x −_v (((Proj ‘G) ∘ (Proj ‘H)) ‘x)) ·_i y) = 0))
47	3	chshi 5132	. . . . . . . 8 ⊢ (G ∩ H) ∈ S_ℋ
48		shocelt 5163	. . . . . . . 8 ⊢ ((G ∩ H) ∈ S_ℋ → ((x −_v (((Proj ‘G) ∘ (Proj ‘H)) ‘x)) ∈ (⊥ ‘(G ∩ H)) ↔ ((x −_v (((Proj ‘G) ∘ (Proj ‘H)) ‘x)) ∈ ℋ ∧ ∀y ∈ (G ∩ H)((x −_v (((Proj ‘G) ∘ (Proj ‘H)) ‘x)) ·_i y) = 0)))
49	47, 48	ax-mp 6	. . . . . . 7 ⊢ ((x −_v (((Proj ‘G) ∘ (Proj ‘H)) ‘x)) ∈ (⊥ ‘(G ∩ H)) ↔ ((x −_v (((Proj ‘G) ∘ (Proj ‘H)) ‘x)) ∈ ℋ ∧ ∀y ∈ (G ∩ H)((x −_v (((Proj ‘G) ∘ (Proj ‘H)) ‘x)) ·_i y) = 0))
50	46, 49	sylibr 175	. . . . . 6 ⊢ ((((Proj ‘G) ∘ (Proj ‘H)) = ((Proj ‘H) ∘ (Proj ‘G)) ∧ x ∈ ℋ ) → (x −_v (((Proj ‘G) ∘ (Proj ‘H)) ‘x)) ∈ (⊥ ‘(G ∩ H)))
51	4, 14, 50	sylanc 361	. . . . 5 ⊢ ((((Proj ‘G) ∘ (Proj ‘H)) = ((Proj ‘H) ∘ (Proj ‘G)) ∧ x ∈ ℋ ) → ((Proj ‘(G ∩ H)) ‘((((Proj ‘G) ∘ (Proj ‘H)) ‘x) +_v (x −_v (((Proj ‘G) ∘ (Proj ‘H)) ‘x)))) = (((Proj ‘G) ∘ (Proj ‘H)) ‘x))
52		hvaddsub12t 5015	. . . . . . . . 9 ⊢ (((((Proj ‘G) ∘ (Proj ‘H)) ‘x) ∈ ℋ ∧ x ∈ ℋ ∧ (((Proj ‘G) ∘ (Proj ‘H)) ‘x) ∈ ℋ ) → ((((Proj ‘G) ∘ (Proj ‘H)) ‘x) +_v (x −_v (((Proj ‘G) ∘ (Proj ‘H)) ‘x))) = (x +_v ((((Proj ‘G) ∘ (Proj ‘H)) ‘x) −_v (((Proj ‘G) ∘ (Proj ‘H)) ‘x))))
53		id 9	. . . . . . . . 9 ⊢ (x ∈ ℋ → x ∈ ℋ )
54	52, 15, 53, 15	syl3anc 629	. . . . . . . 8 ⊢ (x ∈ ℋ → ((((Proj ‘G) ∘ (Proj ‘H)) ‘x) +_v (x −_v (((Proj ‘G) ∘ (Proj ‘H)) ‘x))) = (x +_v ((((Proj ‘G) ∘ (Proj ‘H)) ‘x) −_v (((Proj ‘G) ∘ (Proj ‘H)) ‘x))))
55		hvsubidt 5005	. . . . . . . . . 10 ⊢ ((((Proj ‘G) ∘ (Proj ‘H)) ‘x) ∈ ℋ → ((((Proj ‘G) ∘ (Proj ‘H)) ‘x) −_v (((Proj ‘G) ∘ (Proj ‘H)) ‘x)) = 0_v)
56	15, 55	syl 12	. . . . . . . . 9 ⊢ (x ∈ ℋ → ((((Proj ‘G) ∘ (Proj ‘H)) ‘x) −_v (((Proj ‘G) ∘ (Proj ‘H)) ‘x)) = 0_v)
57	56	opreq2d 3013	. . . . . . . 8 ⊢ (x ∈ ℋ → (x +_v ((((Proj ‘G) ∘ (Proj ‘H)) ‘x) −_v (((Proj ‘G) ∘ (Proj ‘H)) ‘x))) = (x +_v 0_v))
58		ax-hvaddid 4988	. . . . . . . 8 ⊢ (x ∈ ℋ → (x +_v 0_v) = x)
59	54, 57, 58	3eqtrd 1132	. . . . . . 7 ⊢ (x ∈ ℋ → ((((Proj ‘G) ∘ (Proj ‘H)) ‘x) +_v (x −_v (((Proj ‘G) ∘ (Proj ‘H)) ‘x))) = x)
60	59	fveq2d 2836	. . . . . 6 ⊢ (x ∈ ℋ → ((Proj ‘(G ∩ H)) ‘((((Proj ‘G) ∘ (Proj ‘H)) ‘x) +_v (x −_v (((Proj ‘G) ∘ (Proj ‘H)) ‘x)))) = ((Proj ‘(G ∩ H)) ‘x))
61	60	adantl 305	. . . . 5 ⊢ ((((Proj ‘G) ∘ (Proj ‘H)) = ((Proj ‘H) ∘ (Proj ‘G)) ∧ x ∈ ℋ ) → ((Proj ‘(G ∩ H)) ‘((((Proj ‘G) ∘ (Proj ‘H)) ‘x) +_v (x −_v (((Proj ‘G) ∘ (Proj ‘H)) ‘x)))) = ((Proj ‘(G ∩ H)) ‘x))
62	51, 61	eqtr3d 1130	. . . 4 ⊢ ((((Proj ‘G) ∘ (Proj ‘H)) = ((Proj ‘H) ∘ (Proj ‘G)) ∧ x ∈ ℋ ) → (((Proj ‘G) ∘ (Proj ‘H)) ‘x) = ((Proj ‘(G ∩ H)) ‘x))
63	62	exp 291	. . 3 ⊢ (((Proj ‘G) ∘ (Proj ‘H)) = ((Proj ‘H) ∘ (Proj ‘G)) → (x ∈ ℋ → (((Proj ‘G) ∘ (Proj ‘H)) ‘x) = ((Proj ‘(G ∩ H)) ‘x)))
64	63	r19.21aiv 1259	. 2 ⊢ (((Proj ‘G) ∘ (Proj ‘H)) = ((Proj ‘H) ∘ (Proj ‘G)) → ∀x ∈ ℋ (((Proj ‘G) ∘ (Proj ‘H)) ‘x) = ((Proj ‘(G ∩ H)) ‘x))
65	1	pjf 5588	. . . 4 ⊢ (Proj ‘G): ℋ –→ ℋ
66	2	pjf 5588	. . . 4 ⊢ (Proj ‘H): ℋ –→ ℋ
67	65, 66	hocof 5600	. . 3 ⊢ ((Proj ‘G) ∘ (Proj ‘H)): ℋ –→ ℋ
68	3	pjf 5588	. . 3 ⊢ (Proj ‘(G ∩ H)): ℋ –→ ℋ
69	67, 68	hoeq 5595	. 2 ⊢ (∀x ∈ ℋ (((Proj ‘G) ∘ (Proj ‘H)) ‘x) = ((Proj ‘(G ∩ H)) ‘x) ↔ ((Proj ‘G) ∘ (Proj ‘H)) = (Proj ‘(G ∩ H)))
70	64, 69	sylib 173	1 ⊢ (((Proj ‘G) ∘ (Proj ‘H)) = ((Proj ‘H) ∘ (Proj ‘G)) → ((Proj ‘G) ∘ (Proj ‘H)) = (Proj ‘(G ∩ H)))

Colors of variables: wff set class

Syntax hints: → wi 2 ↔ wb 127 ∧ wa 196 ∧ w3a 581 = wceq 1091 ∈ wcel 1092 ∀wral 1201 ∩ cin 1486 ∘ ccom 2414 ‘cfv 2422 (class class class)co 3001 ℂcc 4026 0cc0 4028 − cmin 4089 ℋ chil 4958 +_v cva 4959 0_vc0v 4961 −_v cmv 4962 ·_i csp 4963 S_ℋ csh 4967 C_ℋ cch 4968 ⊥cort 4969 Projcpj 4976

This theorem is referenced by: pjc 5654

This theorem was proved from axioms: ax-1 3 ax-2 4 ax-3 5 ax-mp 6 ax-4 673 ax-5 674 ax-6 675 ax-7 676 ax-gen 677 ax-8 798 ax-9 799 ax-10 800 ax-11 801 ax-12 802 ax-13 804 ax-14 805 ax-16 922 ax-17 925 ax-ext 1074 ax-rep 1075 ax-un 1076 ax-pow 1077 ax-reg 1078 ax-inf 1079 ax-ac 1080 ax-hilex 4983 ax-hvaddcl 4984 ax-hvcom 4985 ax-hvass 4986 ax-hvzercl 4987 ax-hvaddid 4988 ax-hvmulcl 4989 ax-hvmulid 4991 ax-hvmulass 4992 ax-hvdistr1 4993 ax-hvdistr2 4994 ax-hvmulzer 4995 ax-hicl 5043 ax-his1 5045 ax-his2 5046 ax-his3 5047 ax-his4 5048 ax-hcompl 5113

This theorem depends on definitions: df-bi 128 df-or 197 df-an 198 df-3or 582 df-3an 583 df-ex 679 df-sb 853 df-eu 1009 df-mo 1010 df-clab 1093 df-cleq 1097 df-clel 1099 df-ne 1192 df-ral 1205 df-rex 1206 df-reu 1207 df-rab 1208 df-v 1349 df-sbc 1441 df-dif 1489 df-un 1490 df-in 1491 df-ss 1492 df-pss 1494 df-nul 1708 df-if 1777 df-pw 1799 df-sn 1811 df-pr 1812 df-tp 1814 df-op 1815 df-uni 1920 df-int 1966 df-iun 1996 df-tr 2042 df-br 2063 df-opab 2098 df-eprel 2122 df-id 2125 df-po 2128 df-so 2138 df-sup 2154 df-fr 2169 df-we 2186 df-ord 2202 df-on 2203 df-lim 2204 df-suc 2205 df-om 2373 df-xp 2424 df-rel 2425 df-cnv 2426 df-co 2427 df-dm 2428 df-rn 2429 df-res 2430 df-ima 2431 df-fun 2432 df-fn 2433 df-f 2434 df-f1 2435 df-fo 2436 df-f1o 2437 df-fv 2438 df-rdg 2970 df-opr 3003 df-oprab 3004 df-1st 3087 df-2nd 3088 df-1o 3104 df-oadd 3106 df-omul 3107 df-er 3200 df-ec 3202 df-qs 3205 df-ni 3794 df-pli 3795 df-mi 3796 df-lti 3797 df-plpq 3829 df-mpq 3830 df-enq 3831 df-nq 3832 df-plq 3833 df-mq 3834 df-rq 3835 df-ltq 3836 df-1q 3837 df-np 3880 df-1p 3881 df-plp 3882 df-mp 3883 df-ltp 3884 df-plpr 3958 df-mpr 3959 df-enr 3960 df-nr 3961 df-plr 3962 df-mr 3963 df-ltr 3964 df-0r 3965 df-1r 3966 df-m1r 3967 df-c 4034 df-0 4035 df-1 4036 df-i 4037 df-r 4038 df-plus 4039 df-mul 4040 df-lt 4041 df-sub 4133 df-neg 4135 df-div 4216 df-le 4277 df-n 4423 df-2 4462 df-3 4463 df-4 4464 df-n0 4535 df-z 4564 df-seq 4661 df-exp 4676 df-sqr 4728 df-re 4790 df-im 4791 df-cj 4792 df-abs 4793 df-clim 4876 df-hvsub 4996 df-hnorm 5074 df-cauchy 5102 df-hlim 5107 df-sh 5114 df-ch 5127 df-oc 5156 df-ch0 5157 df-pj 5244

metamath.org