MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lbsextlem3 Structured version   Visualization version   GIF version

Theorem lbsextlem3 19855
Description: Lemma for lbsext 19858. A chain in 𝑆 has an upper bound in 𝑆. (Contributed by Mario Carneiro, 25-Jun-2014.)
Hypotheses
Ref Expression
lbsext.v 𝑉 = (Base‘𝑊)
lbsext.j 𝐽 = (LBasis‘𝑊)
lbsext.n 𝑁 = (LSpan‘𝑊)
lbsext.w (𝜑𝑊 ∈ LVec)
lbsext.c (𝜑𝐶𝑉)
lbsext.x (𝜑 → ∀𝑥𝐶 ¬ 𝑥 ∈ (𝑁‘(𝐶 ∖ {𝑥})))
lbsext.s 𝑆 = {𝑧 ∈ 𝒫 𝑉 ∣ (𝐶𝑧 ∧ ∀𝑥𝑧 ¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥})))}
lbsext.p 𝑃 = (LSubSp‘𝑊)
lbsext.a (𝜑𝐴𝑆)
lbsext.z (𝜑𝐴 ≠ ∅)
lbsext.r (𝜑 → [] Or 𝐴)
lbsext.t 𝑇 = 𝑢𝐴 (𝑁‘(𝑢 ∖ {𝑥}))
Assertion
Ref Expression
lbsextlem3 (𝜑 𝐴𝑆)
Distinct variable groups:   𝑥,𝐽   𝑥,𝑢,𝜑   𝑢,𝑆,𝑥   𝑥,𝑧,𝐶   𝑧,𝑢,𝑁,𝑥   𝑢,𝑉,𝑥,𝑧   𝑢,𝑊,𝑥   𝑢,𝐴,𝑥,𝑧
Allowed substitution hints:   𝜑(𝑧)   𝐶(𝑢)   𝑃(𝑥,𝑧,𝑢)   𝑆(𝑧)   𝑇(𝑥,𝑧,𝑢)   𝐽(𝑧,𝑢)   𝑊(𝑧)

