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

Theorem opsqrlem1 29326
Description: Lemma for opsqri . (Contributed by NM, 9-Aug-2006.) (New usage is discouraged.)
Hypotheses
Ref Expression
opsqrlem1.1 𝑇 ∈ HrmOp
opsqrlem1.2 (normop𝑇) ∈ ℝ
opsqrlem1.3 0hopop 𝑇
opsqrlem1.4 𝑅 = ((1 / (normop𝑇)) ·op 𝑇)
opsqrlem1.5 (𝑇 ≠ 0hop → ∃𝑢 ∈ HrmOp ( 0hopop 𝑢 ∧ (𝑢𝑢) = 𝑅))
Assertion
Ref Expression
opsqrlem1 (𝑇 ≠ 0hop → ∃𝑣 ∈ HrmOp ( 0hopop 𝑣 ∧ (𝑣𝑣) = 𝑇))
Distinct variable group:   𝑣,𝑢,𝑇
Allowed substitution hints:   𝑅(𝑣,𝑢)

Proof of Theorem opsqrlem1
StepHypRef Expression
1 opsqrlem1.1 . . . . . . . 8 𝑇 ∈ HrmOp
2 hmopf 29060 . . . . . . . 8 (𝑇 ∈ HrmOp → 𝑇: ℋ⟶ ℋ)
31, 2ax-mp 5 . . . . . . 7 𝑇: ℋ⟶ ℋ
4 nmopge0 29097 . . . . . . 7 (𝑇: ℋ⟶ ℋ → 0 ≤ (normop𝑇))
53, 4ax-mp 5 . . . . . 6 0 ≤ (normop𝑇)
6 opsqrlem1.2 . . . . . . 7 (normop𝑇) ∈ ℝ
76sqrtcli 14330 . . . . . 6 (0 ≤ (normop𝑇) → (√‘(normop𝑇)) ∈ ℝ)
85, 7ax-mp 5 . . . . 5 (√‘(normop𝑇)) ∈ ℝ
9 hmopm 29207 . . . . 5 (((√‘(normop𝑇)) ∈ ℝ ∧ 𝑢 ∈ HrmOp) → ((√‘(normop𝑇)) ·op 𝑢) ∈ HrmOp)
108, 9mpan 673 . . . 4 (𝑢 ∈ HrmOp → ((√‘(normop𝑇)) ·op 𝑢) ∈ HrmOp)
1110ad2antlr 709 . . 3 (((𝑇 ≠ 0hop𝑢 ∈ HrmOp) ∧ ( 0hopop 𝑢 ∧ (𝑢𝑢) = 𝑅)) → ((√‘(normop𝑇)) ·op 𝑢) ∈ HrmOp)
126sqrtge0i 14335 . . . . . . 7 (0 ≤ (normop𝑇) → 0 ≤ (√‘(normop𝑇)))
135, 12ax-mp 5 . . . . . 6 0 ≤ (√‘(normop𝑇))
14 leopmuli 29319 . . . . . 6 ((((√‘(normop𝑇)) ∈ ℝ ∧ 𝑢 ∈ HrmOp) ∧ (0 ≤ (√‘(normop𝑇)) ∧ 0hopop 𝑢)) → 0hopop ((√‘(normop𝑇)) ·op 𝑢))
1513, 14mpanr1 686 . . . . 5 ((((√‘(normop𝑇)) ∈ ℝ ∧ 𝑢 ∈ HrmOp) ∧ 0hopop 𝑢) → 0hopop ((√‘(normop𝑇)) ·op 𝑢))
168, 15mpanl1 683 . . . 4 ((𝑢 ∈ HrmOp ∧ 0hopop 𝑢) → 0hopop ((√‘(normop𝑇)) ·op 𝑢))
1716ad2ant2lr 745 . . 3 (((𝑇 ≠ 0hop𝑢 ∈ HrmOp) ∧ ( 0hopop 𝑢 ∧ (𝑢𝑢) = 𝑅)) → 0hopop ((√‘(normop𝑇)) ·op 𝑢))
18 hmopf 29060 . . . . . . . 8 (𝑢 ∈ HrmOp → 𝑢: ℋ⟶ ℋ)
198recni 10335 . . . . . . . . . 10 (√‘(normop𝑇)) ∈ ℂ
20 homulcl 28945 . . . . . . . . . 10 (((√‘(normop𝑇)) ∈ ℂ ∧ 𝑢: ℋ⟶ ℋ) → ((√‘(normop𝑇)) ·op 𝑢): ℋ⟶ ℋ)
2119, 20mpan 673 . . . . . . . . 9 (𝑢: ℋ⟶ ℋ → ((√‘(normop𝑇)) ·op 𝑢): ℋ⟶ ℋ)
2218, 21syl 17 . . . . . . . 8 (𝑢 ∈ HrmOp → ((√‘(normop𝑇)) ·op 𝑢): ℋ⟶ ℋ)
23 homco1 28987 . . . . . . . . 9 (((√‘(normop𝑇)) ∈ ℂ ∧ 𝑢: ℋ⟶ ℋ ∧ ((√‘(normop𝑇)) ·op 𝑢): ℋ⟶ ℋ) → (((√‘(normop𝑇)) ·op 𝑢) ∘ ((√‘(normop𝑇)) ·op 𝑢)) = ((√‘(normop𝑇)) ·op (𝑢 ∘ ((√‘(normop𝑇)) ·op 𝑢))))
2419, 23mp3an1 1565 . . . . . . . 8 ((𝑢: ℋ⟶ ℋ ∧ ((√‘(normop𝑇)) ·op 𝑢): ℋ⟶ ℋ) → (((√‘(normop𝑇)) ·op 𝑢) ∘ ((√‘(normop𝑇)) ·op 𝑢)) = ((√‘(normop𝑇)) ·op (𝑢 ∘ ((√‘(normop𝑇)) ·op 𝑢))))
2518, 22, 24syl2anc 575 . . . . . . 7 (𝑢 ∈ HrmOp → (((√‘(normop𝑇)) ·op 𝑢) ∘ ((√‘(normop𝑇)) ·op 𝑢)) = ((√‘(normop𝑇)) ·op (𝑢 ∘ ((√‘(normop𝑇)) ·op 𝑢))))
26 hmoplin 29128 . . . . . . . . 9 (𝑢 ∈ HrmOp → 𝑢 ∈ LinOp)
27 homco2 29163 . . . . . . . . . 10 (((√‘(normop𝑇)) ∈ ℂ ∧ 𝑢 ∈ LinOp ∧ 𝑢: ℋ⟶ ℋ) → (𝑢 ∘ ((√‘(normop𝑇)) ·op 𝑢)) = ((√‘(normop𝑇)) ·op (𝑢𝑢)))
2819, 27mp3an1 1565 . . . . . . . . 9 ((𝑢 ∈ LinOp ∧ 𝑢: ℋ⟶ ℋ) → (𝑢 ∘ ((√‘(normop𝑇)) ·op 𝑢)) = ((√‘(normop𝑇)) ·op (𝑢𝑢)))
2926, 18, 28syl2anc 575 . . . . . . . 8 (𝑢 ∈ HrmOp → (𝑢 ∘ ((√‘(normop𝑇)) ·op 𝑢)) = ((√‘(normop𝑇)) ·op (𝑢𝑢)))
3029oveq2d 6886 . . . . . . 7 (𝑢 ∈ HrmOp → ((√‘(normop𝑇)) ·op (𝑢 ∘ ((√‘(normop𝑇)) ·op 𝑢))) = ((√‘(normop𝑇)) ·op ((√‘(normop𝑇)) ·op (𝑢𝑢))))
316sqrtthi 14329 . . . . . . . . . 10 (0 ≤ (normop𝑇) → ((√‘(normop𝑇)) · (√‘(normop𝑇))) = (normop𝑇))
325, 31ax-mp 5 . . . . . . . . 9 ((√‘(normop𝑇)) · (√‘(normop𝑇))) = (normop𝑇)
3332oveq1i 6880 . . . . . . . 8 (((√‘(normop𝑇)) · (√‘(normop𝑇))) ·op (𝑢𝑢)) = ((normop𝑇) ·op (𝑢𝑢))
34 fco 6269 . . . . . . . . . 10 ((𝑢: ℋ⟶ ℋ ∧ 𝑢: ℋ⟶ ℋ) → (𝑢𝑢): ℋ⟶ ℋ)
3518, 18, 34syl2anc 575 . . . . . . . . 9 (𝑢 ∈ HrmOp → (𝑢𝑢): ℋ⟶ ℋ)
36 homulass 28988 . . . . . . . . . 10 (((√‘(normop𝑇)) ∈ ℂ ∧ (√‘(normop𝑇)) ∈ ℂ ∧ (𝑢𝑢): ℋ⟶ ℋ) → (((√‘(normop𝑇)) · (√‘(normop𝑇))) ·op (𝑢𝑢)) = ((√‘(normop𝑇)) ·op ((√‘(normop𝑇)) ·op (𝑢𝑢))))
3719, 19, 36mp3an12 1568 . . . . . . . . 9 ((𝑢𝑢): ℋ⟶ ℋ → (((√‘(normop𝑇)) · (√‘(normop𝑇))) ·op (𝑢𝑢)) = ((√‘(normop𝑇)) ·op ((√‘(normop𝑇)) ·op (𝑢𝑢))))
3835, 37syl 17 . . . . . . . 8 (𝑢 ∈ HrmOp → (((√‘(normop𝑇)) · (√‘(normop𝑇))) ·op (𝑢𝑢)) = ((√‘(normop𝑇)) ·op ((√‘(normop𝑇)) ·op (𝑢𝑢))))
3933, 38syl5reqr 2855 . . . . . . 7 (𝑢 ∈ HrmOp → ((√‘(normop𝑇)) ·op ((√‘(normop𝑇)) ·op (𝑢𝑢))) = ((normop𝑇) ·op (𝑢𝑢)))
4025, 30, 393eqtrd 2844 . . . . . 6 (𝑢 ∈ HrmOp → (((√‘(normop𝑇)) ·op 𝑢) ∘ ((√‘(normop𝑇)) ·op 𝑢)) = ((normop𝑇) ·op (𝑢𝑢)))
4140ad2antlr 709 . . . . 5 (((𝑇 ≠ 0hop𝑢 ∈ HrmOp) ∧ (𝑢𝑢) = 𝑅) → (((√‘(normop𝑇)) ·op 𝑢) ∘ ((√‘(normop𝑇)) ·op 𝑢)) = ((normop𝑇) ·op (𝑢𝑢)))
42 id 22 . . . . . . . . 9 ((𝑢𝑢) = 𝑅 → (𝑢𝑢) = 𝑅)
43 opsqrlem1.4 . . . . . . . . 9 𝑅 = ((1 / (normop𝑇)) ·op 𝑇)
4442, 43syl6eq 2856 . . . . . . . 8 ((𝑢𝑢) = 𝑅 → (𝑢𝑢) = ((1 / (normop𝑇)) ·op 𝑇))
4544oveq2d 6886 . . . . . . 7 ((𝑢𝑢) = 𝑅 → ((normop𝑇) ·op (𝑢𝑢)) = ((normop𝑇) ·op ((1 / (normop𝑇)) ·op 𝑇)))
46 hmoplin 29128 . . . . . . . . . . . 12 (𝑇 ∈ HrmOp → 𝑇 ∈ LinOp)
471, 46ax-mp 5 . . . . . . . . . . 11 𝑇 ∈ LinOp
48 nmlnopne0 29185 . . . . . . . . . . 11 (𝑇 ∈ LinOp → ((normop𝑇) ≠ 0 ↔ 𝑇 ≠ 0hop ))
4947, 48ax-mp 5 . . . . . . . . . 10 ((normop𝑇) ≠ 0 ↔ 𝑇 ≠ 0hop )
506recni 10335 . . . . . . . . . . 11 (normop𝑇) ∈ ℂ
5150recidzi 11033 . . . . . . . . . 10 ((normop𝑇) ≠ 0 → ((normop𝑇) · (1 / (normop𝑇))) = 1)
5249, 51sylbir 226 . . . . . . . . 9 (𝑇 ≠ 0hop → ((normop𝑇) · (1 / (normop𝑇))) = 1)
5352oveq1d 6885 . . . . . . . 8 (𝑇 ≠ 0hop → (((normop𝑇) · (1 / (normop𝑇))) ·op 𝑇) = (1 ·op 𝑇))
546rerecclzi 11070 . . . . . . . . . . 11 ((normop𝑇) ≠ 0 → (1 / (normop𝑇)) ∈ ℝ)
5549, 54sylbir 226 . . . . . . . . . 10 (𝑇 ≠ 0hop → (1 / (normop𝑇)) ∈ ℝ)
5655recnd 10349 . . . . . . . . 9 (𝑇 ≠ 0hop → (1 / (normop𝑇)) ∈ ℂ)
57 homulass 28988 . . . . . . . . . 10 (((normop𝑇) ∈ ℂ ∧ (1 / (normop𝑇)) ∈ ℂ ∧ 𝑇: ℋ⟶ ℋ) → (((normop𝑇) · (1 / (normop𝑇))) ·op 𝑇) = ((normop𝑇) ·op ((1 / (normop𝑇)) ·op 𝑇)))
5850, 3, 57mp3an13 1569 . . . . . . . . 9 ((1 / (normop𝑇)) ∈ ℂ → (((normop𝑇) · (1 / (normop𝑇))) ·op 𝑇) = ((normop𝑇) ·op ((1 / (normop𝑇)) ·op 𝑇)))
5956, 58syl 17 . . . . . . . 8 (𝑇 ≠ 0hop → (((normop𝑇) · (1 / (normop𝑇))) ·op 𝑇) = ((normop𝑇) ·op ((1 / (normop𝑇)) ·op 𝑇)))
60 homulid2 28986 . . . . . . . . 9 (𝑇: ℋ⟶ ℋ → (1 ·op 𝑇) = 𝑇)
613, 60mp1i 13 . . . . . . . 8 (𝑇 ≠ 0hop → (1 ·op 𝑇) = 𝑇)
6253, 59, 613eqtr3d 2848 . . . . . . 7 (𝑇 ≠ 0hop → ((normop𝑇) ·op ((1 / (normop𝑇)) ·op 𝑇)) = 𝑇)
6345, 62sylan9eqr 2862 . . . . . 6 ((𝑇 ≠ 0hop ∧ (𝑢𝑢) = 𝑅) → ((normop𝑇) ·op (𝑢𝑢)) = 𝑇)
6463adantlr 697 . . . . 5 (((𝑇 ≠ 0hop𝑢 ∈ HrmOp) ∧ (𝑢𝑢) = 𝑅) → ((normop𝑇) ·op (𝑢𝑢)) = 𝑇)
6541, 64eqtrd 2840 . . . 4 (((𝑇 ≠ 0hop𝑢 ∈ HrmOp) ∧ (𝑢𝑢) = 𝑅) → (((√‘(normop𝑇)) ·op 𝑢) ∘ ((√‘(normop𝑇)) ·op 𝑢)) = 𝑇)
6665adantrl 698 . . 3 (((𝑇 ≠ 0hop𝑢 ∈ HrmOp) ∧ ( 0hopop 𝑢 ∧ (𝑢𝑢) = 𝑅)) → (((√‘(normop𝑇)) ·op 𝑢) ∘ ((√‘(normop𝑇)) ·op 𝑢)) = 𝑇)
67 breq2 4848 . . . . 5 (𝑣 = ((√‘(normop𝑇)) ·op 𝑢) → ( 0hopop 𝑣 ↔ 0hopop ((√‘(normop𝑇)) ·op 𝑢)))
68 coeq1 5481 . . . . . . 7 (𝑣 = ((√‘(normop𝑇)) ·op 𝑢) → (𝑣𝑣) = (((√‘(normop𝑇)) ·op 𝑢) ∘ 𝑣))
69 coeq2 5482 . . . . . . 7 (𝑣 = ((√‘(normop𝑇)) ·op 𝑢) → (((√‘(normop𝑇)) ·op 𝑢) ∘ 𝑣) = (((√‘(normop𝑇)) ·op 𝑢) ∘ ((√‘(normop𝑇)) ·op 𝑢)))
7068, 69eqtrd 2840 . . . . . 6 (𝑣 = ((√‘(normop𝑇)) ·op 𝑢) → (𝑣𝑣) = (((√‘(normop𝑇)) ·op 𝑢) ∘ ((√‘(normop𝑇)) ·op 𝑢)))
7170eqeq1d 2808 . . . . 5 (𝑣 = ((√‘(normop𝑇)) ·op 𝑢) → ((𝑣𝑣) = 𝑇 ↔ (((√‘(normop𝑇)) ·op 𝑢) ∘ ((√‘(normop𝑇)) ·op 𝑢)) = 𝑇))
7267, 71anbi12d 618 . . . 4 (𝑣 = ((√‘(normop𝑇)) ·op 𝑢) → (( 0hopop 𝑣 ∧ (𝑣𝑣) = 𝑇) ↔ ( 0hopop ((√‘(normop𝑇)) ·op 𝑢) ∧ (((√‘(normop𝑇)) ·op 𝑢) ∘ ((√‘(normop𝑇)) ·op 𝑢)) = 𝑇)))
7372rspcev 3502 . . 3 ((((√‘(normop𝑇)) ·op 𝑢) ∈ HrmOp ∧ ( 0hopop ((√‘(normop𝑇)) ·op 𝑢) ∧ (((√‘(normop𝑇)) ·op 𝑢) ∘ ((√‘(normop𝑇)) ·op 𝑢)) = 𝑇)) → ∃𝑣 ∈ HrmOp ( 0hopop 𝑣 ∧ (𝑣𝑣) = 𝑇))
7411, 17, 66, 73syl12anc 856 . 2 (((𝑇 ≠ 0hop𝑢 ∈ HrmOp) ∧ ( 0hopop 𝑢 ∧ (𝑢𝑢) = 𝑅)) → ∃𝑣 ∈ HrmOp ( 0hopop 𝑣 ∧ (𝑣𝑣) = 𝑇))
75 opsqrlem1.5 . 2 (𝑇 ≠ 0hop → ∃𝑢 ∈ HrmOp ( 0hopop 𝑢 ∧ (𝑢𝑢) = 𝑅))
7674, 75r19.29a 3266 1 (𝑇 ≠ 0hop → ∃𝑣 ∈ HrmOp ( 0hopop 𝑣 ∧ (𝑣𝑣) = 𝑇))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384   = wceq 1637  wcel 2156  wne 2978  wrex 3097   class class class wbr 4844  ccom 5315  wf 6093  cfv 6097  (class class class)co 6870  cc 10215  cr 10216  0cc0 10217  1c1 10218   · cmul 10222  cle 10356   / cdiv 10965  csqrt 14192  chil 28103   ·op chot 28123   0hop ch0o 28127  normopcnop 28129  LinOpclo 28131  HrmOpcho 28134  op cleo 28142
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-8 2158  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-rep 4964  ax-sep 4975  ax-nul 4983  ax-pow 5035  ax-pr 5096  ax-un 7175  ax-inf2 8781  ax-cc 9538  ax-cnex 10273  ax-resscn 10274  ax-1cn 10275  ax-icn 10276  ax-addcl 10277  ax-addrcl 10278  ax-mulcl 10279  ax-mulrcl 10280  ax-mulcom 10281  ax-addass 10282  ax-mulass 10283  ax-distr 10284  ax-i2m1 10285  ax-1ne0 10286  ax-1rid 10287  ax-rnegex 10288  ax-rrecex 10289  ax-cnre 10290  ax-pre-lttri 10291  ax-pre-lttrn 10292  ax-pre-ltadd 10293  ax-pre-mulgt0 10294  ax-pre-sup 10295  ax-addf 10296  ax-mulf 10297  ax-hilex 28183  ax-hfvadd 28184  ax-hvcom 28185  ax-hvass 28186  ax-hv0cl 28187  ax-hvaddid 28188  ax-hfvmul 28189  ax-hvmulid 28190  ax-hvmulass 28191  ax-hvdistr1 28192  ax-hvdistr2 28193  ax-hvmul0 28194  ax-hfi 28263  ax-his1 28266  ax-his2 28267  ax-his3 28268  ax-his4 28269  ax-hcompl 28386
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-fal 1651  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ne 2979  df-nel 3082  df-ral 3101  df-rex 3102  df-reu 3103  df-rmo 3104  df-rab 3105  df-v 3393  df-sbc 3634  df-csb 3729  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-pss 3785  df-nul 4117  df-if 4280  df-pw 4353  df-sn 4371  df-pr 4373  df-tp 4375  df-op 4377  df-uni 4631  df-int 4670  df-iun 4714  df-iin 4715  df-br 4845  df-opab 4907  df-mpt 4924  df-tr 4947  df-id 5219  df-eprel 5224  df-po 5232  df-so 5233  df-fr 5270  df-se 5271  df-we 5272  df-xp 5317  df-rel 5318  df-cnv 5319  df-co 5320  df-dm 5321  df-rn 5322  df-res 5323  df-ima 5324  df-pred 5893  df-ord 5939  df-on 5940  df-lim 5941  df-suc 5942  df-iota 6060  df-fun 6099  df-fn 6100  df-f 6101  df-f1 6102  df-fo 6103  df-f1o 6104  df-fv 6105  df-isom 6106  df-riota 6831  df-ov 6873  df-oprab 6874  df-mpt2 6875  df-of 7123  df-om 7292  df-1st 7394  df-2nd 7395  df-supp 7526  df-wrecs 7638  df-recs 7700  df-rdg 7738  df-1o 7792  df-2o 7793  df-oadd 7796  df-omul 7797  df-er 7975  df-map 8090  df-pm 8091  df-ixp 8142  df-en 8189  df-dom 8190  df-sdom 8191  df-fin 8192  df-fsupp 8511  df-fi 8552  df-sup 8583  df-inf 8584  df-oi 8650  df-card 9044  df-acn 9047  df-cda 9271  df-pnf 10357  df-mnf 10358  df-xr 10359  df-ltxr 10360  df-le 10361  df-sub 10549  df-neg 10550  df-div 10966  df-nn 11302  df-2 11360  df-3 11361  df-4 11362  df-5 11363  df-6 11364  df-7 11365  df-8 11366  df-9 11367  df-n0 11556  df-z 11640  df-dec 11756  df-uz 11901  df-q 12004  df-rp 12043  df-xneg 12158  df-xadd 12159  df-xmul 12160  df-ioo 12393  df-ico 12395  df-icc 12396  df-fz 12546  df-fzo 12686  df-fl 12813  df-seq 13021  df-exp 13080  df-hash 13334  df-cj 14058  df-re 14059  df-im 14060  df-sqrt 14194  df-abs 14195  df-clim 14438  df-rlim 14439  df-sum 14636  df-struct 16066  df-ndx 16067  df-slot 16068  df-base 16070  df-sets 16071  df-ress 16072  df-plusg 16162  df-mulr 16163  df-starv 16164  df-sca 16165  df-vsca 16166  df-ip 16167  df-tset 16168  df-ple 16169  df-ds 16171  df-unif 16172  df-hom 16173  df-cco 16174  df-rest 16284  df-topn 16285  df-0g 16303  df-gsum 16304  df-topgen 16305  df-pt 16306  df-prds 16309  df-xrs 16363  df-qtop 16368  df-imas 16369  df-xps 16371  df-mre 16447  df-mrc 16448  df-acs 16450  df-mgm 17443  df-sgrp 17485  df-mnd 17496  df-submnd 17537  df-mulg 17742  df-cntz 17947  df-cmn 18392  df-psmet 19942  df-xmet 19943  df-met 19944  df-bl 19945  df-mopn 19946  df-fbas 19947  df-fg 19948  df-cnfld 19951  df-top 20909  df-topon 20926  df-topsp 20948  df-bases 20961  df-cld 21034  df-ntr 21035  df-cls 21036  df-nei 21113  df-cn 21242  df-cnp 21243  df-lm 21244  df-haus 21330  df-tx 21576  df-hmeo 21769  df-fil 21860  df-fm 21952  df-flim 21953  df-flf 21954  df-xms 22335  df-ms 22336  df-tms 22337  df-cfil 23263  df-cau 23264  df-cmet 23265  df-grpo 27675  df-gid 27676  df-ginv 27677  df-gdiv 27678  df-ablo 27727  df-vc 27741  df-nv 27774  df-va 27777  df-ba 27778  df-sm 27779  df-0v 27780  df-vs 27781  df-nmcv 27782  df-ims 27783  df-dip 27883  df-ssp 27904  df-lno 27926  df-nmoo 27927  df-0o 27929  df-ph 27995  df-cbn 28046  df-hnorm 28152  df-hba 28153  df-hvsub 28155  df-hlim 28156  df-hcau 28157  df-sh 28391  df-ch 28405  df-oc 28436  df-ch0 28437  df-shs 28494  df-pjh 28581  df-hosum 28916  df-homul 28917  df-hodif 28918  df-h0op 28934  df-nmop 29025  df-lnop 29027  df-hmop 29030  df-leop 29038
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator