Theorem islsat 39451

Description: The predicate "is a 1-dim subspace (atom)" (of a left module or left vector space). (Contributed by NM, 9-Apr-2014.) (Revised by Mario Carneiro, 24-Jun-2014.)

Hypotheses

Ref	Expression
lsatset.v	⊢ 𝑉 = (Base‘𝑊)
lsatset.n	⊢ 𝑁 = (LSpan‘𝑊)
lsatset.z	⊢ 0 = (0g‘𝑊)
lsatset.a	⊢ 𝐴 = (LSAtoms‘𝑊)

Assertion

Ref	Expression
islsat	⊢ (𝑊 ∈ 𝑋 → (𝑈 ∈ 𝐴 ↔ ∃𝑥 ∈ (𝑉 ∖ { 0 })𝑈 = (𝑁‘{𝑥})))

Distinct variable groups:   𝑥,𝑊   𝑥,𝑋   𝑥,𝑁   𝑥,𝑈   𝑥,𝑉   𝑥, 0

Allowed substitution hint:   𝐴(𝑥)

Proof of Theorem islsat

Step	Hyp	Ref	Expression
1		lsatset.v	. . . 4 ⊢ 𝑉 = (Base‘𝑊)
2		lsatset.n	. . . 4 ⊢ 𝑁 = (LSpan‘𝑊)
3		lsatset.z	. . . 4 ⊢ 0 = (0g‘𝑊)
4		lsatset.a	. . . 4 ⊢ 𝐴 = (LSAtoms‘𝑊)
5	1, 2, 3, 4	lsatset 39450	. . 3 ⊢ (𝑊 ∈ 𝑋 → 𝐴 = ran (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑁‘{𝑥})))
6	5	eleq2d 2823	. 2 ⊢ (𝑊 ∈ 𝑋 → (𝑈 ∈ 𝐴 ↔ 𝑈 ∈ ran (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑁‘{𝑥}))))
7		eqid 2737	. . 3 ⊢ (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑁‘{𝑥})) = (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑁‘{𝑥}))
8		fvex 6847	. . 3 ⊢ (𝑁‘{𝑥}) ∈ V
9	7, 8	elrnmpti 5911	. 2 ⊢ (𝑈 ∈ ran (𝑥 ∈ (𝑉 ∖ { 0 }) ↦ (𝑁‘{𝑥})) ↔ ∃𝑥 ∈ (𝑉 ∖ { 0 })𝑈 = (𝑁‘{𝑥}))
10	6, 9	bitrdi 287	1 ⊢ (𝑊 ∈ 𝑋 → (𝑈 ∈ 𝐴 ↔ ∃𝑥 ∈ (𝑉 ∖ { 0 })𝑈 = (𝑁‘{𝑥})))

Syntax hints:   → wi 4   ↔ wb 206   = wceq 1542   ∈ wcel 2114  ∃wrex 3062   ∖ cdif 3887  {csn 4568   ↦ cmpt 5167  ran crn 5625  ‘cfv 6492  Basecbs 17170  0_gc0g 17393  LSpanclspn 20957  LSAtomsclsa 39434

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5231  ax-nul 5241  ax-pr 5370  ax-un 7682

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rab 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-br 5087  df-opab 5149  df-mpt 5168  df-id 5519  df-xp 5630  df-rel 5631  df-cnv 5632  df-co 5633  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-iota 6448  df-fun 6494  df-fn 6495  df-f 6496  df-fv 6500  df-lsatoms 39436

This theorem is referenced by:  lsatlspsn2  39452  lsatlspsn  39453  islsati  39454  lsateln0  39455  lsatn0  39459  lsatcmp  39463  lsmsat  39468  lsatfixedN  39469  islshpat  39477  lsatcv0  39491  lsat0cv  39493  lcv1  39501  l1cvpat  39514  dih1dimatlem  41789  dihlatat  41797  dochsatshp  41911