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

Theorem fh1 27650
Description: Foulis-Holland Theorem. If any 2 pairs in a triple of orthomodular lattice elements commute, the triple is distributive. First of two parts. Theorem 5 of [Kalmbach] p. 25. (Contributed by NM, 14-Jun-2006.) (New usage is discouraged.)
Assertion
Ref Expression
fh1 (((𝐴C𝐵C𝐶C ) ∧ (𝐴 𝐶 𝐵𝐴 𝐶 𝐶)) → (𝐴 ∩ (𝐵 𝐶)) = ((𝐴𝐵) ∨ (𝐴𝐶)))

Proof of Theorem fh1
StepHypRef Expression
1 chincl 27531 . . . . . . . 8 ((𝐴C𝐵C ) → (𝐴𝐵) ∈ C )
2 chincl 27531 . . . . . . . 8 ((𝐴C𝐶C ) → (𝐴𝐶) ∈ C )
3 chjcl 27389 . . . . . . . 8 (((𝐴𝐵) ∈ C ∧ (𝐴𝐶) ∈ C ) → ((𝐴𝐵) ∨ (𝐴𝐶)) ∈ C )
41, 2, 3syl2an 492 . . . . . . 7 (((𝐴C𝐵C ) ∧ (𝐴C𝐶C )) → ((𝐴𝐵) ∨ (𝐴𝐶)) ∈ C )
54anandis 868 . . . . . 6 ((𝐴C ∧ (𝐵C𝐶C )) → ((𝐴𝐵) ∨ (𝐴𝐶)) ∈ C )
6 chjcl 27389 . . . . . . . 8 ((𝐵C𝐶C ) → (𝐵 𝐶) ∈ C )
7 chincl 27531 . . . . . . . 8 ((𝐴C ∧ (𝐵 𝐶) ∈ C ) → (𝐴 ∩ (𝐵 𝐶)) ∈ C )
86, 7sylan2 489 . . . . . . 7 ((𝐴C ∧ (𝐵C𝐶C )) → (𝐴 ∩ (𝐵 𝐶)) ∈ C )
9 chsh 27254 . . . . . . 7 ((𝐴 ∩ (𝐵 𝐶)) ∈ C → (𝐴 ∩ (𝐵 𝐶)) ∈ S )
108, 9syl 17 . . . . . 6 ((𝐴C ∧ (𝐵C𝐶C )) → (𝐴 ∩ (𝐵 𝐶)) ∈ S )
115, 10jca 552 . . . . 5 ((𝐴C ∧ (𝐵C𝐶C )) → (((𝐴𝐵) ∨ (𝐴𝐶)) ∈ C ∧ (𝐴 ∩ (𝐵 𝐶)) ∈ S ))
12113impb 1251 . . . 4 ((𝐴C𝐵C𝐶C ) → (((𝐴𝐵) ∨ (𝐴𝐶)) ∈ C ∧ (𝐴 ∩ (𝐵 𝐶)) ∈ S ))
1312adantr 479 . . 3 (((𝐴C𝐵C𝐶C ) ∧ (𝐴 𝐶 𝐵𝐴 𝐶 𝐶)) → (((𝐴𝐵) ∨ (𝐴𝐶)) ∈ C ∧ (𝐴 ∩ (𝐵 𝐶)) ∈ S ))
14 ledi 27572 . . . 4 ((𝐴C𝐵C𝐶C ) → ((𝐴𝐵) ∨ (𝐴𝐶)) ⊆ (𝐴 ∩ (𝐵 𝐶)))
1514adantr 479 . . 3 (((𝐴C𝐵C𝐶C ) ∧ (𝐴 𝐶 𝐵𝐴 𝐶 𝐶)) → ((𝐴𝐵) ∨ (𝐴𝐶)) ⊆ (𝐴 ∩ (𝐵 𝐶)))
16 incom 3670 . . . . . . . 8 (𝐴 ∩ (𝐵 𝐶)) = ((𝐵 𝐶) ∩ 𝐴)
1716a1i 11 . . . . . . 7 (((𝐴C𝐵C ) ∧ (𝐴C𝐶C )) → (𝐴 ∩ (𝐵 𝐶)) = ((𝐵 𝐶) ∩ 𝐴))
18 chdmj1 27561 . . . . . . . . 9 (((𝐴𝐵) ∈ C ∧ (𝐴𝐶) ∈ C ) → (⊥‘((𝐴𝐵) ∨ (𝐴𝐶))) = ((⊥‘(𝐴𝐵)) ∩ (⊥‘(𝐴𝐶))))
191, 2, 18syl2an 492 . . . . . . . 8 (((𝐴C𝐵C ) ∧ (𝐴C𝐶C )) → (⊥‘((𝐴𝐵) ∨ (𝐴𝐶))) = ((⊥‘(𝐴𝐵)) ∩ (⊥‘(𝐴𝐶))))
20 chdmm1 27557 . . . . . . . . 9 ((𝐴C𝐵C ) → (⊥‘(𝐴𝐵)) = ((⊥‘𝐴) ∨ (⊥‘𝐵)))
21 chdmm1 27557 . . . . . . . . 9 ((𝐴C𝐶C ) → (⊥‘(𝐴𝐶)) = ((⊥‘𝐴) ∨ (⊥‘𝐶)))
2220, 21ineqan12d 3681 . . . . . . . 8 (((𝐴C𝐵C ) ∧ (𝐴C𝐶C )) → ((⊥‘(𝐴𝐵)) ∩ (⊥‘(𝐴𝐶))) = (((⊥‘𝐴) ∨ (⊥‘𝐵)) ∩ ((⊥‘𝐴) ∨ (⊥‘𝐶))))
2319, 22eqtrd 2548 . . . . . . 7 (((𝐴C𝐵C ) ∧ (𝐴C𝐶C )) → (⊥‘((𝐴𝐵) ∨ (𝐴𝐶))) = (((⊥‘𝐴) ∨ (⊥‘𝐵)) ∩ ((⊥‘𝐴) ∨ (⊥‘𝐶))))
2417, 23ineq12d 3680 . . . . . 6 (((𝐴C𝐵C ) ∧ (𝐴C𝐶C )) → ((𝐴 ∩ (𝐵 𝐶)) ∩ (⊥‘((𝐴𝐵) ∨ (𝐴𝐶)))) = (((𝐵 𝐶) ∩ 𝐴) ∩ (((⊥‘𝐴) ∨ (⊥‘𝐵)) ∩ ((⊥‘𝐴) ∨ (⊥‘𝐶)))))
25243impdi 1372 . . . . 5 ((𝐴C𝐵C𝐶C ) → ((𝐴 ∩ (𝐵 𝐶)) ∩ (⊥‘((𝐴𝐵) ∨ (𝐴𝐶)))) = (((𝐵 𝐶) ∩ 𝐴) ∩ (((⊥‘𝐴) ∨ (⊥‘𝐵)) ∩ ((⊥‘𝐴) ∨ (⊥‘𝐶)))))
2625adantr 479 . . . 4 (((𝐴C𝐵C𝐶C ) ∧ (𝐴 𝐶 𝐵𝐴 𝐶 𝐶)) → ((𝐴 ∩ (𝐵 𝐶)) ∩ (⊥‘((𝐴𝐵) ∨ (𝐴𝐶)))) = (((𝐵 𝐶) ∩ 𝐴) ∩ (((⊥‘𝐴) ∨ (⊥‘𝐵)) ∩ ((⊥‘𝐴) ∨ (⊥‘𝐶)))))
27 inass 3688 . . . . . . 7 (((𝐵 𝐶) ∩ 𝐴) ∩ (((⊥‘𝐴) ∨ (⊥‘𝐵)) ∩ ((⊥‘𝐴) ∨ (⊥‘𝐶)))) = ((𝐵 𝐶) ∩ (𝐴 ∩ (((⊥‘𝐴) ∨ (⊥‘𝐵)) ∩ ((⊥‘𝐴) ∨ (⊥‘𝐶)))))
28 cmcm2 27648 . . . . . . . . . . . . . 14 ((𝐴C𝐵C ) → (𝐴 𝐶 𝐵𝐴 𝐶 (⊥‘𝐵)))
29 choccl 27338 . . . . . . . . . . . . . . 15 (𝐵C → (⊥‘𝐵) ∈ C )
30 cmbr3 27640 . . . . . . . . . . . . . . 15 ((𝐴C ∧ (⊥‘𝐵) ∈ C ) → (𝐴 𝐶 (⊥‘𝐵) ↔ (𝐴 ∩ ((⊥‘𝐴) ∨ (⊥‘𝐵))) = (𝐴 ∩ (⊥‘𝐵))))
3129, 30sylan2 489 . . . . . . . . . . . . . 14 ((𝐴C𝐵C ) → (𝐴 𝐶 (⊥‘𝐵) ↔ (𝐴 ∩ ((⊥‘𝐴) ∨ (⊥‘𝐵))) = (𝐴 ∩ (⊥‘𝐵))))
3228, 31bitrd 266 . . . . . . . . . . . . 13 ((𝐴C𝐵C ) → (𝐴 𝐶 𝐵 ↔ (𝐴 ∩ ((⊥‘𝐴) ∨ (⊥‘𝐵))) = (𝐴 ∩ (⊥‘𝐵))))
3332biimpa 499 . . . . . . . . . . . 12 (((𝐴C𝐵C ) ∧ 𝐴 𝐶 𝐵) → (𝐴 ∩ ((⊥‘𝐴) ∨ (⊥‘𝐵))) = (𝐴 ∩ (⊥‘𝐵)))
34333adantl3 1211 . . . . . . . . . . 11 (((𝐴C𝐵C𝐶C ) ∧ 𝐴 𝐶 𝐵) → (𝐴 ∩ ((⊥‘𝐴) ∨ (⊥‘𝐵))) = (𝐴 ∩ (⊥‘𝐵)))
3534adantrr 748 . . . . . . . . . 10 (((𝐴C𝐵C𝐶C ) ∧ (𝐴 𝐶 𝐵𝐴 𝐶 𝐶)) → (𝐴 ∩ ((⊥‘𝐴) ∨ (⊥‘𝐵))) = (𝐴 ∩ (⊥‘𝐵)))
36 cmcm2 27648 . . . . . . . . . . . . . 14 ((𝐴C𝐶C ) → (𝐴 𝐶 𝐶𝐴 𝐶 (⊥‘𝐶)))
37 choccl 27338 . . . . . . . . . . . . . . 15 (𝐶C → (⊥‘𝐶) ∈ C )
38 cmbr3 27640 . . . . . . . . . . . . . . 15 ((𝐴C ∧ (⊥‘𝐶) ∈ C ) → (𝐴 𝐶 (⊥‘𝐶) ↔ (𝐴 ∩ ((⊥‘𝐴) ∨ (⊥‘𝐶))) = (𝐴 ∩ (⊥‘𝐶))))
3937, 38sylan2 489 . . . . . . . . . . . . . 14 ((𝐴C𝐶C ) → (𝐴 𝐶 (⊥‘𝐶) ↔ (𝐴 ∩ ((⊥‘𝐴) ∨ (⊥‘𝐶))) = (𝐴 ∩ (⊥‘𝐶))))
4036, 39bitrd 266 . . . . . . . . . . . . 13 ((𝐴C𝐶C ) → (𝐴 𝐶 𝐶 ↔ (𝐴 ∩ ((⊥‘𝐴) ∨ (⊥‘𝐶))) = (𝐴 ∩ (⊥‘𝐶))))
4140biimpa 499 . . . . . . . . . . . 12 (((𝐴C𝐶C ) ∧ 𝐴 𝐶 𝐶) → (𝐴 ∩ ((⊥‘𝐴) ∨ (⊥‘𝐶))) = (𝐴 ∩ (⊥‘𝐶)))
42413adantl2 1210 . . . . . . . . . . 11 (((𝐴C𝐵C𝐶C ) ∧ 𝐴 𝐶 𝐶) → (𝐴 ∩ ((⊥‘𝐴) ∨ (⊥‘𝐶))) = (𝐴 ∩ (⊥‘𝐶)))
4342adantrl 747 . . . . . . . . . 10 (((𝐴C𝐵C𝐶C ) ∧ (𝐴 𝐶 𝐵𝐴 𝐶 𝐶)) → (𝐴 ∩ ((⊥‘𝐴) ∨ (⊥‘𝐶))) = (𝐴 ∩ (⊥‘𝐶)))
4435, 43ineq12d 3680 . . . . . . . . 9 (((𝐴C𝐵C𝐶C ) ∧ (𝐴 𝐶 𝐵𝐴 𝐶 𝐶)) → ((𝐴 ∩ ((⊥‘𝐴) ∨ (⊥‘𝐵))) ∩ (𝐴 ∩ ((⊥‘𝐴) ∨ (⊥‘𝐶)))) = ((𝐴 ∩ (⊥‘𝐵)) ∩ (𝐴 ∩ (⊥‘𝐶))))
45 inindi 3695 . . . . . . . . 9 (𝐴 ∩ (((⊥‘𝐴) ∨ (⊥‘𝐵)) ∩ ((⊥‘𝐴) ∨ (⊥‘𝐶)))) = ((𝐴 ∩ ((⊥‘𝐴) ∨ (⊥‘𝐵))) ∩ (𝐴 ∩ ((⊥‘𝐴) ∨ (⊥‘𝐶))))
46 inindi 3695 . . . . . . . . 9 (𝐴 ∩ ((⊥‘𝐵) ∩ (⊥‘𝐶))) = ((𝐴 ∩ (⊥‘𝐵)) ∩ (𝐴 ∩ (⊥‘𝐶)))
4744, 45, 463eqtr4g 2573 . . . . . . . 8 (((𝐴C𝐵C𝐶C ) ∧ (𝐴 𝐶 𝐵𝐴 𝐶 𝐶)) → (𝐴 ∩ (((⊥‘𝐴) ∨ (⊥‘𝐵)) ∩ ((⊥‘𝐴) ∨ (⊥‘𝐶)))) = (𝐴 ∩ ((⊥‘𝐵) ∩ (⊥‘𝐶))))
4847ineq2d 3679 . . . . . . 7 (((𝐴C𝐵C𝐶C ) ∧ (𝐴 𝐶 𝐵𝐴 𝐶 𝐶)) → ((𝐵 𝐶) ∩ (𝐴 ∩ (((⊥‘𝐴) ∨ (⊥‘𝐵)) ∩ ((⊥‘𝐴) ∨ (⊥‘𝐶))))) = ((𝐵 𝐶) ∩ (𝐴 ∩ ((⊥‘𝐵) ∩ (⊥‘𝐶)))))
4927, 48syl5eq 2560 . . . . . 6 (((𝐴C𝐵C𝐶C ) ∧ (𝐴 𝐶 𝐵𝐴 𝐶 𝐶)) → (((𝐵 𝐶) ∩ 𝐴) ∩ (((⊥‘𝐴) ∨ (⊥‘𝐵)) ∩ ((⊥‘𝐴) ∨ (⊥‘𝐶)))) = ((𝐵 𝐶) ∩ (𝐴 ∩ ((⊥‘𝐵) ∩ (⊥‘𝐶)))))
50 in12 3689 . . . . . 6 ((𝐵 𝐶) ∩ (𝐴 ∩ ((⊥‘𝐵) ∩ (⊥‘𝐶)))) = (𝐴 ∩ ((𝐵 𝐶) ∩ ((⊥‘𝐵) ∩ (⊥‘𝐶))))
5149, 50syl6eq 2564 . . . . 5 (((𝐴C𝐵C𝐶C ) ∧ (𝐴 𝐶 𝐵𝐴 𝐶 𝐶)) → (((𝐵 𝐶) ∩ 𝐴) ∩ (((⊥‘𝐴) ∨ (⊥‘𝐵)) ∩ ((⊥‘𝐴) ∨ (⊥‘𝐶)))) = (𝐴 ∩ ((𝐵 𝐶) ∩ ((⊥‘𝐵) ∩ (⊥‘𝐶)))))
52 chdmj1 27561 . . . . . . . . . . 11 ((𝐵C𝐶C ) → (⊥‘(𝐵 𝐶)) = ((⊥‘𝐵) ∩ (⊥‘𝐶)))
5352ineq2d 3679 . . . . . . . . . 10 ((𝐵C𝐶C ) → ((𝐵 𝐶) ∩ (⊥‘(𝐵 𝐶))) = ((𝐵 𝐶) ∩ ((⊥‘𝐵) ∩ (⊥‘𝐶))))
54 chocin 27527 . . . . . . . . . . 11 ((𝐵 𝐶) ∈ C → ((𝐵 𝐶) ∩ (⊥‘(𝐵 𝐶))) = 0)
556, 54syl 17 . . . . . . . . . 10 ((𝐵C𝐶C ) → ((𝐵 𝐶) ∩ (⊥‘(𝐵 𝐶))) = 0)
5653, 55eqtr3d 2550 . . . . . . . . 9 ((𝐵C𝐶C ) → ((𝐵 𝐶) ∩ ((⊥‘𝐵) ∩ (⊥‘𝐶))) = 0)
5756ineq2d 3679 . . . . . . . 8 ((𝐵C𝐶C ) → (𝐴 ∩ ((𝐵 𝐶) ∩ ((⊥‘𝐵) ∩ (⊥‘𝐶)))) = (𝐴 ∩ 0))
58 chm0 27523 . . . . . . . 8 (𝐴C → (𝐴 ∩ 0) = 0)
5957, 58sylan9eqr 2570 . . . . . . 7 ((𝐴C ∧ (𝐵C𝐶C )) → (𝐴 ∩ ((𝐵 𝐶) ∩ ((⊥‘𝐵) ∩ (⊥‘𝐶)))) = 0)
60593impb 1251 . . . . . 6 ((𝐴C𝐵C𝐶C ) → (𝐴 ∩ ((𝐵 𝐶) ∩ ((⊥‘𝐵) ∩ (⊥‘𝐶)))) = 0)
6160adantr 479 . . . . 5 (((𝐴C𝐵C𝐶C ) ∧ (𝐴 𝐶 𝐵𝐴 𝐶 𝐶)) → (𝐴 ∩ ((𝐵 𝐶) ∩ ((⊥‘𝐵) ∩ (⊥‘𝐶)))) = 0)
6251, 61eqtrd 2548 . . . 4 (((𝐴C𝐵C𝐶C ) ∧ (𝐴 𝐶 𝐵𝐴 𝐶 𝐶)) → (((𝐵 𝐶) ∩ 𝐴) ∩ (((⊥‘𝐴) ∨ (⊥‘𝐵)) ∩ ((⊥‘𝐴) ∨ (⊥‘𝐶)))) = 0)
6326, 62eqtrd 2548 . . 3 (((𝐴C𝐵C𝐶C ) ∧ (𝐴 𝐶 𝐵𝐴 𝐶 𝐶)) → ((𝐴 ∩ (𝐵 𝐶)) ∩ (⊥‘((𝐴𝐵) ∨ (𝐴𝐶)))) = 0)
64 pjoml 27468 . . 3 (((((𝐴𝐵) ∨ (𝐴𝐶)) ∈ C ∧ (𝐴 ∩ (𝐵 𝐶)) ∈ S ) ∧ (((𝐴𝐵) ∨ (𝐴𝐶)) ⊆ (𝐴 ∩ (𝐵 𝐶)) ∧ ((𝐴 ∩ (𝐵 𝐶)) ∩ (⊥‘((𝐴𝐵) ∨ (𝐴𝐶)))) = 0)) → ((𝐴𝐵) ∨ (𝐴𝐶)) = (𝐴 ∩ (𝐵 𝐶)))
6513, 15, 63, 64syl12anc 1315 . 2 (((𝐴C𝐵C𝐶C ) ∧ (𝐴 𝐶 𝐵𝐴 𝐶 𝐶)) → ((𝐴𝐵) ∨ (𝐴𝐶)) = (𝐴 ∩ (𝐵 𝐶)))
6665eqcomd 2520 1 (((𝐴C𝐵C𝐶C ) ∧ (𝐴 𝐶 𝐵𝐴 𝐶 𝐶)) → (𝐴 ∩ (𝐵 𝐶)) = ((𝐴𝐵) ∨ (𝐴𝐶)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382  w3a 1030   = wceq 1474  wcel 1938  cin 3443  wss 3444   class class class wbr 4481  cfv 5689  (class class class)co 6425   S csh 26958   C cch 26959  cort 26960   chj 26963  0c0h 26965   𝐶 ccm 26966
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-8 1940  ax-9 1947  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-rep 4597  ax-sep 4607  ax-nul 4616  ax-pow 4668  ax-pr 4732  ax-un 6722  ax-inf2 8296  ax-cc 9015  ax-cnex 9746  ax-resscn 9747  ax-1cn 9748  ax-icn 9749  ax-addcl 9750  ax-addrcl 9751  ax-mulcl 9752  ax-mulrcl 9753  ax-mulcom 9754  ax-addass 9755  ax-mulass 9756  ax-distr 9757  ax-i2m1 9758  ax-1ne0 9759  ax-1rid 9760  ax-rnegex 9761  ax-rrecex 9762  ax-cnre 9763  ax-pre-lttri 9764  ax-pre-lttrn 9765  ax-pre-ltadd 9766  ax-pre-mulgt0 9767  ax-pre-sup 9768  ax-addf 9769  ax-mulf 9770  ax-hilex 27029  ax-hfvadd 27030  ax-hvcom 27031  ax-hvass 27032  ax-hv0cl 27033  ax-hvaddid 27034  ax-hfvmul 27035  ax-hvmulid 27036  ax-hvmulass 27037  ax-hvdistr1 27038  ax-hvdistr2 27039  ax-hvmul0 27040  ax-hfi 27109  ax-his1 27112  ax-his2 27113  ax-his3 27114  ax-his4 27115  ax-hcompl 27232
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3or 1031  df-3an 1032  df-tru 1477  df-fal 1480  df-ex 1695  df-nf 1699  df-sb 1831  df-eu 2366  df-mo 2367  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ne 2686  df-nel 2687  df-ral 2805  df-rex 2806  df-reu 2807  df-rmo 2808  df-rab 2809  df-v 3079  df-sbc 3307  df-csb 3404  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-pss 3460  df-nul 3778  df-if 3940  df-pw 4013  df-sn 4029  df-pr 4031  df-tp 4033  df-op 4035  df-uni 4271  df-int 4309  df-iun 4355  df-iin 4356  df-br 4482  df-opab 4542  df-mpt 4543  df-tr 4579  df-eprel 4843  df-id 4847  df-po 4853  df-so 4854  df-fr 4891  df-se 4892  df-we 4893  df-xp 4938  df-rel 4939  df-cnv 4940  df-co 4941  df-dm 4942  df-rn 4943  df-res 4944  df-ima 4945  df-pred 5487  df-ord 5533  df-on 5534  df-lim 5535  df-suc 5536  df-iota 5653  df-fun 5691  df-fn 5692  df-f 5693  df-f1 5694  df-fo 5695  df-f1o 5696  df-fv 5697  df-isom 5698  df-riota 6387  df-ov 6428  df-oprab 6429  df-mpt2 6430  df-of 6670  df-om 6833  df-1st 6933  df-2nd 6934  df-supp 7057  df-wrecs 7168  df-recs 7230  df-rdg 7268  df-1o 7322  df-2o 7323  df-oadd 7326  df-omul 7327  df-er 7504  df-map 7621  df-pm 7622  df-ixp 7670  df-en 7717  df-dom 7718  df-sdom 7719  df-fin 7720  df-fsupp 8034  df-fi 8075  df-sup 8106  df-inf 8107  df-oi 8173  df-card 8523  df-acn 8526  df-cda 8748  df-pnf 9830  df-mnf 9831  df-xr 9832  df-ltxr 9833  df-le 9834  df-sub 10018  df-neg 10019  df-div 10433  df-nn 10775  df-2 10833  df-3 10834  df-4 10835  df-5 10836  df-6 10837  df-7 10838  df-8 10839  df-9 10840  df-n0 11047  df-z 11118  df-dec 11233  df-uz 11427  df-q 11530  df-rp 11574  df-xneg 11687  df-xadd 11688  df-xmul 11689  df-ioo 11918  df-ico 11920  df-icc 11921  df-fz 12065  df-fzo 12202  df-fl 12322  df-seq 12531  df-exp 12590  df-hash 12847  df-cj 13544  df-re 13545  df-im 13546  df-sqrt 13680  df-abs 13681  df-clim 13931  df-rlim 13932  df-sum 14132  df-struct 15579  df-ndx 15580  df-slot 15581  df-base 15582  df-sets 15583  df-ress 15584  df-plusg 15663  df-mulr 15664  df-starv 15665  df-sca 15666  df-vsca 15667  df-ip 15668  df-tset 15669  df-ple 15670  df-ds 15673  df-unif 15674  df-hom 15675  df-cco 15676  df-rest 15788  df-topn 15789  df-0g 15807  df-gsum 15808  df-topgen 15809  df-pt 15810  df-prds 15813  df-xrs 15867  df-qtop 15873  df-imas 15874  df-xps 15877  df-mre 15959  df-mrc 15960  df-acs 15962  df-mgm 16955  df-sgrp 16997  df-mnd 17008  df-submnd 17049  df-mulg 17254  df-cntz 17463  df-cmn 17924  df-psmet 19461  df-xmet 19462  df-met 19463  df-bl 19464  df-mopn 19465  df-fbas 19466  df-fg 19467  df-cnfld 19470  df-top 20422  df-bases 20423  df-topon 20424  df-topsp 20425  df-cld 20534  df-ntr 20535  df-cls 20536  df-nei 20613  df-cn 20742  df-cnp 20743  df-lm 20744  df-haus 20830  df-tx 21076  df-hmeo 21269  df-fil 21361  df-fm 21453  df-flim 21454  df-flf 21455  df-xms 21835  df-ms 21836  df-tms 21837  df-cfil 22726  df-cau 22727  df-cmet 22728  df-grpo 26470  df-gid 26471  df-ginv 26472  df-gdiv 26473  df-ablo 26525  df-vc 26540  df-nv 26588  df-va 26591  df-ba 26592  df-sm 26593  df-0v 26594  df-vs 26595  df-nmcv 26596  df-ims 26597  df-dip 26714  df-ssp 26738  df-ph 26831  df-cbn 26882  df-hnorm 26998  df-hba 26999  df-hvsub 27001  df-hlim 27002  df-hcau 27003  df-sh 27237  df-ch 27251  df-oc 27282  df-ch0 27283  df-shs 27340  df-chj 27342  df-cm 27615
This theorem is referenced by:  cm2j  27652  fh1i  27653  chirredlem3  28424
  Copyright terms: Public domain W3C validator