Table of ContentsTable of Contents Mathbox for Frédéric Liné < Previous   Next >
Related theorems
Unicode version
Theorem isplibg 15319
Description: The predicate "is a planar incidence-betweenness geometry "
Hypotheses
Ref Expression
isplibg.1 |- P = U.L
isplibg.2 |- (ph <-> ((L e. Plig /\ Rel B /\ Rel dom B) /\ (dom dom B = P /\ ran dom B = P /\ ran B = P)))
isplibg.3 |- (ps <-> A.p e. P A.q e. P A.r e. P (<.<.p, q>., r>. e. B -> (<.<.r, q>., p>. e. B /\ E.l e. L (p e. l /\ q e. l /\ r e. l) /\ (p =/= q /\ p =/= r /\ q =/= r))))
isplibg.4 |- (ch <-> A.b e. P A.d e. P (b =/= d -> E.a e. P E.c e. P E.e e. P (<.<.a, b>., d>. e. B /\ <.<.b, c>., d>. e. B /\ <.<.b, d>., e>. e. B)))
isplibg.5 |- (th <-> A.l e. L A.p e. P A.q e. P A.r e. P (((p e. l /\ q e. l /\ r e. l) /\ (p =/= q /\ q =/= r /\ p =/= r)) -> ((<.<.q, p>., r>. e. B /\ -. <.<.p, q>., r>. e. B /\ -. <.<.p, r>., q>. e. B) \/ (-. <.<.q, p>., r>. e. B /\ <.<.p, q>., r>. e. B /\ -. <.<.p, r>., q>. e. B) \/ (-. <.<.q, p>., r>. e. B /\ -. <.<.p, q>., r>. e. B /\ <.<.p, r>., q>. e. B))))
isplibg.6 |- (ta <-> A.l e. L A.p e. P A.q e. P A.r e. P (((-. p e. l /\ -. q e. l /\ -. r e. l) /\ ({a e. P | (<.<.p, a>., q>. e. B \/ a = p \/ a = q)} i^i l) = (/) /\ ({a e. P | (<.<.q, a>., r>. e. B \/ a = q \/ a = r)} i^i l) = (/)) -> ({a e. P | (<.<.p, a>., r>. e. B \/ a = p \/ a = r)} i^i l) = (/)))
isplibg.7 |- (et <-> A.l e. L A.p e. P A.q e. P A.r e. P (((-. p e. l /\ -. q e. l /\ -. r e. l) /\ (({a e. P | (<.<.p, a>., q>. e. B \/ a = p \/ a = q)} i^i l) =/= (/) /\ ({a e. P | (<.<.q, a>., r>. e. B \/ a = q \/ a = r)} i^i l) =/= (/))) -> ({a e. P | (<.<.p, a>., r>. e. B \/ a = p \/ a = r)} i^i l) = (/)))
Assertion
Ref Expression
isplibg |- ((L e. A /\ B e. C) -> (<.L, B>. e. Plibg <-> (ph /\ (ps /\ (ch /\ (th /\ (ta /\ et)))))))
Distinct variable groups:   B,a,b,c,d,e   B,l,p,q,r,a   L,a,b,c,d,e   L,l,p,q,r   P,a,b,c,d,e   P,p,q,r
Proof of Theorem isplibg
StepHypRef Expression
1 df-plibg 15318 . . . 4 |- Plibg = (Plibg0 i^i (Plibg1 i^i (Plibg2 i^i (Plibg3 i^i (Plibg4a i^i Plibg4b)))))
21a1i 8 . . 3 |- ((L e. A /\ B e. C) -> Plibg = (Plibg0 i^i (Plibg1 i^i (Plibg2 i^i (Plibg3 i^i (Plibg4a i^i Plibg4b))))))
32eleq2d 1964 . 2 |- ((L e. A /\ B e. C) -> (<.L, B>. e. Plibg <-> <.L, B>. e. (Plibg0 i^i (Plibg1 i^i (Plibg2 i^i (Plibg3 i^i (Plibg4a i^i Plibg4b)))))))
4 isplibg.1 . . . . . 6 |- P = U.L
54isplibg0 15307 . . . . 5 |- ((L e. A /\ B e. C) -> (<.L, B>. e. Plibg0 <-> ((L e. Plig /\ Rel B /\ Rel dom B) /\ (dom dom B = P /\ ran dom B = P /\ ran B = P))))
6 isplibg.2 . . . . 5 |- (ph <-> ((L e. Plig /\ Rel B /\ Rel dom B) /\ (dom dom B = P /\ ran dom B = P /\ ran B = P)))
75, 6syl6bbr 597 . . . 4 |- ((L e. A /\ B e. C) -> (<.L, B>. e. Plibg0 <-> ph))
84isplibg1 15309 . . . . . . 7 |- ((L e. A /\ B e. C) -> (<.L, B>. e. Plibg1 <-> A.p e. P A.q e. P A.r e. P (<.<.p, q>., r>. e. B -> (<.<.r, q>., p>. e. B /\ E.l e. L (p e. l /\ q e. l /\ r e. l) /\ (p =/= q /\ p =/= r /\ q =/= r)))))
9 isplibg.3 . . . . . . 7 |- (ps <-> A.p e. P A.q e. P A.r e. P (<.<.p, q>., r>. e. B -> (<.<.r, q>., p>. e. B /\ E.l e. L (p e. l /\ q e. l /\ r e. l) /\ (p =/= q /\ p =/= r /\ q =/= r))))
108, 9syl6bbr 597 . . . . . 6 |- ((L e. A /\ B e. C) -> (<.L, B>. e. Plibg1 <-> ps))
114isplibg2 15311 . . . . . . . . 9 |- ((L e. A /\ B e. C) -> (<.L, B>. e. Plibg2 <-> A.b e. P A.d e. P (b =/= d -> E.a e. P E.c e. P E.e e. P (<.<.a, b>., d>. e. B /\ <.<.b, c>., d>. e. B /\ <.<.b, d>., e>. e. B))))
12 isplibg.4 . . . . . . . . 9 |- (ch <-> A.b e. P A.d e. P (b =/= d -> E.a e. P E.c e. P E.e e. P (<.<.a, b>., d>. e. B /\ <.<.b, c>., d>. e. B /\ <.<.b, d>., e>. e. B)))
1311, 12syl6bbr 597 . . . . . . . 8 |- ((L e. A /\ B e. C) -> (<.L, B>. e. Plibg2 <-> ch))
144isplibg3 15313 . . . . . . . . . . 11 |- ((L e. A /\ B e. C) -> (<.L, B>. e. Plibg3 <-> A.l e. L A.p e. P A.q e. P A.r e. P (((p e. l /\ q e. l /\ r e. l) /\ (p =/= q /\ q =/= r /\ p =/= r)) -> ((<.<.q, p>., r>. e. B /\ -. <.<.p, q>., r>. e. B /\ -. <.<.p, r>., q>. e. B) \/ (-. <.<.q, p>., r>. e. B /\ <.<.p, q>., r>. e. B /\ -. <.<.p, r>., q>. e. B) \/ (-. <.<.q, p>., r>. e. B /\ -. <.<.p, q>., r>. e. B /\ <.<.p, r>., q>. e. B)))))
15 isplibg.5 . . . . . . . . . . 11 |- (th <-> A.l e. L A.p e. P A.q e. P A.r e. P (((p e. l /\ q e. l /\ r e. l) /\ (p =/= q /\ q =/= r /\ p =/= r)) -> ((<.<.q, p>., r>. e. B /\ -. <.<.p, q>., r>. e. B /\ -. <.<.p, r>., q>. e. B) \/ (-. <.<.q, p>., r>. e. B /\ <.<.p, q>., r>. e. B /\ -. <.<.p, r>., q>. e. B) \/ (-. <.<.q, p>., r>. e. B /\ -. <.<.p, q>., r>. e. B /\ <.<.p, r>., q>. e. B))))
1614, 15syl6bbr 597 . . . . . . . . . 10 |- ((L e. A /\ B e. C) -> (<.L, B>. e. Plibg3 <-> th))
174isplibg4a 15315 . . . . . . . . . . . . 13 |- ((L e. A /\ B e. C) -> (<.L, B>. e. Plibg4a <-> A.l e. L A.p e. P A.q e. P A.r e. P (((-. p e. l /\ -. q e. l /\ -. r e. l) /\ ({a e. P | (<.<.p, a>., q>. e. B \/ a = p \/ a = q)} i^i l) = (/) /\ ({a e. P | (<.<.q, a>., r>. e. B \/ a = q \/ a = r)} i^i l) = (/)) -> ({a e. P | (<.<.p, a>., r>. e. B \/ a = p \/ a = r)} i^i l) = (/))))
18 isplibg.6 . . . . . . . . . . . . 13 |- (ta <-> A.l e. L A.p e. P A.q e. P A.r e. P (((-. p e. l /\ -. q e. l /\ -. r e. l) /\ ({a e. P | (<.<.p, a>., q>. e. B \/ a = p \/ a = q)} i^i l) = (/) /\ ({a e. P | (<.<.q, a>., r>. e. B \/ a = q \/ a = r)} i^i l) = (/)) -> ({a e. P | (<.<.p, a>., r>. e. B \/ a = p \/ a = r)} i^i l) = (/)))
1917, 18syl6bbr 597 . . . . . . . . . . . 12 |- ((L e. A /\ B e. C) -> (<.L, B>. e. Plibg4a <-> ta))
204isplibg4b 15317 . . . . . . . . . . . . 13 |- ((L e. A /\ B e. C) -> (<.L, B>. e. Plibg4b <-> A.l e. L A.p e. P A.q e. P A.r e. P (((-. p e. l /\ -. q e. l /\ -. r e. l) /\ (({a e. P | (<.<.p, a>., q>. e. B \/ a = p \/ a = q)} i^i l) =/= (/) /\ ({a e. P | (<.<.q, a>., r>. e. B \/ a = q \/ a = r)} i^i l) =/= (/))) -> ({a e. P | (<.<.p, a>., r>. e. B \/ a = p \/ a = r)} i^i l) = (/))))
21 isplibg.7 . . . . . . . . . . . . 13 |- (et <-> A.l e. L A.p e. P A.q e. P A.r e. P (((-. p e. l /\ -. q e. l /\ -. r e. l) /\ (({a e. P | (<.<.p, a>., q>. e. B \/ a = p \/ a = q)} i^i l) =/= (/) /\ ({a e. P | (<.<.q, a>., r>. e. B \/ a = q \/ a = r)} i^i l) =/= (/))) -> ({a e. P | (<.<.p, a>., r>. e. B \/ a = p \/ a = r)} i^i l) = (/)))
2220, 21syl6bbr 597 . . . . . . . . . . . 12 |- ((L e. A /\ B e. C) -> (<.L, B>. e. Plibg4b <-> et))
2319, 22anbi12d 690 . . . . . . . . . . 11 |- ((L e. A /\ B e. C) -> ((<.L, B>. e. Plibg4a /\ <.L, B>. e. Plibg4b) <-> (ta /\ et)))
24 elin 2786 . . . . . . . . . . 11 |- (<.L, B>. e. (Plibg4a i^i Plibg4b) <-> (<.L, B>. e. Plibg4a /\ <.L, B>. e. Plibg4b))
2523, 24syl5bb 591 . . . . . . . . . 10 |- ((L e. A /\ B e. C) -> (<.L, B>. e. (Plibg4a i^i Plibg4b) <-> (ta /\ et)))
2616, 25anbi12d 690 . . . . . . . . 9 |- ((L e. A /\ B e. C) -> ((<.L, B>. e. Plibg3 /\ <.L, B>. e. (Plibg4a i^i Plibg4b)) <-> (th /\ (ta /\ et))))
27 elin 2786 . . . . . . . . 9 |- (<.L, B>. e. (Plibg3 i^i (Plibg4a i^i Plibg4b)) <-> (<.L, B>. e. Plibg3 /\ <.L, B>. e. (Plibg4a i^i Plibg4b)))
2826, 27syl5bb 591 . . . . . . . 8 |- ((L e. A /\ B e. C) -> (<.L, B>. e. (Plibg3 i^i (Plibg4a i^i Plibg4b)) <-> (th /\ (ta /\ et))))
2913, 28anbi12d 690 . . . . . . 7 |- ((L e. A /\ B e. C) -> ((<.L, B>. e. Plibg2 /\ <.L, B>. e. (Plibg3 i^i (Plibg4a i^i Plibg4b))) <-> (ch /\ (th /\ (ta /\ et)))))
30 elin 2786 . . . . . . 7 |- (<.L, B>. e. (Plibg2 i^i (Plibg3 i^i (Plibg4a i^i Plibg4b))) <-> (<.L, B>. e. Plibg2 /\ <.L, B>. e. (Plibg3 i^i (Plibg4a i^i Plibg4b))))
3129, 30syl5bb 591 . . . . . 6 |- ((L e. A /\ B e. C) -> (<.L, B>. e. (Plibg2 i^i (Plibg3 i^i (Plibg4a i^i Plibg4b))) <-> (ch /\ (th /\ (ta /\ et)))))
3210, 31anbi12d 690 . . . . 5 |- ((L e. A /\ B e. C) -> ((<.L, B>. e. Plibg1 /\ <.L, B>. e. (Plibg2 i^i (Plibg3 i^i (Plibg4a i^i Plibg4b)))) <-> (ps /\ (ch /\ (th /\ (ta /\ et))))))
33 elin 2786 . . . . 5 |- (<.L, B>. e. (Plibg1 i^i (Plibg2 i^i (Plibg3 i^i (Plibg4a i^i Plibg4b)))) <-> (<.L, B>. e. Plibg1 /\ <.L, B>. e. (Plibg2 i^i (Plibg3 i^i (Plibg4a i^i Plibg4b)))))
3432, 33syl5bb 591 . . . 4 |- ((L e. A /\ B e. C) -> (<.L, B>. e. (Plibg1 i^i (Plibg2 i^i (Plibg3 i^i (Plibg4a i^i Plibg4b)))) <-> (ps /\ (ch /\ (th /\ (ta /\ et))))))
357, 34anbi12d 690 . . 3 |- ((L e. A /\ B e. C) -> ((<.L, B>. e. Plibg0 /\ <.L, B>. e. (Plibg1 i^i (Plibg2 i^i (Plibg3 i^i (Plibg4a i^i Plibg4b))))) <-> (ph /\ (ps /\ (ch /\ (th /\ (ta /\ et)))))))
36 elin 2786 . . 3 |- (<.L, B>. e. (Plibg0 i^i (Plibg1 i^i (Plibg2 i^i (Plibg3 i^i (Plibg4a i^i Plibg4b))))) <-> (<.L, B>. e. Plibg0 /\ <.L, B>. e. (Plibg1 i^i (Plibg2 i^i (Plibg3 i^i (Plibg4a i^i Plibg4b))))))
3735, 36syl5bb 591 . 2 |- ((L e. A /\ B e. C) -> (<.L, B>. e. (Plibg0 i^i (Plibg1 i^i (Plibg2 i^i (Plibg3 i^i (Plibg4a i^i Plibg4b))))) <-> (ph /\ (ps /\ (ch /\ (th /\ (ta /\ et)))))))
383, 37bitrd 587 1 |- ((L e. A /\ B e. C) -> (<.L, B>. e. Plibg <-> (ph /\ (ps /\ (ch /\ (th /\ (ta /\ et)))))))
Colors of variables: wff set class
Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   /\ wa 240   \/ w3o 857   /\ w3a 858   = wceq 1298   e. wcel 1300   =/= wne 2017  A.wral 2105  E.wrex 2106  {crab 2108   i^i cin 2592  (/)c0 2875  <.cop 3046  U.cuni 3177  dom cdm 3986  ran crn 3987  Rel wrel 3991  Pligcplig 10343  Plibgcplibg 15295  Plibg0cplibg0 15296  Plibg1cplibg1 15297  Plibg2cplibg2 15298  Plibg3cplibg3 15299  Plibg4acplibg4a 15300  Plibg4bcplibg4b 15301
This theorem is referenced by:  plibgax0 15320  plibgax1 15321  plibgax2 15322  plibgax3 15323  plibgax4a 15324  plibgax4b 15325
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524
This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3or 859  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-rab 2112  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-rel 4001  df-cnv 4002  df-dm 4004  df-rn 4005  df-plibg0 15306  df-plibg1 15308  df-plibg2 15310  df-plibg3 15312  df-plibg4a 15314  df-plibg4b 15316  df-plibg 15318
Copyright terms: Public domain