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

Theorem isperp 25325
Description: Property for 2 lines A, B to be perpendicular. Item (ii) of definition 8.11 of [Schwabhauser] p. 59. (Contributed by Thierry Arnoux, 16-Oct-2019.)
Hypotheses
Ref Expression
isperp.p 𝑃 = (Base‘𝐺)
isperp.d = (dist‘𝐺)
isperp.i 𝐼 = (Itv‘𝐺)
isperp.l 𝐿 = (LineG‘𝐺)
isperp.g (𝜑𝐺 ∈ TarskiG)
isperp.a (𝜑𝐴 ∈ ran 𝐿)
isperp.b (𝜑𝐵 ∈ ran 𝐿)
Assertion
Ref Expression
isperp (𝜑 → (𝐴(⟂G‘𝐺)𝐵 ↔ ∃𝑥 ∈ (𝐴𝐵)∀𝑢𝐴𝑣𝐵 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺)))
Distinct variable groups:   𝑣,𝑢,𝑥,𝐴   𝑢,𝐵,𝑣,𝑥   𝑢,𝐺,𝑣,𝑥   𝜑,𝑢,𝑣,𝑥
Allowed substitution hints:   𝑃(𝑥,𝑣,𝑢)   𝐼(𝑥,𝑣,𝑢)   𝐿(𝑥,𝑣,𝑢)   (𝑥,𝑣,𝑢)