Proof of Theorem lbsextlem3
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 lbsext.a . . . . 5 (𝜑𝐴𝑆)
2 lbsext.s . . . . . 6 𝑆 = {𝑧 ∈ 𝒫 𝑉 ∣ (𝐶𝑧 ∧ ∀𝑥𝑧 ¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥})))}
32ssrab3 4060 . . . . 5 𝑆 ⊆ 𝒫 𝑉
41, 3syl6ss 3982 . . . 4 (𝜑𝐴 ⊆ 𝒫 𝑉)
5 sspwuni 5018 . . . 4 (𝐴 ⊆ 𝒫 𝑉 𝐴𝑉)
64, 5sylib 219 . . 3 (𝜑 𝐴𝑉)
7 lbsext.v . . . . 5 𝑉 = (Base‘𝑊)
87fvexi 6680 . . . 4 𝑉 ∈ V
98elpw2 5244 . . 3 ( 𝐴 ∈ 𝒫 𝑉 𝐴𝑉)
106, 9sylibr 235 . 2 (𝜑 𝐴 ∈ 𝒫 𝑉)
11 ssintub 4891 . . . . 5 𝐶 {𝑧 ∈ 𝒫 𝑉𝐶𝑧}
12 simpl 483 . . . . . . . . . 10 ((𝐶𝑧 ∧ ∀𝑥𝑧 ¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥}))) → 𝐶𝑧)
1312a1i 11 . . . . . . . . 9 (𝑧 ∈ 𝒫 𝑉 → ((𝐶𝑧 ∧ ∀𝑥𝑧 ¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥}))) → 𝐶𝑧))
1413ss2rabi 4056 . . . . . . . 8 {𝑧 ∈ 𝒫 𝑉 ∣ (𝐶𝑧 ∧ ∀𝑥𝑧 ¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥})))} ⊆ {𝑧 ∈ 𝒫 𝑉𝐶𝑧}
152, 14eqsstri 4004 . . . . . . 7 𝑆 ⊆ {𝑧 ∈ 𝒫 𝑉𝐶𝑧}
161, 15syl6ss 3982 . . . . . 6 (𝜑𝐴 ⊆ {𝑧 ∈ 𝒫 𝑉𝐶𝑧})
17 intss 4894 . . . . . 6 (𝐴 ⊆ {𝑧 ∈ 𝒫 𝑉𝐶𝑧} → {𝑧 ∈ 𝒫 𝑉𝐶𝑧} ⊆ 𝐴)
1816, 17syl 17 . . . . 5 (𝜑 {𝑧 ∈ 𝒫 𝑉𝐶𝑧} ⊆ 𝐴)
1911, 18sstrid 3981 . . . 4 (𝜑𝐶 𝐴)
20 lbsext.z . . . . 5 (𝜑𝐴 ≠ ∅)
21 intssuni 4895 . . . . 5 (𝐴 ≠ ∅ → 𝐴 𝐴)
2220, 21syl 17 . . . 4 (𝜑 𝐴 𝐴)
2319, 22sstrd 3980 . . 3 (𝜑𝐶 𝐴)
24 eluni2 4840 . . . . 5 (𝑥 𝐴 ↔ ∃𝑦𝐴 𝑥𝑦)
25 simpll1 1206 . . . . . . . . . . . 12 ((((𝜑𝑦𝐴𝑥𝑦) ∧ 𝑢𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → 𝜑)
26 lbsext.w . . . . . . . . . . . . 13 (𝜑𝑊 ∈ LVec)
27 lveclmod 19801 . . . . . . . . . . . . 13 (𝑊 ∈ LVec → 𝑊 ∈ LMod)
2826, 27syl 17 . . . . . . . . . . . 12 (𝜑𝑊 ∈ LMod)
2925, 28syl 17 . . . . . . . . . . 11 ((((𝜑𝑦𝐴𝑥𝑦) ∧ 𝑢𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → 𝑊 ∈ LMod)
3025, 1syl 17 . . . . . . . . . . . . . . 15 ((((𝜑𝑦𝐴𝑥𝑦) ∧ 𝑢𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → 𝐴𝑆)
31 lbsext.r . . . . . . . . . . . . . . . . 17 (𝜑 → [] Or 𝐴)
3225, 31syl 17 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦𝐴𝑥𝑦) ∧ 𝑢𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → [] Or 𝐴)
33 simpll2 1207 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦𝐴𝑥𝑦) ∧ 𝑢𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → 𝑦𝐴)
34 simplr 765 . . . . . . . . . . . . . . . 16 ((((𝜑𝑦𝐴𝑥𝑦) ∧ 𝑢𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → 𝑢𝐴)
35 sorpssun 7449 . . . . . . . . . . . . . . . 16 (( [] Or 𝐴 ∧ (𝑦𝐴𝑢𝐴)) → (𝑦𝑢) ∈ 𝐴)
3632, 33, 34, 35syl12anc 834 . . . . . . . . . . . . . . 15 ((((𝜑𝑦𝐴𝑥𝑦) ∧ 𝑢𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → (𝑦𝑢) ∈ 𝐴)
3730, 36sseldd 3971 . . . . . . . . . . . . . 14 ((((𝜑𝑦𝐴𝑥𝑦) ∧ 𝑢𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → (𝑦𝑢) ∈ 𝑆)
383, 37sseldi 3968 . . . . . . . . . . . . 13 ((((𝜑𝑦𝐴𝑥𝑦) ∧ 𝑢𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → (𝑦𝑢) ∈ 𝒫 𝑉)
3938elpwid 4555 . . . . . . . . . . . 12 ((((𝜑𝑦𝐴𝑥𝑦) ∧ 𝑢𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → (𝑦𝑢) ⊆ 𝑉)
4039ssdifssd 4122 . . . . . . . . . . 11 ((((𝜑𝑦𝐴𝑥𝑦) ∧ 𝑢𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → ((𝑦𝑢) ∖ {𝑥}) ⊆ 𝑉)
41 ssun2 4152 . . . . . . . . . . . 12 𝑢 ⊆ (𝑦𝑢)
42 ssdif 4119 . . . . . . . . . . . 12 (𝑢 ⊆ (𝑦𝑢) → (𝑢 ∖ {𝑥}) ⊆ ((𝑦𝑢) ∖ {𝑥}))
4341, 42mp1i 13 . . . . . . . . . . 11 ((((𝜑𝑦𝐴𝑥𝑦) ∧ 𝑢𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → (𝑢 ∖ {𝑥}) ⊆ ((𝑦𝑢) ∖ {𝑥}))
44 lbsext.n . . . . . . . . . . . 12 𝑁 = (LSpan‘𝑊)
457, 44lspss 19679 . . . . . . . . . . 11 ((𝑊 ∈ LMod ∧ ((𝑦𝑢) ∖ {𝑥}) ⊆ 𝑉 ∧ (𝑢 ∖ {𝑥}) ⊆ ((𝑦𝑢) ∖ {𝑥})) → (𝑁‘(𝑢 ∖ {𝑥})) ⊆ (𝑁‘((𝑦𝑢) ∖ {𝑥})))
4629, 40, 43, 45syl3anc 1365 . . . . . . . . . 10 ((((𝜑𝑦𝐴𝑥𝑦) ∧ 𝑢𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → (𝑁‘(𝑢 ∖ {𝑥})) ⊆ (𝑁‘((𝑦𝑢) ∖ {𝑥})))
47 simpr 485 . . . . . . . . . 10 ((((𝜑𝑦𝐴𝑥𝑦) ∧ 𝑢𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥})))
4846, 47sseldd 3971 . . . . . . . . 9 ((((𝜑𝑦𝐴𝑥𝑦) ∧ 𝑢𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → 𝑥 ∈ (𝑁‘((𝑦𝑢) ∖ {𝑥})))
49 sseq2 3996 . . . . . . . . . . . . . . 15 (𝑧 = (𝑦𝑢) → (𝐶𝑧𝐶 ⊆ (𝑦𝑢)))
50 difeq1 4095 . . . . . . . . . . . . . . . . . . 19 (𝑧 = (𝑦𝑢) → (𝑧 ∖ {𝑥}) = ((𝑦𝑢) ∖ {𝑥}))
5150fveq2d 6670 . . . . . . . . . . . . . . . . . 18 (𝑧 = (𝑦𝑢) → (𝑁‘(𝑧 ∖ {𝑥})) = (𝑁‘((𝑦𝑢) ∖ {𝑥})))
5251eleq2d 2902 . . . . . . . . . . . . . . . . 17 (𝑧 = (𝑦𝑢) → (𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥})) ↔ 𝑥 ∈ (𝑁‘((𝑦𝑢) ∖ {𝑥}))))
5352notbid 319 . . . . . . . . . . . . . . . 16 (𝑧 = (𝑦𝑢) → (¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥})) ↔ ¬ 𝑥 ∈ (𝑁‘((𝑦𝑢) ∖ {𝑥}))))
5453raleqbi1dv 3408 . . . . . . . . . . . . . . 15 (𝑧 = (𝑦𝑢) → (∀𝑥𝑧 ¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥})) ↔ ∀𝑥 ∈ (𝑦𝑢) ¬ 𝑥 ∈ (𝑁‘((𝑦𝑢) ∖ {𝑥}))))
5549, 54anbi12d 630 . . . . . . . . . . . . . 14 (𝑧 = (𝑦𝑢) → ((𝐶𝑧 ∧ ∀𝑥𝑧 ¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥}))) ↔ (𝐶 ⊆ (𝑦𝑢) ∧ ∀𝑥 ∈ (𝑦𝑢) ¬ 𝑥 ∈ (𝑁‘((𝑦𝑢) ∖ {𝑥})))))
5655, 2elrab2 3686 . . . . . . . . . . . . 13 ((𝑦𝑢) ∈ 𝑆 ↔ ((𝑦𝑢) ∈ 𝒫 𝑉 ∧ (𝐶 ⊆ (𝑦𝑢) ∧ ∀𝑥 ∈ (𝑦𝑢) ¬ 𝑥 ∈ (𝑁‘((𝑦𝑢) ∖ {𝑥})))))
5756simprbi 497 . . . . . . . . . . . 12 ((𝑦𝑢) ∈ 𝑆 → (𝐶 ⊆ (𝑦𝑢) ∧ ∀𝑥 ∈ (𝑦𝑢) ¬ 𝑥 ∈ (𝑁‘((𝑦𝑢) ∖ {𝑥}))))
5857simprd 496 . . . . . . . . . . 11 ((𝑦𝑢) ∈ 𝑆 → ∀𝑥 ∈ (𝑦𝑢) ¬ 𝑥 ∈ (𝑁‘((𝑦𝑢) ∖ {𝑥})))
5937, 58syl 17 . . . . . . . . . 10 ((((𝜑𝑦𝐴𝑥𝑦) ∧ 𝑢𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → ∀𝑥 ∈ (𝑦𝑢) ¬ 𝑥 ∈ (𝑁‘((𝑦𝑢) ∖ {𝑥})))
60 simpll3 1208 . . . . . . . . . . 11 ((((𝜑𝑦𝐴𝑥𝑦) ∧ 𝑢𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → 𝑥𝑦)
61 elun1 4155 . . . . . . . . . . 11 (𝑥𝑦𝑥 ∈ (𝑦𝑢))
6260, 61syl 17 . . . . . . . . . 10 ((((𝜑𝑦𝐴𝑥𝑦) ∧ 𝑢𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → 𝑥 ∈ (𝑦𝑢))
63 rsp 3209 . . . . . . . . . 10 (∀𝑥 ∈ (𝑦𝑢) ¬ 𝑥 ∈ (𝑁‘((𝑦𝑢) ∖ {𝑥})) → (𝑥 ∈ (𝑦𝑢) → ¬ 𝑥 ∈ (𝑁‘((𝑦𝑢) ∖ {𝑥}))))
6459, 62, 63sylc 65 . . . . . . . . 9 ((((𝜑𝑦𝐴𝑥𝑦) ∧ 𝑢𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → ¬ 𝑥 ∈ (𝑁‘((𝑦𝑢) ∖ {𝑥})))
6548, 64pm2.65da 813 . . . . . . . 8 (((𝜑𝑦𝐴𝑥𝑦) ∧ 𝑢𝐴) → ¬ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥})))
6665nrexdv 3274 . . . . . . 7 ((𝜑𝑦𝐴𝑥𝑦) → ¬ ∃𝑢𝐴 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥})))
67 lbsext.j . . . . . . . . . . . . . . . 16 𝐽 = (LBasis‘𝑊)
68 lbsext.c . . . . . . . . . . . . . . . 16 (𝜑𝐶𝑉)
69 lbsext.x . . . . . . . . . . . . . . . 16 (𝜑 → ∀𝑥𝐶 ¬ 𝑥 ∈ (𝑁‘(𝐶 ∖ {𝑥})))
70 lbsext.p . . . . . . . . . . . . . . . 16 𝑃 = (LSubSp‘𝑊)
71 lbsext.t . . . . . . . . . . . . . . . 16 𝑇 = 𝑢𝐴 (𝑁‘(𝑢 ∖ {𝑥}))
727, 67, 44, 26, 68, 69, 2, 70, 1, 20, 31, 71lbsextlem2 19854 . . . . . . . . . . . . . . 15 (𝜑 → (𝑇𝑃 ∧ ( 𝐴 ∖ {𝑥}) ⊆ 𝑇))
7372simpld 495 . . . . . . . . . . . . . 14 (𝜑𝑇𝑃)
747, 70lssss 19631 . . . . . . . . . . . . . 14 (𝑇𝑃𝑇𝑉)
7573, 74syl 17 . . . . . . . . . . . . 13 (𝜑𝑇𝑉)
7672simprd 496 . . . . . . . . . . . . 13 (𝜑 → ( 𝐴 ∖ {𝑥}) ⊆ 𝑇)
777, 44lspss 19679 . . . . . . . . . . . . 13 ((𝑊 ∈ LMod ∧ 𝑇𝑉 ∧ ( 𝐴 ∖ {𝑥}) ⊆ 𝑇) → (𝑁‘( 𝐴 ∖ {𝑥})) ⊆ (𝑁𝑇))
7828, 75, 76, 77syl3anc 1365 . . . . . . . . . . . 12 (𝜑 → (𝑁‘( 𝐴 ∖ {𝑥})) ⊆ (𝑁𝑇))
7970, 44lspid 19677 . . . . . . . . . . . . 13 ((𝑊 ∈ LMod ∧ 𝑇𝑃) → (𝑁𝑇) = 𝑇)
8028, 73, 79syl2anc 584 . . . . . . . . . . . 12 (𝜑 → (𝑁𝑇) = 𝑇)
8178, 80sseqtrd 4010 . . . . . . . . . . 11 (𝜑 → (𝑁‘( 𝐴 ∖ {𝑥})) ⊆ 𝑇)
82813ad2ant1 1127 . . . . . . . . . 10 ((𝜑𝑦𝐴𝑥𝑦) → (𝑁‘( 𝐴 ∖ {𝑥})) ⊆ 𝑇)
8382, 71syl6sseq 4020 . . . . . . . . 9 ((𝜑𝑦𝐴𝑥𝑦) → (𝑁‘( 𝐴 ∖ {𝑥})) ⊆ 𝑢𝐴 (𝑁‘(𝑢 ∖ {𝑥})))
8483sseld 3969 . . . . . . . 8 ((𝜑𝑦𝐴𝑥𝑦) → (𝑥 ∈ (𝑁‘( 𝐴 ∖ {𝑥})) → 𝑥 𝑢𝐴 (𝑁‘(𝑢 ∖ {𝑥}))))
85 eliun 4920 . . . . . . . 8 (𝑥 𝑢𝐴 (𝑁‘(𝑢 ∖ {𝑥})) ↔ ∃𝑢𝐴 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥})))
8684, 85syl6ib 252 . . . . . . 7 ((𝜑𝑦𝐴𝑥𝑦) → (𝑥 ∈ (𝑁‘( 𝐴 ∖ {𝑥})) → ∃𝑢𝐴 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))))
8766, 86mtod 199 . . . . . 6 ((𝜑𝑦𝐴𝑥𝑦) → ¬ 𝑥 ∈ (𝑁‘( 𝐴 ∖ {𝑥})))
8887rexlimdv3a 3290 . . . . 5 (𝜑 → (∃𝑦𝐴 𝑥𝑦 → ¬ 𝑥 ∈ (𝑁‘( 𝐴 ∖ {𝑥}))))
8924, 88syl5bi 243 . . . 4 (𝜑 → (𝑥 𝐴 → ¬ 𝑥 ∈ (𝑁‘( 𝐴 ∖ {𝑥}))))
9089ralrimiv 3185 . . 3 (𝜑 → ∀𝑥 𝐴 ¬ 𝑥 ∈ (𝑁‘( 𝐴 ∖ {𝑥})))
9123, 90jca 512 . 2 (𝜑 → (𝐶 𝐴 ∧ ∀𝑥 𝐴 ¬ 𝑥 ∈ (𝑁‘( 𝐴 ∖ {𝑥}))))
92 sseq2 3996 . . . 4 (𝑧 = 𝐴 → (𝐶𝑧𝐶 𝐴))
93 difeq1 4095 . . . . . . . 8 (𝑧 = 𝐴 → (𝑧 ∖ {𝑥}) = ( 𝐴 ∖ {𝑥}))
9493fveq2d 6670 . . . . . . 7 (𝑧 = 𝐴 → (𝑁‘(𝑧 ∖ {𝑥})) = (𝑁‘( 𝐴 ∖ {𝑥})))
9594eleq2d 2902 . . . . . 6 (𝑧 = 𝐴 → (𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥})) ↔ 𝑥 ∈ (𝑁‘( 𝐴 ∖ {𝑥}))))
9695notbid 319 . . . . 5 (𝑧 = 𝐴 → (¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥})) ↔ ¬ 𝑥 ∈ (𝑁‘( 𝐴 ∖ {𝑥}))))
9796raleqbi1dv 3408 . . . 4 (𝑧 = 𝐴 → (∀𝑥𝑧 ¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥})) ↔ ∀𝑥 𝐴 ¬ 𝑥 ∈ (𝑁‘( 𝐴 ∖ {𝑥}))))
9892, 97anbi12d 630 . . 3 (𝑧 = 𝐴 → ((𝐶𝑧 ∧ ∀𝑥𝑧 ¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥}))) ↔ (𝐶 𝐴 ∧ ∀𝑥 𝐴 ¬ 𝑥 ∈ (𝑁‘( 𝐴 ∖ {𝑥})))))
9998, 2elrab2 3686 . 2 ( 𝐴𝑆 ↔ ( 𝐴 ∈ 𝒫 𝑉 ∧ (𝐶 𝐴 ∧ ∀𝑥 𝐴 ¬ 𝑥 ∈ (𝑁‘( 𝐴 ∖ {𝑥})))))
10010, 91, 99sylanbrc 583 1 (𝜑 𝐴𝑆)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  w3a 1081   = wceq 1530  wcel 2107  wne 3020  wral 3142  wrex 3143  {crab 3146  cdif 3936  cun 3937  wss 3939  c0 4294  𝒫 cpw 4541  {csn 4563   cuni 4836   cint 4873   ciun 4916   Or wor 5471  cfv 6351   [] crpss 7441  Basecbs 16476  LModclmod 19557  LSubSpclss 19626  LSpanclspn 19666  LBasisclbs 19769  LVecclvec 19797
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797  ax-rep 5186  ax-sep 5199  ax-nul 5206  ax-pow 5262  ax-pr 5325  ax-un 7454  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2619  df-eu 2651  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-ne 3021  df-nel 3128  df-ral 3147  df-rex 3148  df-reu 3149  df-rmo 3150  df-rab 3151  df-v 3501  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-pss 3957  df-nul 4295  df-if 4470  df-pw 4543  df-sn 4564  df-pr 4566  df-tp 4568  df-op 4570  df-uni 4837  df-int 4874  df-iun 4918  df-br 5063  df-opab 5125  df-mpt 5143  df-tr 5169  df-id 5458  df-eprel 5463  df-po 5472  df-so 5473  df-fr 5512  df-we 5514  df-xp 5559  df-rel 5560  df-cnv 5561  df-co 5562  df-dm 5563  df-rn 5564  df-res 5565  df-ima 5566  df-pred 6145  df-ord 6191  df-on 6192  df-lim 6193  df-suc 6194  df-iota 6311  df-fun 6353  df-fn 6354  df-f 6355  df-f1 6356  df-fo 6357  df-f1o 6358  df-fv 6359  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-rpss 7442  df-om 7572  df-1st 7683  df-2nd 7684  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-er 8282  df-en 8502  df-dom 8503  df-sdom 8504  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-nn 11631  df-2 11692  df-ndx 16479  df-slot 16480  df-base 16482  df-sets 16483  df-plusg 16571  df-0g 16708  df-mgm 17845  df-sgrp 17893  df-mnd 17904  df-grp 18039  df-minusg 18040  df-sbg 18041  df-mgp 19163  df-ur 19175  df-ring 19222  df-lmod 19559  df-lss 19627  df-lsp 19667  df-lvec 19798
This theorem is referenced by:  lbsextlem4  19856
  Copyright terms: Public domain W3C validator