Hilbert Space Explorer

Hilbert Space Explorer

< Previous Next >
Related theorems
GIF version

Theorem pjclem1 5649

Description: Lemma for projection commutation theorem.

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

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

**Proof of Theorem pjclem1**
Step	Hyp	Ref	Expression
1		pjclem1.1	. . . . . 6 ⊢ G ∈ C_ℋ
2		pjclem1.2	. . . . . 6 ⊢ H ∈ C_ℋ
3	1, 2	cmbr 5499	. . . . 5 ⊢ (G Com H ↔ G = ((G ∩ H) ∨_ℋ (G ∩ (⊥ ‘H))))
4		fveq2 2832	. . . . 5 ⊢ (G = ((G ∩ H) ∨_ℋ (G ∩ (⊥ ‘H))) → (Proj ‘G) = (Proj ‘((G ∩ H) ∨_ℋ (G ∩ (⊥ ‘H)))))
5	3, 4	sylbi 174	. . . 4 ⊢ (G Com H → (Proj ‘G) = (Proj ‘((G ∩ H) ∨_ℋ (G ∩ (⊥ ‘H)))))
6		inss2 1658	. . . . . . . 8 ⊢ (G ∩ H) ⊆ H
7	1	chocl 5192	. . . . . . . . . 10 ⊢ (⊥ ‘G) ∈ C_ℋ
8	2, 7	chub2 5391	. . . . . . . . 9 ⊢ H ⊆ ((⊥ ‘G) ∨_ℋ H)
9	1, 2	chdmm3 5400	. . . . . . . . 9 ⊢ (⊥ ‘(G ∩ (⊥ ‘H))) = ((⊥ ‘G) ∨_ℋ H)
10	8, 9	sseqtr4 1533	. . . . . . . 8 ⊢ H ⊆ (⊥ ‘(G ∩ (⊥ ‘H)))
11	6, 10	sstri 1512	. . . . . . 7 ⊢ (G ∩ H) ⊆ (⊥ ‘(G ∩ (⊥ ‘H)))
12	1, 2	chincl 5382	. . . . . . . 8 ⊢ (G ∩ H) ∈ C_ℋ
13	2	chocl 5192	. . . . . . . . 9 ⊢ (⊥ ‘H) ∈ C_ℋ
14	1, 13	chincl 5382	. . . . . . . 8 ⊢ (G ∩ (⊥ ‘H)) ∈ C_ℋ
15	12, 14	pjscj 5640	. . . . . . 7 ⊢ ((G ∩ H) ⊆ (⊥ ‘(G ∩ (⊥ ‘H))) → (Proj ‘((G ∩ H) ∨_ℋ (G ∩ (⊥ ‘H)))) = ((Proj ‘(G ∩ H)) +_P (Proj ‘(G ∩ (⊥ ‘H)))))
16	11, 15	ax-mp 6	. . . . . 6 ⊢ (Proj ‘((G ∩ H) ∨_ℋ (G ∩ (⊥ ‘H)))) = ((Proj ‘(G ∩ H)) +_P (Proj ‘(G ∩ (⊥ ‘H))))
17	16	cleq2i 1111	. . . . 5 ⊢ ((Proj ‘G) = (Proj ‘((G ∩ H) ∨_ℋ (G ∩ (⊥ ‘H)))) ↔ (Proj ‘G) = ((Proj ‘(G ∩ H)) +_P (Proj ‘(G ∩ (⊥ ‘H)))))
18		coeq2 2503	. . . . . 6 ⊢ ((Proj ‘G) = ((Proj ‘(G ∩ H)) +_P (Proj ‘(G ∩ (⊥ ‘H)))) → ((Proj ‘H) ∘ (Proj ‘G)) = ((Proj ‘H) ∘ ((Proj ‘(G ∩ H)) +_P (Proj ‘(G ∩ (⊥ ‘H))))))
19	12	pjf 5588	. . . . . . . . . 10 ⊢ (Proj ‘(G ∩ H)): ℋ –→ ℋ
20	14	pjf 5588	. . . . . . . . . 10 ⊢ (Proj ‘(G ∩ (⊥ ‘H))): ℋ –→ ℋ
21	2, 19, 20	pjsdi 5625	. . . . . . . . 9 ⊢ ((Proj ‘H) ∘ ((Proj ‘(G ∩ H)) +_P (Proj ‘(G ∩ (⊥ ‘H))))) = (((Proj ‘H) ∘ (Proj ‘(G ∩ H))) +_P ((Proj ‘H) ∘ (Proj ‘(G ∩ (⊥ ‘H)))))
22	12, 2	pjss1co 5633	. . . . . . . . . . 11 ⊢ ((G ∩ H) ⊆ H ↔ ((Proj ‘H) ∘ (Proj ‘(G ∩ H))) = (Proj ‘(G ∩ H)))
23	6, 22	mpbi 164	. . . . . . . . . 10 ⊢ ((Proj ‘H) ∘ (Proj ‘(G ∩ H))) = (Proj ‘(G ∩ H))
24	2, 14	pjorthco 5639	. . . . . . . . . . 11 ⊢ (H ⊆ (⊥ ‘(G ∩ (⊥ ‘H))) → ((Proj ‘H) ∘ (Proj ‘(G ∩ (⊥ ‘H)))) = (Proj ‘0_ℋ))
25	10, 24	ax-mp 6	. . . . . . . . . 10 ⊢ ((Proj ‘H) ∘ (Proj ‘(G ∩ (⊥ ‘H)))) = (Proj ‘0_ℋ)
26	23, 25	opreq12i 3011	. . . . . . . . 9 ⊢ (((Proj ‘H) ∘ (Proj ‘(G ∩ H))) +_P ((Proj ‘H) ∘ (Proj ‘(G ∩ (⊥ ‘H))))) = ((Proj ‘(G ∩ H)) +_P (Proj ‘0_ℋ))
27	19	hoid0 5614	. . . . . . . . 9 ⊢ ((Proj ‘(G ∩ H)) +_P (Proj ‘0_ℋ)) = (Proj ‘(G ∩ H))
28	21, 26, 27	3eqtr 1123	. . . . . . . 8 ⊢ ((Proj ‘H) ∘ ((Proj ‘(G ∩ H)) +_P (Proj ‘(G ∩ (⊥ ‘H))))) = (Proj ‘(G ∩ H))
29	28	cleq2i 1111	. . . . . . 7 ⊢ (((Proj ‘H) ∘ (Proj ‘G)) = ((Proj ‘H) ∘ ((Proj ‘(G ∩ H)) +_P (Proj ‘(G ∩ (⊥ ‘H))))) ↔ ((Proj ‘H) ∘ (Proj ‘G)) = (Proj ‘(G ∩ H)))
30		coeq2 2503	. . . . . . . 8 ⊢ (((Proj ‘H) ∘ (Proj ‘G)) = (Proj ‘(G ∩ H)) → ((Proj ‘G) ∘ ((Proj ‘H) ∘ (Proj ‘G))) = ((Proj ‘G) ∘ (Proj ‘(G ∩ H))))
31		inss1 1657	. . . . . . . . 9 ⊢ (G ∩ H) ⊆ G
32	12, 1	pjss1co 5633	. . . . . . . . 9 ⊢ ((G ∩ H) ⊆ G ↔ ((Proj ‘G) ∘ (Proj ‘(G ∩ H))) = (Proj ‘(G ∩ H)))
33	31, 32	mpbi 164	. . . . . . . 8 ⊢ ((Proj ‘G) ∘ (Proj ‘(G ∩ H))) = (Proj ‘(G ∩ H))
34	30, 33	syl6eq 1140	. . . . . . 7 ⊢ (((Proj ‘H) ∘ (Proj ‘G)) = (Proj ‘(G ∩ H)) → ((Proj ‘G) ∘ ((Proj ‘H) ∘ (Proj ‘G))) = (Proj ‘(G ∩ H)))
35	29, 34	sylbi 174	. . . . . 6 ⊢ (((Proj ‘H) ∘ (Proj ‘G)) = ((Proj ‘H) ∘ ((Proj ‘(G ∩ H)) +_P (Proj ‘(G ∩ (⊥ ‘H))))) → ((Proj ‘G) ∘ ((Proj ‘H) ∘ (Proj ‘G))) = (Proj ‘(G ∩ H)))
36	18, 35	syl 12	. . . . 5 ⊢ ((Proj ‘G) = ((Proj ‘(G ∩ H)) +_P (Proj ‘(G ∩ (⊥ ‘H)))) → ((Proj ‘G) ∘ ((Proj ‘H) ∘ (Proj ‘G))) = (Proj ‘(G ∩ H)))
37	17, 36	sylbi 174	. . . 4 ⊢ ((Proj ‘G) = (Proj ‘((G ∩ H) ∨_ℋ (G ∩ (⊥ ‘H)))) → ((Proj ‘G) ∘ ((Proj ‘H) ∘ (Proj ‘G))) = (Proj ‘(G ∩ H)))
38	5, 37	syl 12	. . 3 ⊢ (G Com H → ((Proj ‘G) ∘ ((Proj ‘H) ∘ (Proj ‘G))) = (Proj ‘(G ∩ H)))
39	1, 2	cmcm3 5503	. . . . 5 ⊢ (G Com H ↔ (⊥ ‘G) Com H)
40	7, 2	cmbr 5499	. . . . 5 ⊢ ((⊥ ‘G) Com H ↔ (⊥ ‘G) = (((⊥ ‘G) ∩ H) ∨_ℋ ((⊥ ‘G) ∩ (⊥ ‘H))))
41	39, 40	bitr 151	. . . 4 ⊢ (G Com H ↔ (⊥ ‘G) = (((⊥ ‘G) ∩ H) ∨_ℋ ((⊥ ‘G) ∩ (⊥ ‘H))))
42		fveq2 2832	. . . . 5 ⊢ ((⊥ ‘G) = (((⊥ ‘G) ∩ H) ∨_ℋ ((⊥ ‘G) ∩ (⊥ ‘H))) → (Proj ‘(⊥ ‘G)) = (Proj ‘(((⊥ ‘G) ∩ H) ∨_ℋ ((⊥ ‘G) ∩ (⊥ ‘H)))))
43		inss2 1658	. . . . . . . . 9 ⊢ ((⊥ ‘G) ∩ H) ⊆ H
44	2, 1	chub2 5391	. . . . . . . . . 10 ⊢ H ⊆ (G ∨_ℋ H)
45	1, 2	chdmm4 5401	. . . . . . . . . 10 ⊢ (⊥ ‘((⊥ ‘G) ∩ (⊥ ‘H))) = (G ∨_ℋ H)
46	44, 45	sseqtr4 1533	. . . . . . . . 9 ⊢ H ⊆ (⊥ ‘((⊥ ‘G) ∩ (⊥ ‘H)))
47	43, 46	sstri 1512	. . . . . . . 8 ⊢ ((⊥ ‘G) ∩ H) ⊆ (⊥ ‘((⊥ ‘G) ∩ (⊥ ‘H)))
48	7, 2	chincl 5382	. . . . . . . . 9 ⊢ ((⊥ ‘G) ∩ H) ∈ C_ℋ
49	7, 13	chincl 5382	. . . . . . . . 9 ⊢ ((⊥ ‘G) ∩ (⊥ ‘H)) ∈ C_ℋ
50	48, 49	pjscj 5640	. . . . . . . 8 ⊢ (((⊥ ‘G) ∩ H) ⊆ (⊥ ‘((⊥ ‘G) ∩ (⊥ ‘H))) → (Proj ‘(((⊥ ‘G) ∩ H) ∨_ℋ ((⊥ ‘G) ∩ (⊥ ‘H)))) = ((Proj ‘((⊥ ‘G) ∩ H)) +_P (Proj ‘((⊥ ‘G) ∩ (⊥ ‘H)))))
51	47, 50	ax-mp 6	. . . . . . 7 ⊢ (Proj ‘(((⊥ ‘G) ∩ H) ∨_ℋ ((⊥ ‘G) ∩ (⊥ ‘H)))) = ((Proj ‘((⊥ ‘G) ∩ H)) +_P (Proj ‘((⊥ ‘G) ∩ (⊥ ‘H))))
52	51	cleq2i 1111	. . . . . 6 ⊢ ((Proj ‘(⊥ ‘G)) = (Proj ‘(((⊥ ‘G) ∩ H) ∨_ℋ ((⊥ ‘G) ∩ (⊥ ‘H)))) ↔ (Proj ‘(⊥ ‘G)) = ((Proj ‘((⊥ ‘G) ∩ H)) +_P (Proj ‘((⊥ ‘G) ∩ (⊥ ‘H)))))
53		coeq2 2503	. . . . . . 7 ⊢ ((Proj ‘(⊥ ‘G)) = ((Proj ‘((⊥ ‘G) ∩ H)) +_P (Proj ‘((⊥ ‘G) ∩ (⊥ ‘H)))) → ((Proj ‘H) ∘ (Proj ‘(⊥ ‘G))) = ((Proj ‘H) ∘ ((Proj ‘((⊥ ‘G) ∩ H)) +_P (Proj ‘((⊥ ‘G) ∩ (⊥ ‘H))))))
54	48	pjf 5588	. . . . . . . . . . 11 ⊢ (Proj ‘((⊥ ‘G) ∩ H)): ℋ –→ ℋ
55	49	pjf 5588	. . . . . . . . . . 11 ⊢ (Proj ‘((⊥ ‘G) ∩ (⊥ ‘H))): ℋ –→ ℋ
56	2, 54, 55	pjsdi 5625	. . . . . . . . . 10 ⊢ ((Proj ‘H) ∘ ((Proj ‘((⊥ ‘G) ∩ H)) +_P (Proj ‘((⊥ ‘G) ∩ (⊥ ‘H))))) = (((Proj ‘H) ∘ (Proj ‘((⊥ ‘G) ∩ H))) +_P ((Proj ‘H) ∘ (Proj ‘((⊥ ‘G) ∩ (⊥ ‘H)))))
57	48, 2	pjss1co 5633	. . . . . . . . . . . 12 ⊢ (((⊥ ‘G) ∩ H) ⊆ H ↔ ((Proj ‘H) ∘ (Proj ‘((⊥ ‘G) ∩ H))) = (Proj ‘((⊥ ‘G) ∩ H)))
58	43, 57	mpbi 164	. . . . . . . . . . 11 ⊢ ((Proj ‘H) ∘ (Proj ‘((⊥ ‘G) ∩ H))) = (Proj ‘((⊥ ‘G) ∩ H))
59	2, 49	pjorthco 5639	. . . . . . . . . . . 12 ⊢ (H ⊆ (⊥ ‘((⊥ ‘G) ∩ (⊥ ‘H))) → ((Proj ‘H) ∘ (Proj ‘((⊥ ‘G) ∩ (⊥ ‘H)))) = (Proj ‘0_ℋ))
60	46, 59	ax-mp 6	. . . . . . . . . . 11 ⊢ ((Proj ‘H) ∘ (Proj ‘((⊥ ‘G) ∩ (⊥ ‘H)))) = (Proj ‘0_ℋ)
61	58, 60	opreq12i 3011	. . . . . . . . . 10 ⊢ (((Proj ‘H) ∘ (Proj ‘((⊥ ‘G) ∩ H))) +_P ((Proj ‘H) ∘ (Proj ‘((⊥ ‘G) ∩ (⊥ ‘H))))) = ((Proj ‘((⊥ ‘G) ∩ H)) +_P (Proj ‘0_ℋ))
62	54	hoid0 5614	. . . . . . . . . 10 ⊢ ((Proj ‘((⊥ ‘G) ∩ H)) +_P (Proj ‘0_ℋ)) = (Proj ‘((⊥ ‘G) ∩ H))
63	56, 61, 62	3eqtr 1123	. . . . . . . . 9 ⊢ ((Proj ‘H) ∘ ((Proj ‘((⊥ ‘G) ∩ H)) +_P (Proj ‘((⊥ ‘G) ∩ (⊥ ‘H))))) = (Proj ‘((⊥ ‘G) ∩ H))
64	63	cleq2i 1111	. . . . . . . 8 ⊢ (((Proj ‘H) ∘ (Proj ‘(⊥ ‘G))) = ((Proj ‘H) ∘ ((Proj ‘((⊥ ‘G) ∩ H)) +_P (Proj ‘((⊥ ‘G) ∩ (⊥ ‘H))))) ↔ ((Proj ‘H) ∘ (Proj ‘(⊥ ‘G))) = (Proj ‘((⊥ ‘G) ∩ H)))
65		coeq2 2503	. . . . . . . . 9 ⊢ (((Proj ‘H) ∘ (Proj ‘(⊥ ‘G))) = (Proj ‘((⊥ ‘G) ∩ H)) → ((Proj ‘G) ∘ ((Proj ‘H) ∘ (Proj ‘(⊥ ‘G)))) = ((Proj ‘G) ∘ (Proj ‘((⊥ ‘G) ∩ H))))
66	1, 13	chub1 5390	. . . . . . . . . . 11 ⊢ G ⊆ (G ∨_ℋ (⊥ ‘H))
67	1, 2	chdmm2 5399	. . . . . . . . . . 11 ⊢ (⊥ ‘((⊥ ‘G) ∩ H)) = (G ∨_ℋ (⊥ ‘H))
68	66, 67	sseqtr4 1533	. . . . . . . . . 10 ⊢ G ⊆ (⊥ ‘((⊥ ‘G) ∩ H))
69	1, 48	pjorthco 5639	. . . . . . . . . 10 ⊢ (G ⊆ (⊥ ‘((⊥ ‘G) ∩ H)) → ((Proj ‘G) ∘ (Proj ‘((⊥ ‘G) ∩ H))) = (Proj ‘0_ℋ))
70	68, 69	ax-mp 6	. . . . . . . . 9 ⊢ ((Proj ‘G) ∘ (Proj ‘((⊥ ‘G) ∩ H))) = (Proj ‘0_ℋ)
71	65, 70	syl6eq 1140	. . . . . . . 8 ⊢ (((Proj ‘H) ∘ (Proj ‘(⊥ ‘G))) = (Proj ‘((⊥ ‘G) ∩ H)) → ((Proj ‘G) ∘ ((Proj ‘H) ∘ (Proj ‘(⊥ ‘G)))) = (Proj ‘0_ℋ))
72	64, 71	sylbi 174	. . . . . . 7 ⊢ (((Proj ‘H) ∘ (Proj ‘(⊥ ‘G))) = ((Proj ‘H) ∘ ((Proj ‘((⊥ ‘G) ∩ H)) +_P (Proj ‘((⊥ ‘G) ∩ (⊥ ‘H))))) → ((Proj ‘G) ∘ ((Proj ‘H) ∘ (Proj ‘(⊥ ‘G)))) = (Proj ‘0_ℋ))
73	53, 72	syl 12	. . . . . 6 ⊢ ((Proj ‘(⊥ ‘G)) = ((Proj ‘((⊥ ‘G) ∩ H)) +_P (Proj ‘((⊥ ‘G) ∩ (⊥ ‘H)))) → ((Proj ‘G) ∘ ((Proj ‘H) ∘ (Proj ‘(⊥ ‘G)))) = (Proj ‘0_ℋ))
74	52, 73	sylbi 174	. . . . 5 ⊢ ((Proj ‘(⊥ ‘G)) = (Proj ‘(((⊥ ‘G) ∩ H) ∨_ℋ ((⊥ ‘G) ∩ (⊥ ‘H)))) → ((Proj ‘G) ∘ ((Proj ‘H) ∘ (Proj ‘(⊥ ‘G)))) = (Proj ‘0_ℋ))
75	42, 74	syl 12	. . . 4 ⊢ ((⊥ ‘G) = (((⊥ ‘G) ∩ H) ∨_ℋ ((⊥ ‘G) ∩ (⊥ ‘H))) → ((Proj ‘G) ∘ ((Proj ‘H) ∘ (Proj ‘(⊥ ‘G)))) = (Proj ‘0_ℋ))
76	41, 75	sylbi 174	. . 3 ⊢ (G Com H → ((Proj ‘G) ∘ ((Proj ‘H) ∘ (Proj ‘(⊥ ‘G)))) = (Proj ‘0_ℋ))
77	38, 76	opreq12d 3014	. 2 ⊢ (G Com H → (((Proj ‘G) ∘ ((Proj ‘H) ∘ (Proj ‘G))) +_P ((Proj ‘G) ∘ ((Proj ‘H) ∘ (Proj ‘(⊥ ‘G))))) = ((Proj ‘(G ∩ H)) +_P (Proj ‘0_ℋ)))
78	1	pjtot 5644	. . . . . 6 ⊢ ((Proj ‘G) +_P (Proj ‘(⊥ ‘G))) = (Proj ‘ ℋ )
79	78	coeq2i 2505	. . . . 5 ⊢ ((Proj ‘H) ∘ ((Proj ‘G) +_P (Proj ‘(⊥ ‘G)))) = ((Proj ‘H) ∘ (Proj ‘ ℋ ))
80	1	pjf 5588	. . . . . 6 ⊢ (Proj ‘G): ℋ –→ ℋ
81	7	pjf 5588	. . . . . 6 ⊢ (Proj ‘(⊥ ‘G)): ℋ –→ ℋ
82	2, 80, 81	pjsdi 5625	. . . . 5 ⊢ ((Proj ‘H) ∘ ((Proj ‘G) +_P (Proj ‘(⊥ ‘G)))) = (((Proj ‘H) ∘ (Proj ‘G)) +_P ((Proj ‘H) ∘ (Proj ‘(⊥ ‘G))))
83	2	pjf 5588	. . . . . 6 ⊢ (Proj ‘H): ℋ –→ ℋ
84	83	hoid1 5617	. . . . 5 ⊢ ((Proj ‘H) ∘ (Proj ‘ ℋ )) = (Proj ‘H)
85	79, 82, 84	3eqtr3r 1125	. . . 4 ⊢ (Proj ‘H) = (((Proj ‘H) ∘ (Proj ‘G)) +_P ((Proj ‘H) ∘ (Proj ‘(⊥ ‘G))))
86	85	coeq2i 2505	. . 3 ⊢ ((Proj ‘G) ∘ (Proj ‘H)) = ((Proj ‘G) ∘ (((Proj ‘H) ∘ (Proj ‘G)) +_P ((Proj ‘H) ∘ (Proj ‘(⊥ ‘G)))))
87	83, 80	hocof 5600	. . . 4 ⊢ ((Proj ‘H) ∘ (Proj ‘G)): ℋ –→ ℋ
88	83, 81	hocof 5600	. . . 4 ⊢ ((Proj ‘H) ∘ (Proj ‘(⊥ ‘G))): ℋ –→ ℋ
89	1, 87, 88	pjsdi 5625	. . 3 ⊢ ((Proj ‘G) ∘ (((Proj ‘H) ∘ (Proj ‘G)) +_P ((Proj ‘H) ∘ (Proj ‘(⊥ ‘G))))) = (((Proj ‘G) ∘ ((Proj ‘H) ∘ (Proj ‘G))) +_P ((Proj ‘G) ∘ ((Proj ‘H) ∘ (Proj ‘(⊥ ‘G)))))
90	86, 89	eqtr2 1120	. 2 ⊢ (((Proj ‘G) ∘ ((Proj ‘H) ∘ (Proj ‘G))) +_P ((Proj ‘G) ∘ ((Proj ‘H) ∘ (Proj ‘(⊥ ‘G))))) = ((Proj ‘G) ∘ (Proj ‘H))
91	77, 90, 27	3eqtr3g 1146	1 ⊢ (G Com H → ((Proj ‘G) ∘ (Proj ‘H)) = (Proj ‘(G ∩ H)))

Colors of variables: wff set class

Syntax hints: → wi 2 = wceq 1091 ∈ wcel 1092 ∩ cin 1486 ⊆ wss 1487 class class class wbr 2054 ∘ ccom 2414 ‘cfv 2422 (class class class)co 3001 ℋ chil 4958 C_ℋ cch 4968 ⊥cort 4969 ∨_ℋ chj 4972 0_ℋc0h 4974 Com ccm 4975 Projcpj 4976 +_P chos 4977

This theorem is referenced by: pjclem2 5650

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 df-shsum 5275 df-chj 5277 df-hosum 5485 df-cm 5493

metamath.org