HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  chirredlem3 Structured version   Visualization version   GIF version

Theorem chirredlem3 31572
Description: Lemma for chirredi 31574. (Contributed by NM, 15-Jun-2006.) (New usage is discouraged.)
Hypotheses
Ref Expression
chirred.1 𝐴C
chirred.2 (𝑥C𝐴 𝐶 𝑥)
Assertion
Ref Expression
chirredlem3 ((((𝑝 ∈ HAtoms ∧ 𝑝𝐴) ∧ (𝑞 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ (𝑟 ∈ HAtoms ∧ 𝑟 ⊆ (𝑝 𝑞))) → (𝑟𝐴𝑟 = 𝑝))
Distinct variable group:   𝑞,𝑝,𝑟,𝑥,𝐴

Proof of Theorem chirredlem3
StepHypRef Expression
1 atelch 31524 . . 3 (𝑞 ∈ HAtoms → 𝑞C )
2 chirred.1 . . . . . . . . . . . 12 𝐴C
32chirredlem2 31571 . . . . . . . . . . 11 ((((𝑝 ∈ HAtoms ∧ 𝑝𝐴) ∧ (𝑞C𝑞 ⊆ (⊥‘𝐴))) ∧ ((𝑟 ∈ HAtoms ∧ 𝑟𝐴) ∧ 𝑟 ⊆ (𝑝 𝑞))) → ((⊥‘𝑟) ∩ (𝑝 𝑞)) = 𝑞)
43oveq2d 7410 . . . . . . . . . 10 ((((𝑝 ∈ HAtoms ∧ 𝑝𝐴) ∧ (𝑞C𝑞 ⊆ (⊥‘𝐴))) ∧ ((𝑟 ∈ HAtoms ∧ 𝑟𝐴) ∧ 𝑟 ⊆ (𝑝 𝑞))) → (𝑟 ((⊥‘𝑟) ∩ (𝑝 𝑞))) = (𝑟 𝑞))
5 atelch 31524 . . . . . . . . . . . . . 14 (𝑟 ∈ HAtoms → 𝑟C )
65adantr 481 . . . . . . . . . . . . 13 ((𝑟 ∈ HAtoms ∧ 𝑟𝐴) → 𝑟C )
7 atelch 31524 . . . . . . . . . . . . . . 15 (𝑝 ∈ HAtoms → 𝑝C )
8 chjcl 30537 . . . . . . . . . . . . . . 15 ((𝑝C𝑞C ) → (𝑝 𝑞) ∈ C )
97, 8sylan 580 . . . . . . . . . . . . . 14 ((𝑝 ∈ HAtoms ∧ 𝑞C ) → (𝑝 𝑞) ∈ C )
109ad2ant2r 745 . . . . . . . . . . . . 13 (((𝑝 ∈ HAtoms ∧ 𝑝𝐴) ∧ (𝑞C𝑞 ⊆ (⊥‘𝐴))) → (𝑝 𝑞) ∈ C )
11 id 22 . . . . . . . . . . . . 13 (𝑟 ⊆ (𝑝 𝑞) → 𝑟 ⊆ (𝑝 𝑞))
12 pjoml2 30791 . . . . . . . . . . . . 13 ((𝑟C ∧ (𝑝 𝑞) ∈ C𝑟 ⊆ (𝑝 𝑞)) → (𝑟 ((⊥‘𝑟) ∩ (𝑝 𝑞))) = (𝑝 𝑞))
136, 10, 11, 12syl3an 1160 . . . . . . . . . . . 12 (((𝑟 ∈ HAtoms ∧ 𝑟𝐴) ∧ ((𝑝 ∈ HAtoms ∧ 𝑝𝐴) ∧ (𝑞C𝑞 ⊆ (⊥‘𝐴))) ∧ 𝑟 ⊆ (𝑝 𝑞)) → (𝑟 ((⊥‘𝑟) ∩ (𝑝 𝑞))) = (𝑝 𝑞))
14133com12 1123 . . . . . . . . . . 11 ((((𝑝 ∈ HAtoms ∧ 𝑝𝐴) ∧ (𝑞C𝑞 ⊆ (⊥‘𝐴))) ∧ (𝑟 ∈ HAtoms ∧ 𝑟𝐴) ∧ 𝑟 ⊆ (𝑝 𝑞)) → (𝑟 ((⊥‘𝑟) ∩ (𝑝 𝑞))) = (𝑝 𝑞))
15143expb 1120 . . . . . . . . . 10 ((((𝑝 ∈ HAtoms ∧ 𝑝𝐴) ∧ (𝑞C𝑞 ⊆ (⊥‘𝐴))) ∧ ((𝑟 ∈ HAtoms ∧ 𝑟𝐴) ∧ 𝑟 ⊆ (𝑝 𝑞))) → (𝑟 ((⊥‘𝑟) ∩ (𝑝 𝑞))) = (𝑝 𝑞))
164, 15eqtr3d 2774 . . . . . . . . 9 ((((𝑝 ∈ HAtoms ∧ 𝑝𝐴) ∧ (𝑞C𝑞 ⊆ (⊥‘𝐴))) ∧ ((𝑟 ∈ HAtoms ∧ 𝑟𝐴) ∧ 𝑟 ⊆ (𝑝 𝑞))) → (𝑟 𝑞) = (𝑝 𝑞))
1716ineq2d 4209 . . . . . . . 8 ((((𝑝 ∈ HAtoms ∧ 𝑝𝐴) ∧ (𝑞C𝑞 ⊆ (⊥‘𝐴))) ∧ ((𝑟 ∈ HAtoms ∧ 𝑟𝐴) ∧ 𝑟 ⊆ (𝑝 𝑞))) → (𝐴 ∩ (𝑟 𝑞)) = (𝐴 ∩ (𝑝 𝑞)))
18 breq2 5146 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑟 → (𝐴 𝐶 𝑥𝐴 𝐶 𝑟))
19 chirred.2 . . . . . . . . . . . . . . . 16 (𝑥C𝐴 𝐶 𝑥)
2018, 19vtoclga 3563 . . . . . . . . . . . . . . 15 (𝑟C𝐴 𝐶 𝑟)
21 breq2 5146 . . . . . . . . . . . . . . . 16 (𝑥 = 𝑞 → (𝐴 𝐶 𝑥𝐴 𝐶 𝑞))
2221, 19vtoclga 3563 . . . . . . . . . . . . . . 15 (𝑞C𝐴 𝐶 𝑞)
2320, 22anim12i 613 . . . . . . . . . . . . . 14 ((𝑟C𝑞C ) → (𝐴 𝐶 𝑟𝐴 𝐶 𝑞))
24 fh1 30798 . . . . . . . . . . . . . . 15 (((𝐴C𝑟C𝑞C ) ∧ (𝐴 𝐶 𝑟𝐴 𝐶 𝑞)) → (𝐴 ∩ (𝑟 𝑞)) = ((𝐴𝑟) ∨ (𝐴𝑞)))
252, 24mp3anl1 1455 . . . . . . . . . . . . . 14 (((𝑟C𝑞C ) ∧ (𝐴 𝐶 𝑟𝐴 𝐶 𝑞)) → (𝐴 ∩ (𝑟 𝑞)) = ((𝐴𝑟) ∨ (𝐴𝑞)))
2623, 25mpdan 685 . . . . . . . . . . . . 13 ((𝑟C𝑞C ) → (𝐴 ∩ (𝑟 𝑞)) = ((𝐴𝑟) ∨ (𝐴𝑞)))
275, 26sylan 580 . . . . . . . . . . . 12 ((𝑟 ∈ HAtoms ∧ 𝑞C ) → (𝐴 ∩ (𝑟 𝑞)) = ((𝐴𝑟) ∨ (𝐴𝑞)))
2827ancoms 459 . . . . . . . . . . 11 ((𝑞C𝑟 ∈ HAtoms) → (𝐴 ∩ (𝑟 𝑞)) = ((𝐴𝑟) ∨ (𝐴𝑞)))
2928adantrr 715 . . . . . . . . . 10 ((𝑞C ∧ (𝑟 ∈ HAtoms ∧ 𝑟𝐴)) → (𝐴 ∩ (𝑟 𝑞)) = ((𝐴𝑟) ∨ (𝐴𝑞)))
3029ad2ant2r 745 . . . . . . . . 9 (((𝑞C𝑞 ⊆ (⊥‘𝐴)) ∧ ((𝑟 ∈ HAtoms ∧ 𝑟𝐴) ∧ 𝑟 ⊆ (𝑝 𝑞))) → (𝐴 ∩ (𝑟 𝑞)) = ((𝐴𝑟) ∨ (𝐴𝑞)))
3130adantll 712 . . . . . . . 8 ((((𝑝 ∈ HAtoms ∧ 𝑝𝐴) ∧ (𝑞C𝑞 ⊆ (⊥‘𝐴))) ∧ ((𝑟 ∈ HAtoms ∧ 𝑟𝐴) ∧ 𝑟 ⊆ (𝑝 𝑞))) → (𝐴 ∩ (𝑟 𝑞)) = ((𝐴𝑟) ∨ (𝐴𝑞)))
32 breq2 5146 . . . . . . . . . . . . . 14 (𝑥 = 𝑝 → (𝐴 𝐶 𝑥𝐴 𝐶 𝑝))
3332, 19vtoclga 3563 . . . . . . . . . . . . 13 (𝑝C𝐴 𝐶 𝑝)
3433, 22anim12i 613 . . . . . . . . . . . 12 ((𝑝C𝑞C ) → (𝐴 𝐶 𝑝𝐴 𝐶 𝑞))
35 fh1 30798 . . . . . . . . . . . . 13 (((𝐴C𝑝C𝑞C ) ∧ (𝐴 𝐶 𝑝𝐴 𝐶 𝑞)) → (𝐴 ∩ (𝑝 𝑞)) = ((𝐴𝑝) ∨ (𝐴𝑞)))
362, 35mp3anl1 1455 . . . . . . . . . . . 12 (((𝑝C𝑞C ) ∧ (𝐴 𝐶 𝑝𝐴 𝐶 𝑞)) → (𝐴 ∩ (𝑝 𝑞)) = ((𝐴𝑝) ∨ (𝐴𝑞)))
3734, 36mpdan 685 . . . . . . . . . . 11 ((𝑝C𝑞C ) → (𝐴 ∩ (𝑝 𝑞)) = ((𝐴𝑝) ∨ (𝐴𝑞)))
387, 37sylan 580 . . . . . . . . . 10 ((𝑝 ∈ HAtoms ∧ 𝑞C ) → (𝐴 ∩ (𝑝 𝑞)) = ((𝐴𝑝) ∨ (𝐴𝑞)))
3938ad2ant2r 745 . . . . . . . . 9 (((𝑝 ∈ HAtoms ∧ 𝑝𝐴) ∧ (𝑞C𝑞 ⊆ (⊥‘𝐴))) → (𝐴 ∩ (𝑝 𝑞)) = ((𝐴𝑝) ∨ (𝐴𝑞)))
4039adantr 481 . . . . . . . 8 ((((𝑝 ∈ HAtoms ∧ 𝑝𝐴) ∧ (𝑞C𝑞 ⊆ (⊥‘𝐴))) ∧ ((𝑟 ∈ HAtoms ∧ 𝑟𝐴) ∧ 𝑟 ⊆ (𝑝 𝑞))) → (𝐴 ∩ (𝑝 𝑞)) = ((𝐴𝑝) ∨ (𝐴𝑞)))
4117, 31, 403eqtr3d 2780 . . . . . . 7 ((((𝑝 ∈ HAtoms ∧ 𝑝𝐴) ∧ (𝑞C𝑞 ⊆ (⊥‘𝐴))) ∧ ((𝑟 ∈ HAtoms ∧ 𝑟𝐴) ∧ 𝑟 ⊆ (𝑝 𝑞))) → ((𝐴𝑟) ∨ (𝐴𝑞)) = ((𝐴𝑝) ∨ (𝐴𝑞)))
42 sseqin2 4212 . . . . . . . . . . 11 (𝑟𝐴 ↔ (𝐴𝑟) = 𝑟)
4342biimpi 215 . . . . . . . . . 10 (𝑟𝐴 → (𝐴𝑟) = 𝑟)
4443ad2antlr 725 . . . . . . . . 9 (((𝑟 ∈ HAtoms ∧ 𝑟𝐴) ∧ 𝑟 ⊆ (𝑝 𝑞)) → (𝐴𝑟) = 𝑟)
4544adantl 482 . . . . . . . 8 ((((𝑝 ∈ HAtoms ∧ 𝑝𝐴) ∧ (𝑞C𝑞 ⊆ (⊥‘𝐴))) ∧ ((𝑟 ∈ HAtoms ∧ 𝑟𝐴) ∧ 𝑟 ⊆ (𝑝 𝑞))) → (𝐴𝑟) = 𝑟)
46 incom 4198 . . . . . . . . . 10 (𝐴𝑞) = (𝑞𝐴)
47 chsh 30404 . . . . . . . . . . . 12 (𝑞C𝑞S )
482chshii 30407 . . . . . . . . . . . 12 𝐴S
49 orthin 30626 . . . . . . . . . . . 12 ((𝑞S𝐴S ) → (𝑞 ⊆ (⊥‘𝐴) → (𝑞𝐴) = 0))
5047, 48, 49sylancl 586 . . . . . . . . . . 11 (𝑞C → (𝑞 ⊆ (⊥‘𝐴) → (𝑞𝐴) = 0))
5150imp 407 . . . . . . . . . 10 ((𝑞C𝑞 ⊆ (⊥‘𝐴)) → (𝑞𝐴) = 0)
5246, 51eqtrid 2784 . . . . . . . . 9 ((𝑞C𝑞 ⊆ (⊥‘𝐴)) → (𝐴𝑞) = 0)
5352ad2antlr 725 . . . . . . . 8 ((((𝑝 ∈ HAtoms ∧ 𝑝𝐴) ∧ (𝑞C𝑞 ⊆ (⊥‘𝐴))) ∧ ((𝑟 ∈ HAtoms ∧ 𝑟𝐴) ∧ 𝑟 ⊆ (𝑝 𝑞))) → (𝐴𝑞) = 0)
5445, 53oveq12d 7412 . . . . . . 7 ((((𝑝 ∈ HAtoms ∧ 𝑝𝐴) ∧ (𝑞C𝑞 ⊆ (⊥‘𝐴))) ∧ ((𝑟 ∈ HAtoms ∧ 𝑟𝐴) ∧ 𝑟 ⊆ (𝑝 𝑞))) → ((𝐴𝑟) ∨ (𝐴𝑞)) = (𝑟 0))
55 sseqin2 4212 . . . . . . . . . . 11 (𝑝𝐴 ↔ (𝐴𝑝) = 𝑝)
5655biimpi 215 . . . . . . . . . 10 (𝑝𝐴 → (𝐴𝑝) = 𝑝)
5756adantl 482 . . . . . . . . 9 ((𝑝 ∈ HAtoms ∧ 𝑝𝐴) → (𝐴𝑝) = 𝑝)
5857ad2antrr 724 . . . . . . . 8 ((((𝑝 ∈ HAtoms ∧ 𝑝𝐴) ∧ (𝑞C𝑞 ⊆ (⊥‘𝐴))) ∧ ((𝑟 ∈ HAtoms ∧ 𝑟𝐴) ∧ 𝑟 ⊆ (𝑝 𝑞))) → (𝐴𝑝) = 𝑝)
5958, 53oveq12d 7412 . . . . . . 7 ((((𝑝 ∈ HAtoms ∧ 𝑝𝐴) ∧ (𝑞C𝑞 ⊆ (⊥‘𝐴))) ∧ ((𝑟 ∈ HAtoms ∧ 𝑟𝐴) ∧ 𝑟 ⊆ (𝑝 𝑞))) → ((𝐴𝑝) ∨ (𝐴𝑞)) = (𝑝 0))
6041, 54, 593eqtr3d 2780 . . . . . 6 ((((𝑝 ∈ HAtoms ∧ 𝑝𝐴) ∧ (𝑞C𝑞 ⊆ (⊥‘𝐴))) ∧ ((𝑟 ∈ HAtoms ∧ 𝑟𝐴) ∧ 𝑟 ⊆ (𝑝 𝑞))) → (𝑟 0) = (𝑝 0))
61 chj0 30677 . . . . . . . . 9 (𝑟C → (𝑟 0) = 𝑟)
625, 61syl 17 . . . . . . . 8 (𝑟 ∈ HAtoms → (𝑟 0) = 𝑟)
6362ad2antrr 724 . . . . . . 7 (((𝑟 ∈ HAtoms ∧ 𝑟𝐴) ∧ 𝑟 ⊆ (𝑝 𝑞)) → (𝑟 0) = 𝑟)
6463adantl 482 . . . . . 6 ((((𝑝 ∈ HAtoms ∧ 𝑝𝐴) ∧ (𝑞C𝑞 ⊆ (⊥‘𝐴))) ∧ ((𝑟 ∈ HAtoms ∧ 𝑟𝐴) ∧ 𝑟 ⊆ (𝑝 𝑞))) → (𝑟 0) = 𝑟)
65 chj0 30677 . . . . . . . 8 (𝑝C → (𝑝 0) = 𝑝)
667, 65syl 17 . . . . . . 7 (𝑝 ∈ HAtoms → (𝑝 0) = 𝑝)
6766ad3antrrr 728 . . . . . 6 ((((𝑝 ∈ HAtoms ∧ 𝑝𝐴) ∧ (𝑞C𝑞 ⊆ (⊥‘𝐴))) ∧ ((𝑟 ∈ HAtoms ∧ 𝑟𝐴) ∧ 𝑟 ⊆ (𝑝 𝑞))) → (𝑝 0) = 𝑝)
6860, 64, 673eqtr3d 2780 . . . . 5 ((((𝑝 ∈ HAtoms ∧ 𝑝𝐴) ∧ (𝑞C𝑞 ⊆ (⊥‘𝐴))) ∧ ((𝑟 ∈ HAtoms ∧ 𝑟𝐴) ∧ 𝑟 ⊆ (𝑝 𝑞))) → 𝑟 = 𝑝)
6968exp44 438 . . . 4 (((𝑝 ∈ HAtoms ∧ 𝑝𝐴) ∧ (𝑞C𝑞 ⊆ (⊥‘𝐴))) → (𝑟 ∈ HAtoms → (𝑟𝐴 → (𝑟 ⊆ (𝑝 𝑞) → 𝑟 = 𝑝))))
7069com34 91 . . 3 (((𝑝 ∈ HAtoms ∧ 𝑝𝐴) ∧ (𝑞C𝑞 ⊆ (⊥‘𝐴))) → (𝑟 ∈ HAtoms → (𝑟 ⊆ (𝑝 𝑞) → (𝑟𝐴𝑟 = 𝑝))))
711, 70sylanr1 680 . 2 (((𝑝 ∈ HAtoms ∧ 𝑝𝐴) ∧ (𝑞 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝐴))) → (𝑟 ∈ HAtoms → (𝑟 ⊆ (𝑝 𝑞) → (𝑟𝐴𝑟 = 𝑝))))
7271imp32 419 1 ((((𝑝 ∈ HAtoms ∧ 𝑝𝐴) ∧ (𝑞 ∈ HAtoms ∧ 𝑞 ⊆ (⊥‘𝐴))) ∧ (𝑟 ∈ HAtoms ∧ 𝑟 ⊆ (𝑝 𝑞))) → (𝑟𝐴𝑟 = 𝑝))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396   = wceq 1541  wcel 2106  cin 3944  wss 3945   class class class wbr 5142  cfv 6533  (class class class)co 7394   S csh 30108   C cch 30109  cort 30110   chj 30113  0c0h 30115   𝐶 ccm 30116  HAtomscat 30145
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-rep 5279  ax-sep 5293  ax-nul 5300  ax-pow 5357  ax-pr 5421  ax-un 7709  ax-inf2 9620  ax-cc 10414  ax-cnex 11150  ax-resscn 11151  ax-1cn 11152  ax-icn 11153  ax-addcl 11154  ax-addrcl 11155  ax-mulcl 11156  ax-mulrcl 11157  ax-mulcom 11158  ax-addass 11159  ax-mulass 11160  ax-distr 11161  ax-i2m1 11162  ax-1ne0 11163  ax-1rid 11164  ax-rnegex 11165  ax-rrecex 11166  ax-cnre 11167  ax-pre-lttri 11168  ax-pre-lttrn 11169  ax-pre-ltadd 11170  ax-pre-mulgt0 11171  ax-pre-sup 11172  ax-addf 11173  ax-mulf 11174  ax-hilex 30179  ax-hfvadd 30180  ax-hvcom 30181  ax-hvass 30182  ax-hv0cl 30183  ax-hvaddid 30184  ax-hfvmul 30185  ax-hvmulid 30186  ax-hvmulass 30187  ax-hvdistr1 30188  ax-hvdistr2 30189  ax-hvmul0 30190  ax-hfi 30259  ax-his1 30262  ax-his2 30263  ax-his3 30264  ax-his4 30265  ax-hcompl 30382
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3376  df-reu 3377  df-rab 3433  df-v 3476  df-sbc 3775  df-csb 3891  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-pss 3964  df-nul 4320  df-if 4524  df-pw 4599  df-sn 4624  df-pr 4626  df-tp 4628  df-op 4630  df-uni 4903  df-int 4945  df-iun 4993  df-iin 4994  df-br 5143  df-opab 5205  df-mpt 5226  df-tr 5260  df-id 5568  df-eprel 5574  df-po 5582  df-so 5583  df-fr 5625  df-se 5626  df-we 5627  df-xp 5676  df-rel 5677  df-cnv 5678  df-co 5679  df-dm 5680  df-rn 5681  df-res 5682  df-ima 5683  df-pred 6290  df-ord 6357  df-on 6358  df-lim 6359  df-suc 6360  df-iota 6485  df-fun 6535  df-fn 6536  df-f 6537  df-f1 6538  df-fo 6539  df-f1o 6540  df-fv 6541  df-isom 6542  df-riota 7350  df-ov 7397  df-oprab 7398  df-mpo 7399  df-of 7654  df-om 7840  df-1st 7959  df-2nd 7960  df-supp 8131  df-frecs 8250  df-wrecs 8281  df-recs 8355  df-rdg 8394  df-1o 8450  df-2o 8451  df-oadd 8454  df-omul 8455  df-er 8688  df-map 8807  df-pm 8808  df-ixp 8877  df-en 8925  df-dom 8926  df-sdom 8927  df-fin 8928  df-fsupp 9347  df-fi 9390  df-sup 9421  df-inf 9422  df-oi 9489  df-card 9918  df-acn 9921  df-pnf 11234  df-mnf 11235  df-xr 11236  df-ltxr 11237  df-le 11238  df-sub 11430  df-neg 11431  df-div 11856  df-nn 12197  df-2 12259  df-3 12260  df-4 12261  df-5 12262  df-6 12263  df-7 12264  df-8 12265  df-9 12266  df-n0 12457  df-z 12543  df-dec 12662  df-uz 12807  df-q 12917  df-rp 12959  df-xneg 13076  df-xadd 13077  df-xmul 13078  df-ioo 13312  df-ico 13314  df-icc 13315  df-fz 13469  df-fzo 13612  df-fl 13741  df-seq 13951  df-exp 14012  df-hash 14275  df-cj 15030  df-re 15031  df-im 15032  df-sqrt 15166  df-abs 15167  df-clim 15416  df-rlim 15417  df-sum 15617  df-struct 17064  df-sets 17081  df-slot 17099  df-ndx 17111  df-base 17129  df-ress 17158  df-plusg 17194  df-mulr 17195  df-starv 17196  df-sca 17197  df-vsca 17198  df-ip 17199  df-tset 17200  df-ple 17201  df-ds 17203  df-unif 17204  df-hom 17205  df-cco 17206  df-rest 17352  df-topn 17353  df-0g 17371  df-gsum 17372  df-topgen 17373  df-pt 17374  df-prds 17377  df-xrs 17432  df-qtop 17437  df-imas 17438  df-xps 17440  df-mre 17514  df-mrc 17515  df-acs 17517  df-mgm 18545  df-sgrp 18594  df-mnd 18605  df-submnd 18650  df-mulg 18925  df-cntz 19149  df-cmn 19616  df-psmet 20872  df-xmet 20873  df-met 20874  df-bl 20875  df-mopn 20876  df-fbas 20877  df-fg 20878  df-cnfld 20881  df-top 22327  df-topon 22344  df-topsp 22366  df-bases 22380  df-cld 22454  df-ntr 22455  df-cls 22456  df-nei 22533  df-cn 22662  df-cnp 22663  df-lm 22664  df-haus 22750  df-tx 22997  df-hmeo 23190  df-fil 23281  df-fm 23373  df-flim 23374  df-flf 23375  df-xms 23757  df-ms 23758  df-tms 23759  df-cfil 24703  df-cau 24704  df-cmet 24705  df-grpo 29673  df-gid 29674  df-ginv 29675  df-gdiv 29676  df-ablo 29725  df-vc 29739  df-nv 29772  df-va 29775  df-ba 29776  df-sm 29777  df-0v 29778  df-vs 29779  df-nmcv 29780  df-ims 29781  df-dip 29881  df-ssp 29902  df-ph 29993  df-cbn 30043  df-hnorm 30148  df-hba 30149  df-hvsub 30151  df-hlim 30152  df-hcau 30153  df-sh 30387  df-ch 30401  df-oc 30432  df-ch0 30433  df-shs 30488  df-span 30489  df-chj 30490  df-chsup 30491  df-pjh 30575  df-cm 30763  df-cv 31459  df-at 31518
This theorem is referenced by:  chirredlem4  31573
  Copyright terms: Public domain W3C validator