Proof of Theorem isperp
Dummy variables 𝑎 𝑏 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-br 4578 . . 3 (𝐴(⟂G‘𝐺)𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ (⟂G‘𝐺))
2 df-perpg 25309 . . . . . 6 ⟂G = (𝑔 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ran (LineG‘𝑔) ∧ 𝑏 ∈ ran (LineG‘𝑔)) ∧ ∃𝑥 ∈ (𝑎𝑏)∀𝑢𝑎𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝑔))})
32a1i 11 . . . . 5 (𝜑 → ⟂G = (𝑔 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ran (LineG‘𝑔) ∧ 𝑏 ∈ ran (LineG‘𝑔)) ∧ ∃𝑥 ∈ (𝑎𝑏)∀𝑢𝑎𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝑔))}))
4 simpr 475 . . . . . . . . . . . 12 ((𝜑𝑔 = 𝐺) → 𝑔 = 𝐺)
54fveq2d 6092 . . . . . . . . . . 11 ((𝜑𝑔 = 𝐺) → (LineG‘𝑔) = (LineG‘𝐺))
6 isperp.l . . . . . . . . . . 11 𝐿 = (LineG‘𝐺)
75, 6syl6eqr 2661 . . . . . . . . . 10 ((𝜑𝑔 = 𝐺) → (LineG‘𝑔) = 𝐿)
87rneqd 5261 . . . . . . . . 9 ((𝜑𝑔 = 𝐺) → ran (LineG‘𝑔) = ran 𝐿)
98eleq2d 2672 . . . . . . . 8 ((𝜑𝑔 = 𝐺) → (𝑎 ∈ ran (LineG‘𝑔) ↔ 𝑎 ∈ ran 𝐿))
108eleq2d 2672 . . . . . . . 8 ((𝜑𝑔 = 𝐺) → (𝑏 ∈ ran (LineG‘𝑔) ↔ 𝑏 ∈ ran 𝐿))
119, 10anbi12d 742 . . . . . . 7 ((𝜑𝑔 = 𝐺) → ((𝑎 ∈ ran (LineG‘𝑔) ∧ 𝑏 ∈ ran (LineG‘𝑔)) ↔ (𝑎 ∈ ran 𝐿𝑏 ∈ ran 𝐿)))
124fveq2d 6092 . . . . . . . . . 10 ((𝜑𝑔 = 𝐺) → (∟G‘𝑔) = (∟G‘𝐺))
1312eleq2d 2672 . . . . . . . . 9 ((𝜑𝑔 = 𝐺) → (⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝑔) ↔ ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺)))
1413ralbidv 2968 . . . . . . . 8 ((𝜑𝑔 = 𝐺) → (∀𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝑔) ↔ ∀𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺)))
1514rexralbidv 3039 . . . . . . 7 ((𝜑𝑔 = 𝐺) → (∃𝑥 ∈ (𝑎𝑏)∀𝑢𝑎𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝑔) ↔ ∃𝑥 ∈ (𝑎𝑏)∀𝑢𝑎𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺)))
1611, 15anbi12d 742 . . . . . 6 ((𝜑𝑔 = 𝐺) → (((𝑎 ∈ ran (LineG‘𝑔) ∧ 𝑏 ∈ ran (LineG‘𝑔)) ∧ ∃𝑥 ∈ (𝑎𝑏)∀𝑢𝑎𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝑔)) ↔ ((𝑎 ∈ ran 𝐿𝑏 ∈ ran 𝐿) ∧ ∃𝑥 ∈ (𝑎𝑏)∀𝑢𝑎𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺))))
1716opabbidv 4642 . . . . 5 ((𝜑𝑔 = 𝐺) → {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ran (LineG‘𝑔) ∧ 𝑏 ∈ ran (LineG‘𝑔)) ∧ ∃𝑥 ∈ (𝑎𝑏)∀𝑢𝑎𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝑔))} = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ran 𝐿𝑏 ∈ ran 𝐿) ∧ ∃𝑥 ∈ (𝑎𝑏)∀𝑢𝑎𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺))})
18 isperp.g . . . . . 6 (𝜑𝐺 ∈ TarskiG)
19 elex 3184 . . . . . 6 (𝐺 ∈ TarskiG → 𝐺 ∈ V)
2018, 19syl 17 . . . . 5 (𝜑𝐺 ∈ V)
21 fvex 6098 . . . . . . . . 9 (LineG‘𝐺) ∈ V
226, 21eqeltri 2683 . . . . . . . 8 𝐿 ∈ V
23 rnexg 6967 . . . . . . . 8 (𝐿 ∈ V → ran 𝐿 ∈ V)
2422, 23mp1i 13 . . . . . . 7 (𝜑 → ran 𝐿 ∈ V)
25 xpexg 6835 . . . . . . 7 ((ran 𝐿 ∈ V ∧ ran 𝐿 ∈ V) → (ran 𝐿 × ran 𝐿) ∈ V)
2624, 24, 25syl2anc 690 . . . . . 6 (𝜑 → (ran 𝐿 × ran 𝐿) ∈ V)
27 opabssxp 5106 . . . . . . 7 {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ran 𝐿𝑏 ∈ ran 𝐿) ∧ ∃𝑥 ∈ (𝑎𝑏)∀𝑢𝑎𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺))} ⊆ (ran 𝐿 × ran 𝐿)
2827a1i 11 . . . . . 6 (𝜑 → {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ran 𝐿𝑏 ∈ ran 𝐿) ∧ ∃𝑥 ∈ (𝑎𝑏)∀𝑢𝑎𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺))} ⊆ (ran 𝐿 × ran 𝐿))
2926, 28ssexd 4728 . . . . 5 (𝜑 → {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ran 𝐿𝑏 ∈ ran 𝐿) ∧ ∃𝑥 ∈ (𝑎𝑏)∀𝑢𝑎𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺))} ∈ V)
303, 17, 20, 29fvmptd 6182 . . . 4 (𝜑 → (⟂G‘𝐺) = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ran 𝐿𝑏 ∈ ran 𝐿) ∧ ∃𝑥 ∈ (𝑎𝑏)∀𝑢𝑎𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺))})
3130eleq2d 2672 . . 3 (𝜑 → (⟨𝐴, 𝐵⟩ ∈ (⟂G‘𝐺) ↔ ⟨𝐴, 𝐵⟩ ∈ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ran 𝐿𝑏 ∈ ran 𝐿) ∧ ∃𝑥 ∈ (𝑎𝑏)∀𝑢𝑎𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺))}))
321, 31syl5bb 270 . 2 (𝜑 → (𝐴(⟂G‘𝐺)𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ran 𝐿𝑏 ∈ ran 𝐿) ∧ ∃𝑥 ∈ (𝑎𝑏)∀𝑢𝑎𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺))}))
33 isperp.a . . 3 (𝜑𝐴 ∈ ran 𝐿)
34 isperp.b . . 3 (𝜑𝐵 ∈ ran 𝐿)
35 ineq12 3770 . . . . 5 ((𝑎 = 𝐴𝑏 = 𝐵) → (𝑎𝑏) = (𝐴𝐵))
36 simpll 785 . . . . . 6 (((𝑎 = 𝐴𝑏 = 𝐵) ∧ 𝑥 ∈ (𝑎𝑏)) → 𝑎 = 𝐴)
37 simpllr 794 . . . . . . 7 ((((𝑎 = 𝐴𝑏 = 𝐵) ∧ 𝑥 ∈ (𝑎𝑏)) ∧ 𝑢𝑎) → 𝑏 = 𝐵)
3837raleqdv 3120 . . . . . 6 ((((𝑎 = 𝐴𝑏 = 𝐵) ∧ 𝑥 ∈ (𝑎𝑏)) ∧ 𝑢𝑎) → (∀𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺) ↔ ∀𝑣𝐵 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺)))
3936, 38raleqbidva 3130 . . . . 5 (((𝑎 = 𝐴𝑏 = 𝐵) ∧ 𝑥 ∈ (𝑎𝑏)) → (∀𝑢𝑎𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺) ↔ ∀𝑢𝐴𝑣𝐵 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺)))
4035, 39rexeqbidva 3131 . . . 4 ((𝑎 = 𝐴𝑏 = 𝐵) → (∃𝑥 ∈ (𝑎𝑏)∀𝑢𝑎𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺) ↔ ∃𝑥 ∈ (𝐴𝐵)∀𝑢𝐴𝑣𝐵 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺)))
4140opelopab2a 4905 . . 3 ((𝐴 ∈ ran 𝐿𝐵 ∈ ran 𝐿) → (⟨𝐴, 𝐵⟩ ∈ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ran 𝐿𝑏 ∈ ran 𝐿) ∧ ∃𝑥 ∈ (𝑎𝑏)∀𝑢𝑎𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺))} ↔ ∃𝑥 ∈ (𝐴𝐵)∀𝑢𝐴𝑣𝐵 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺)))
4233, 34, 41syl2anc 690 . 2 (𝜑 → (⟨𝐴, 𝐵⟩ ∈ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ran 𝐿𝑏 ∈ ran 𝐿) ∧ ∃𝑥 ∈ (𝑎𝑏)∀𝑢𝑎𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺))} ↔ ∃𝑥 ∈ (𝐴𝐵)∀𝑢𝐴𝑣𝐵 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺)))
4332, 42bitrd 266 1 (𝜑 → (𝐴(⟂G‘𝐺)𝐵 ↔ ∃𝑥 ∈ (𝐴𝐵)∀𝑢𝐴𝑣𝐵 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382   = wceq 1474  wcel 1976  wral 2895  wrex 2896  Vcvv 3172  cin 3538  wss 3539  cop 4130   class class class wbr 4577  {copab 4636  cmpt 4637   × cxp 5026  ran crn 5029  cfv 5790  ⟨“cs3 13384  Basecbs 15641  distcds 15723  TarskiGcstrkg 25046  Itvcitv 25052  LineGclng 25053  ∟Gcrag 25306  ⟂Gcperpg 25308
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-8 1978  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pow 4764  ax-pr 4828  ax-un 6824
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-sbc 3402  df-csb 3499  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-pw 4109  df-sn 4125  df-pr 4127  df-op 4131  df-uni 4367  df-br 4578  df-opab 4638  df-mpt 4639  df-id 4943  df-xp 5034  df-rel 5035  df-cnv 5036  df-co 5037  df-dm 5038  df-rn 5039  df-iota 5754  df-fun 5792  df-fv 5798  df-perpg 25309
This theorem is referenced by:  perpcom  25326  perpneq  25327  isperp2  25328
  Copyright terms: Public domain W3C validator