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

Theorem spansncvi 28850
Description: Hilbert space has the covering property (using spans of singletons to represent atoms). Exercise 5 of [Kalmbach] p. 153. (Contributed by NM, 7-Jun-2004.) (New usage is discouraged.)
Hypotheses
Ref Expression
spansncv.1 𝐴C
spansncv.2 𝐵C
spansncv.3 𝐶 ∈ ℋ
Assertion
Ref Expression
spansncvi ((𝐴𝐵𝐵 ⊆ (𝐴 (span‘{𝐶}))) → 𝐵 = (𝐴 (span‘{𝐶})))

Proof of Theorem spansncvi
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpr 471 . 2 ((𝐴𝐵𝐵 ⊆ (𝐴 (span‘{𝐶}))) → 𝐵 ⊆ (𝐴 (span‘{𝐶})))
2 pssss 3852 . . . 4 (𝐴𝐵𝐴𝐵)
32adantr 466 . . 3 ((𝐴𝐵𝐵 ⊆ (𝐴 (span‘{𝐶}))) → 𝐴𝐵)
4 pssnel 4182 . . . . . . 7 (𝐴𝐵 → ∃𝑥(𝑥𝐵 ∧ ¬ 𝑥𝐴))
5 ssel2 3747 . . . . . . . . . . . 12 ((𝐵 ⊆ (𝐴 (span‘{𝐶})) ∧ 𝑥𝐵) → 𝑥 ∈ (𝐴 (span‘{𝐶})))
6 spansncv.1 . . . . . . . . . . . . . . . 16 𝐴C
7 spansncv.3 . . . . . . . . . . . . . . . 16 𝐶 ∈ ℋ
86, 7spansnji 28844 . . . . . . . . . . . . . . 15 (𝐴 + (span‘{𝐶})) = (𝐴 (span‘{𝐶}))
98eleq2i 2842 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝐴 + (span‘{𝐶})) ↔ 𝑥 ∈ (𝐴 (span‘{𝐶})))
107spansnchi 28760 . . . . . . . . . . . . . . 15 (span‘{𝐶}) ∈ C
116, 10chseli 28657 . . . . . . . . . . . . . 14 (𝑥 ∈ (𝐴 + (span‘{𝐶})) ↔ ∃𝑦𝐴𝑧 ∈ (span‘{𝐶})𝑥 = (𝑦 + 𝑧))
129, 11bitr3i 266 . . . . . . . . . . . . 13 (𝑥 ∈ (𝐴 (span‘{𝐶})) ↔ ∃𝑦𝐴𝑧 ∈ (span‘{𝐶})𝑥 = (𝑦 + 𝑧))
13 eleq1 2838 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑥 = (𝑦 + 𝑧) → (𝑥𝐵 ↔ (𝑦 + 𝑧) ∈ 𝐵))
1413biimpac 464 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑥𝐵𝑥 = (𝑦 + 𝑧)) → (𝑦 + 𝑧) ∈ 𝐵)
152sselda 3752 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐴𝐵𝑦𝐴) → 𝑦𝐵)
16 spansncv.2 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 𝐵C
1716chshii 28423 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 𝐵S
18 shsubcl 28416 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((𝐵S ∧ (𝑦 + 𝑧) ∈ 𝐵𝑦𝐵) → ((𝑦 + 𝑧) − 𝑦) ∈ 𝐵)
1917, 18mp3an1 1559 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((𝑦 + 𝑧) ∈ 𝐵𝑦𝐵) → ((𝑦 + 𝑧) − 𝑦) ∈ 𝐵)
2014, 15, 19syl2an 583 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((𝑥𝐵𝑥 = (𝑦 + 𝑧)) ∧ (𝐴𝐵𝑦𝐴)) → ((𝑦 + 𝑧) − 𝑦) ∈ 𝐵)
2120exp43 423 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑥𝐵 → (𝑥 = (𝑦 + 𝑧) → (𝐴𝐵 → (𝑦𝐴 → ((𝑦 + 𝑧) − 𝑦) ∈ 𝐵))))
2221com14 96 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑦𝐴 → (𝑥 = (𝑦 + 𝑧) → (𝐴𝐵 → (𝑥𝐵 → ((𝑦 + 𝑧) − 𝑦) ∈ 𝐵))))
2322imp45 416 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦𝐴 ∧ (𝑥 = (𝑦 + 𝑧) ∧ (𝐴𝐵𝑥𝐵))) → ((𝑦 + 𝑧) − 𝑦) ∈ 𝐵)
246cheli 28428 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑦𝐴𝑦 ∈ ℋ)
2510cheli 28428 . . . . . . . . . . . . . . . . . . . . . . . 24 (𝑧 ∈ (span‘{𝐶}) → 𝑧 ∈ ℋ)
26 hvpncan2 28236 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑦 ∈ ℋ ∧ 𝑧 ∈ ℋ) → ((𝑦 + 𝑧) − 𝑦) = 𝑧)
2724, 25, 26syl2an 583 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦𝐴𝑧 ∈ (span‘{𝐶})) → ((𝑦 + 𝑧) − 𝑦) = 𝑧)
2827eleq1d 2835 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦𝐴𝑧 ∈ (span‘{𝐶})) → (((𝑦 + 𝑧) − 𝑦) ∈ 𝐵𝑧𝐵))
2923, 28syl5ib 234 . . . . . . . . . . . . . . . . . . . . 21 ((𝑦𝐴𝑧 ∈ (span‘{𝐶})) → ((𝑦𝐴 ∧ (𝑥 = (𝑦 + 𝑧) ∧ (𝐴𝐵𝑥𝐵))) → 𝑧𝐵))
3029imp 393 . . . . . . . . . . . . . . . . . . . 20 (((𝑦𝐴𝑧 ∈ (span‘{𝐶})) ∧ (𝑦𝐴 ∧ (𝑥 = (𝑦 + 𝑧) ∧ (𝐴𝐵𝑥𝐵)))) → 𝑧𝐵)
3130anandis 657 . . . . . . . . . . . . . . . . . . 19 ((𝑦𝐴 ∧ (𝑧 ∈ (span‘{𝐶}) ∧ (𝑥 = (𝑦 + 𝑧) ∧ (𝐴𝐵𝑥𝐵)))) → 𝑧𝐵)
3231exp45 425 . . . . . . . . . . . . . . . . . 18 (𝑦𝐴 → (𝑧 ∈ (span‘{𝐶}) → (𝑥 = (𝑦 + 𝑧) → ((𝐴𝐵𝑥𝐵) → 𝑧𝐵))))
3332imp41 412 . . . . . . . . . . . . . . . . 17 ((((𝑦𝐴𝑧 ∈ (span‘{𝐶})) ∧ 𝑥 = (𝑦 + 𝑧)) ∧ (𝐴𝐵𝑥𝐵)) → 𝑧𝐵)
3433adantrr 696 . . . . . . . . . . . . . . . 16 ((((𝑦𝐴𝑧 ∈ (span‘{𝐶})) ∧ 𝑥 = (𝑦 + 𝑧)) ∧ ((𝐴𝐵𝑥𝐵) ∧ ¬ 𝑥𝐴)) → 𝑧𝐵)
35 oveq2 6803 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑧 = 0 → (𝑦 + 𝑧) = (𝑦 + 0))
36 ax-hvaddid 28200 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 (𝑦 ∈ ℋ → (𝑦 + 0) = 𝑦)
3724, 36syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (𝑦𝐴 → (𝑦 + 0) = 𝑦)
3835, 37sylan9eqr 2827 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝑦𝐴𝑧 = 0) → (𝑦 + 𝑧) = 𝑦)
3938eqeq2d 2781 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑦𝐴𝑧 = 0) → (𝑥 = (𝑦 + 𝑧) ↔ 𝑥 = 𝑦))
40 eleq1a 2845 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (𝑦𝐴 → (𝑥 = 𝑦𝑥𝐴))
4140adantr 466 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((𝑦𝐴𝑧 = 0) → (𝑥 = 𝑦𝑥𝐴))
4239, 41sylbid 230 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑦𝐴𝑧 = 0) → (𝑥 = (𝑦 + 𝑧) → 𝑥𝐴))
4342impancom 439 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑦𝐴𝑥 = (𝑦 + 𝑧)) → (𝑧 = 0𝑥𝐴))
4443necon3bd 2957 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑦𝐴𝑥 = (𝑦 + 𝑧)) → (¬ 𝑥𝐴𝑧 ≠ 0))
4544imp 393 . . . . . . . . . . . . . . . . . . . . 21 (((𝑦𝐴𝑥 = (𝑦 + 𝑧)) ∧ ¬ 𝑥𝐴) → 𝑧 ≠ 0)
46 spansnss 28769 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝐵S𝑧𝐵) → (span‘{𝑧}) ⊆ 𝐵)
4717, 46mpan 670 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑧𝐵 → (span‘{𝑧}) ⊆ 𝐵)
48 spansneleq 28768 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((𝐶 ∈ ℋ ∧ 𝑧 ≠ 0) → (𝑧 ∈ (span‘{𝐶}) → (span‘{𝑧}) = (span‘{𝐶})))
497, 48mpan 670 . . . . . . . . . . . . . . . . . . . . . . . . 25 (𝑧 ≠ 0 → (𝑧 ∈ (span‘{𝐶}) → (span‘{𝑧}) = (span‘{𝐶})))
5049imp 393 . . . . . . . . . . . . . . . . . . . . . . . 24 ((𝑧 ≠ 0𝑧 ∈ (span‘{𝐶})) → (span‘{𝑧}) = (span‘{𝐶}))
5150sseq1d 3781 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑧 ≠ 0𝑧 ∈ (span‘{𝐶})) → ((span‘{𝑧}) ⊆ 𝐵 ↔ (span‘{𝐶}) ⊆ 𝐵))
5247, 51syl5ib 234 . . . . . . . . . . . . . . . . . . . . . 22 ((𝑧 ≠ 0𝑧 ∈ (span‘{𝐶})) → (𝑧𝐵 → (span‘{𝐶}) ⊆ 𝐵))
5352ancoms 446 . . . . . . . . . . . . . . . . . . . . 21 ((𝑧 ∈ (span‘{𝐶}) ∧ 𝑧 ≠ 0) → (𝑧𝐵 → (span‘{𝐶}) ⊆ 𝐵))
5445, 53sylan2 580 . . . . . . . . . . . . . . . . . . . 20 ((𝑧 ∈ (span‘{𝐶}) ∧ ((𝑦𝐴𝑥 = (𝑦 + 𝑧)) ∧ ¬ 𝑥𝐴)) → (𝑧𝐵 → (span‘{𝐶}) ⊆ 𝐵))
5554exp44 424 . . . . . . . . . . . . . . . . . . 19 (𝑧 ∈ (span‘{𝐶}) → (𝑦𝐴 → (𝑥 = (𝑦 + 𝑧) → (¬ 𝑥𝐴 → (𝑧𝐵 → (span‘{𝐶}) ⊆ 𝐵)))))
5655com12 32 . . . . . . . . . . . . . . . . . 18 (𝑦𝐴 → (𝑧 ∈ (span‘{𝐶}) → (𝑥 = (𝑦 + 𝑧) → (¬ 𝑥𝐴 → (𝑧𝐵 → (span‘{𝐶}) ⊆ 𝐵)))))
5756imp41 412 . . . . . . . . . . . . . . . . 17 ((((𝑦𝐴𝑧 ∈ (span‘{𝐶})) ∧ 𝑥 = (𝑦 + 𝑧)) ∧ ¬ 𝑥𝐴) → (𝑧𝐵 → (span‘{𝐶}) ⊆ 𝐵))
5857adantrl 695 . . . . . . . . . . . . . . . 16 ((((𝑦𝐴𝑧 ∈ (span‘{𝐶})) ∧ 𝑥 = (𝑦 + 𝑧)) ∧ ((𝐴𝐵𝑥𝐵) ∧ ¬ 𝑥𝐴)) → (𝑧𝐵 → (span‘{𝐶}) ⊆ 𝐵))
5934, 58mpd 15 . . . . . . . . . . . . . . 15 ((((𝑦𝐴𝑧 ∈ (span‘{𝐶})) ∧ 𝑥 = (𝑦 + 𝑧)) ∧ ((𝐴𝐵𝑥𝐵) ∧ ¬ 𝑥𝐴)) → (span‘{𝐶}) ⊆ 𝐵)
6059exp43 423 . . . . . . . . . . . . . 14 ((𝑦𝐴𝑧 ∈ (span‘{𝐶})) → (𝑥 = (𝑦 + 𝑧) → ((𝐴𝐵𝑥𝐵) → (¬ 𝑥𝐴 → (span‘{𝐶}) ⊆ 𝐵))))
6160rexlimivv 3184 . . . . . . . . . . . . 13 (∃𝑦𝐴𝑧 ∈ (span‘{𝐶})𝑥 = (𝑦 + 𝑧) → ((𝐴𝐵𝑥𝐵) → (¬ 𝑥𝐴 → (span‘{𝐶}) ⊆ 𝐵)))
6212, 61sylbi 207 . . . . . . . . . . . 12 (𝑥 ∈ (𝐴 (span‘{𝐶})) → ((𝐴𝐵𝑥𝐵) → (¬ 𝑥𝐴 → (span‘{𝐶}) ⊆ 𝐵)))
635, 62syl 17 . . . . . . . . . . 11 ((𝐵 ⊆ (𝐴 (span‘{𝐶})) ∧ 𝑥𝐵) → ((𝐴𝐵𝑥𝐵) → (¬ 𝑥𝐴 → (span‘{𝐶}) ⊆ 𝐵)))
6463imp 393 . . . . . . . . . 10 (((𝐵 ⊆ (𝐴 (span‘{𝐶})) ∧ 𝑥𝐵) ∧ (𝐴𝐵𝑥𝐵)) → (¬ 𝑥𝐴 → (span‘{𝐶}) ⊆ 𝐵))
6564anandirs 658 . . . . . . . . 9 (((𝐵 ⊆ (𝐴 (span‘{𝐶})) ∧ 𝐴𝐵) ∧ 𝑥𝐵) → (¬ 𝑥𝐴 → (span‘{𝐶}) ⊆ 𝐵))
6665expimpd 441 . . . . . . . 8 ((𝐵 ⊆ (𝐴 (span‘{𝐶})) ∧ 𝐴𝐵) → ((𝑥𝐵 ∧ ¬ 𝑥𝐴) → (span‘{𝐶}) ⊆ 𝐵))
6766exlimdv 2013 . . . . . . 7 ((𝐵 ⊆ (𝐴 (span‘{𝐶})) ∧ 𝐴𝐵) → (∃𝑥(𝑥𝐵 ∧ ¬ 𝑥𝐴) → (span‘{𝐶}) ⊆ 𝐵))
684, 67syl5 34 . . . . . 6 ((𝐵 ⊆ (𝐴 (span‘{𝐶})) ∧ 𝐴𝐵) → (𝐴𝐵 → (span‘{𝐶}) ⊆ 𝐵))
6968ex 397 . . . . 5 (𝐵 ⊆ (𝐴 (span‘{𝐶})) → (𝐴𝐵 → (𝐴𝐵 → (span‘{𝐶}) ⊆ 𝐵)))
7069pm2.43d 53 . . . 4 (𝐵 ⊆ (𝐴 (span‘{𝐶})) → (𝐴𝐵 → (span‘{𝐶}) ⊆ 𝐵))
7170impcom 394 . . 3 ((𝐴𝐵𝐵 ⊆ (𝐴 (span‘{𝐶}))) → (span‘{𝐶}) ⊆ 𝐵)
726, 10, 16chlubii 28670 . . 3 ((𝐴𝐵 ∧ (span‘{𝐶}) ⊆ 𝐵) → (𝐴 (span‘{𝐶})) ⊆ 𝐵)
733, 71, 72syl2anc 573 . 2 ((𝐴𝐵𝐵 ⊆ (𝐴 (span‘{𝐶}))) → (𝐴 (span‘{𝐶})) ⊆ 𝐵)
741, 73eqssd 3769 1 ((𝐴𝐵𝐵 ⊆ (𝐴 (span‘{𝐶}))) → 𝐵 = (𝐴 (span‘{𝐶})))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 382   = wceq 1631  wex 1852  wcel 2145  wne 2943  wrex 3062  wss 3723  wpss 3724  {csn 4317  cfv 6030  (class class class)co 6795  chil 28115   + cva 28116  0c0v 28120   cmv 28121   S csh 28124   C cch 28125   + cph 28127  spancspn 28128   chj 28129
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-8 2147  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-rep 4905  ax-sep 4916  ax-nul 4924  ax-pow 4975  ax-pr 5035  ax-un 7099  ax-inf2 8705  ax-cc 9462  ax-cnex 10197  ax-resscn 10198  ax-1cn 10199  ax-icn 10200  ax-addcl 10201  ax-addrcl 10202  ax-mulcl 10203  ax-mulrcl 10204  ax-mulcom 10205  ax-addass 10206  ax-mulass 10207  ax-distr 10208  ax-i2m1 10209  ax-1ne0 10210  ax-1rid 10211  ax-rnegex 10212  ax-rrecex 10213  ax-cnre 10214  ax-pre-lttri 10215  ax-pre-lttrn 10216  ax-pre-ltadd 10217  ax-pre-mulgt0 10218  ax-pre-sup 10219  ax-addf 10220  ax-mulf 10221  ax-hilex 28195  ax-hfvadd 28196  ax-hvcom 28197  ax-hvass 28198  ax-hv0cl 28199  ax-hvaddid 28200  ax-hfvmul 28201  ax-hvmulid 28202  ax-hvmulass 28203  ax-hvdistr1 28204  ax-hvdistr2 28205  ax-hvmul0 28206  ax-hfi 28275  ax-his1 28278  ax-his2 28279  ax-his3 28280  ax-his4 28281  ax-hcompl 28398
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3or 1072  df-3an 1073  df-tru 1634  df-fal 1637  df-ex 1853  df-nf 1858  df-sb 2050  df-eu 2622  df-mo 2623  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rmo 3069  df-rab 3070  df-v 3353  df-sbc 3588  df-csb 3683  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-pss 3739  df-nul 4064  df-if 4227  df-pw 4300  df-sn 4318  df-pr 4320  df-tp 4322  df-op 4324  df-uni 4576  df-int 4613  df-iun 4657  df-iin 4658  df-br 4788  df-opab 4848  df-mpt 4865  df-tr 4888  df-id 5158  df-eprel 5163  df-po 5171  df-so 5172  df-fr 5209  df-se 5210  df-we 5211  df-xp 5256  df-rel 5257  df-cnv 5258  df-co 5259  df-dm 5260  df-rn 5261  df-res 5262  df-ima 5263  df-pred 5822  df-ord 5868  df-on 5869  df-lim 5870  df-suc 5871  df-iota 5993  df-fun 6032  df-fn 6033  df-f 6034  df-f1 6035  df-fo 6036  df-f1o 6037  df-fv 6038  df-isom 6039  df-riota 6756  df-ov 6798  df-oprab 6799  df-mpt2 6800  df-of 7047  df-om 7216  df-1st 7318  df-2nd 7319  df-supp 7450  df-wrecs 7562  df-recs 7624  df-rdg 7662  df-1o 7716  df-2o 7717  df-oadd 7720  df-omul 7721  df-er 7899  df-map 8014  df-pm 8015  df-ixp 8066  df-en 8113  df-dom 8114  df-sdom 8115  df-fin 8116  df-fsupp 8435  df-fi 8476  df-sup 8507  df-inf 8508  df-oi 8574  df-card 8968  df-acn 8971  df-cda 9195  df-pnf 10281  df-mnf 10282  df-xr 10283  df-ltxr 10284  df-le 10285  df-sub 10473  df-neg 10474  df-div 10890  df-nn 11226  df-2 11284  df-3 11285  df-4 11286  df-5 11287  df-6 11288  df-7 11289  df-8 11290  df-9 11291  df-n0 11499  df-z 11584  df-dec 11700  df-uz 11893  df-q 11996  df-rp 12035  df-xneg 12150  df-xadd 12151  df-xmul 12152  df-ioo 12383  df-ico 12385  df-icc 12386  df-fz 12533  df-fzo 12673  df-fl 12800  df-seq 13008  df-exp 13067  df-hash 13321  df-cj 14046  df-re 14047  df-im 14048  df-sqrt 14182  df-abs 14183  df-clim 14426  df-rlim 14427  df-sum 14624  df-struct 16065  df-ndx 16066  df-slot 16067  df-base 16069  df-sets 16070  df-ress 16071  df-plusg 16161  df-mulr 16162  df-starv 16163  df-sca 16164  df-vsca 16165  df-ip 16166  df-tset 16167  df-ple 16168  df-ds 16171  df-unif 16172  df-hom 16173  df-cco 16174  df-rest 16290  df-topn 16291  df-0g 16309  df-gsum 16310  df-topgen 16311  df-pt 16312  df-prds 16315  df-xrs 16369  df-qtop 16374  df-imas 16375  df-xps 16377  df-mre 16453  df-mrc 16454  df-acs 16456  df-mgm 17449  df-sgrp 17491  df-mnd 17502  df-submnd 17543  df-mulg 17748  df-cntz 17956  df-cmn 18401  df-psmet 19952  df-xmet 19953  df-met 19954  df-bl 19955  df-mopn 19956  df-fbas 19957  df-fg 19958  df-cnfld 19961  df-top 20918  df-topon 20935  df-topsp 20957  df-bases 20970  df-cld 21043  df-ntr 21044  df-cls 21045  df-nei 21122  df-cn 21251  df-cnp 21252  df-lm 21253  df-haus 21339  df-tx 21585  df-hmeo 21778  df-fil 21869  df-fm 21961  df-flim 21962  df-flf 21963  df-xms 22344  df-ms 22345  df-tms 22346  df-cfil 23271  df-cau 23272  df-cmet 23273  df-grpo 27686  df-gid 27687  df-ginv 27688  df-gdiv 27689  df-ablo 27738  df-vc 27753  df-nv 27786  df-va 27789  df-ba 27790  df-sm 27791  df-0v 27792  df-vs 27793  df-nmcv 27794  df-ims 27795  df-dip 27895  df-ssp 27916  df-ph 28007  df-cbn 28058  df-hnorm 28164  df-hba 28165  df-hvsub 28167  df-hlim 28168  df-hcau 28169  df-sh 28403  df-ch 28417  df-oc 28448  df-ch0 28449  df-shs 28506  df-span 28507  df-chj 28508  df-pjh 28593
This theorem is referenced by:  spansncv  28851
  Copyright terms: Public domain W3C validator