Users' Mathboxes Mathbox for Norm Megill < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  isline2 Structured version   Visualization version   GIF version

Theorem isline2 36970
Description: Definition of line in terms of projective map. (Contributed by NM, 25-Jan-2012.)
Hypotheses
Ref Expression
isline2.j = (join‘𝐾)
isline2.a 𝐴 = (Atoms‘𝐾)
isline2.n 𝑁 = (Lines‘𝐾)
isline2.m 𝑀 = (pmap‘𝐾)
Assertion
Ref Expression
isline2 (𝐾 ∈ Lat → (𝑋𝑁 ↔ ∃𝑝𝐴𝑞𝐴 (𝑝𝑞𝑋 = (𝑀‘(𝑝 𝑞)))))
Distinct variable groups:   𝑞,𝑝,𝐴   𝐾,𝑝,𝑞   𝑋,𝑝,𝑞
Allowed substitution hints:   (𝑞,𝑝)   𝑀(𝑞,𝑝)   𝑁(𝑞,𝑝)

Proof of Theorem isline2
Dummy variable 𝑟 is distinct from all other variables.
StepHypRef Expression
1 eqid 2824 . . 3 (le‘𝐾) = (le‘𝐾)
2 isline2.j . . 3 = (join‘𝐾)
3 isline2.a . . 3 𝐴 = (Atoms‘𝐾)
4 isline2.n . . 3 𝑁 = (Lines‘𝐾)
51, 2, 3, 4isline 36935 . 2 (𝐾 ∈ Lat → (𝑋𝑁 ↔ ∃𝑝𝐴𝑞𝐴 (𝑝𝑞𝑋 = {𝑟𝐴𝑟(le‘𝐾)(𝑝 𝑞)})))
6 simpl 486 . . . . . . 7 ((𝐾 ∈ Lat ∧ (𝑝𝐴𝑞𝐴)) → 𝐾 ∈ Lat)
7 eqid 2824 . . . . . . . . 9 (Base‘𝐾) = (Base‘𝐾)
87, 3atbase 36485 . . . . . . . 8 (𝑝𝐴𝑝 ∈ (Base‘𝐾))
98ad2antrl 727 . . . . . . 7 ((𝐾 ∈ Lat ∧ (𝑝𝐴𝑞𝐴)) → 𝑝 ∈ (Base‘𝐾))
107, 3atbase 36485 . . . . . . . 8 (𝑞𝐴𝑞 ∈ (Base‘𝐾))
1110ad2antll 728 . . . . . . 7 ((𝐾 ∈ Lat ∧ (𝑝𝐴𝑞𝐴)) → 𝑞 ∈ (Base‘𝐾))
127, 2latjcl 17650 . . . . . . 7 ((𝐾 ∈ Lat ∧ 𝑝 ∈ (Base‘𝐾) ∧ 𝑞 ∈ (Base‘𝐾)) → (𝑝 𝑞) ∈ (Base‘𝐾))
136, 9, 11, 12syl3anc 1368 . . . . . 6 ((𝐾 ∈ Lat ∧ (𝑝𝐴𝑞𝐴)) → (𝑝 𝑞) ∈ (Base‘𝐾))
14 isline2.m . . . . . . 7 𝑀 = (pmap‘𝐾)
157, 1, 3, 14pmapval 36953 . . . . . 6 ((𝐾 ∈ Lat ∧ (𝑝 𝑞) ∈ (Base‘𝐾)) → (𝑀‘(𝑝 𝑞)) = {𝑟𝐴𝑟(le‘𝐾)(𝑝 𝑞)})
1613, 15syldan 594 . . . . 5 ((𝐾 ∈ Lat ∧ (𝑝𝐴𝑞𝐴)) → (𝑀‘(𝑝 𝑞)) = {𝑟𝐴𝑟(le‘𝐾)(𝑝 𝑞)})
1716eqeq2d 2835 . . . 4 ((𝐾 ∈ Lat ∧ (𝑝𝐴𝑞𝐴)) → (𝑋 = (𝑀‘(𝑝 𝑞)) ↔ 𝑋 = {𝑟𝐴𝑟(le‘𝐾)(𝑝 𝑞)}))
1817anbi2d 631 . . 3 ((𝐾 ∈ Lat ∧ (𝑝𝐴𝑞𝐴)) → ((𝑝𝑞𝑋 = (𝑀‘(𝑝 𝑞))) ↔ (𝑝𝑞𝑋 = {𝑟𝐴𝑟(le‘𝐾)(𝑝 𝑞)})))
19182rexbidva 3291 . 2 (𝐾 ∈ Lat → (∃𝑝𝐴𝑞𝐴 (𝑝𝑞𝑋 = (𝑀‘(𝑝 𝑞))) ↔ ∃𝑝𝐴𝑞𝐴 (𝑝𝑞𝑋 = {𝑟𝐴𝑟(le‘𝐾)(𝑝 𝑞)})))
205, 19bitr4d 285 1 (𝐾 ∈ Lat → (𝑋𝑁 ↔ ∃𝑝𝐴𝑞𝐴 (𝑝𝑞𝑋 = (𝑀‘(𝑝 𝑞)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399   = wceq 1538  wcel 2115  wne 3013  wrex 3133  {crab 3136   class class class wbr 5047  cfv 6336  (class class class)co 7138  Basecbs 16472  lecple 16561  joincjn 17543  Latclat 17644  Atomscatm 36459  Linesclines 36690  pmapcpmap 36693
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 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-rep 5171  ax-sep 5184  ax-nul 5191  ax-pow 5247  ax-pr 5311  ax-un 7444
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3014  df-ral 3137  df-rex 3138  df-reu 3139  df-rab 3141  df-v 3481  df-sbc 3758  df-csb 3866  df-dif 3921  df-un 3923  df-in 3925  df-ss 3935  df-nul 4275  df-if 4449  df-pw 4522  df-sn 4549  df-pr 4551  df-op 4555  df-uni 4820  df-iun 4902  df-br 5048  df-opab 5110  df-mpt 5128  df-id 5441  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-f1 6341  df-fo 6342  df-f1o 6343  df-fv 6344  df-riota 7096  df-ov 7141  df-oprab 7142  df-lub 17573  df-glb 17574  df-join 17575  df-meet 17576  df-lat 17645  df-ats 36463  df-lines 36697  df-pmap 36700
This theorem is referenced by:  isline3  36972  lncvrelatN  36977  linepsubclN  37147
  Copyright terms: Public domain W3C validator