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

Theorem isperp 26180
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 4963 . . 3 (𝐴(⟂G‘𝐺)𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ (⟂G‘𝐺))
2 df-perpg 26164 . . . . 5 ⟂G = (𝑔 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ran (LineG‘𝑔) ∧ 𝑏 ∈ ran (LineG‘𝑔)) ∧ ∃𝑥 ∈ (𝑎𝑏)∀𝑢𝑎𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝑔))})
3 simpr 485 . . . . . . . . . . . 12 ((𝜑𝑔 = 𝐺) → 𝑔 = 𝐺)
43fveq2d 6542 . . . . . . . . . . 11 ((𝜑𝑔 = 𝐺) → (LineG‘𝑔) = (LineG‘𝐺))
5 isperp.l . . . . . . . . . . 11 𝐿 = (LineG‘𝐺)
64, 5syl6eqr 2849 . . . . . . . . . 10 ((𝜑𝑔 = 𝐺) → (LineG‘𝑔) = 𝐿)
76rneqd 5690 . . . . . . . . 9 ((𝜑𝑔 = 𝐺) → ran (LineG‘𝑔) = ran 𝐿)
87eleq2d 2868 . . . . . . . 8 ((𝜑𝑔 = 𝐺) → (𝑎 ∈ ran (LineG‘𝑔) ↔ 𝑎 ∈ ran 𝐿))
97eleq2d 2868 . . . . . . . 8 ((𝜑𝑔 = 𝐺) → (𝑏 ∈ ran (LineG‘𝑔) ↔ 𝑏 ∈ ran 𝐿))
108, 9anbi12d 630 . . . . . . 7 ((𝜑𝑔 = 𝐺) → ((𝑎 ∈ ran (LineG‘𝑔) ∧ 𝑏 ∈ ran (LineG‘𝑔)) ↔ (𝑎 ∈ ran 𝐿𝑏 ∈ ran 𝐿)))
113fveq2d 6542 . . . . . . . . . 10 ((𝜑𝑔 = 𝐺) → (∟G‘𝑔) = (∟G‘𝐺))
1211eleq2d 2868 . . . . . . . . 9 ((𝜑𝑔 = 𝐺) → (⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝑔) ↔ ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺)))
1312ralbidv 3164 . . . . . . . 8 ((𝜑𝑔 = 𝐺) → (∀𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝑔) ↔ ∀𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺)))
1413rexralbidv 3264 . . . . . . 7 ((𝜑𝑔 = 𝐺) → (∃𝑥 ∈ (𝑎𝑏)∀𝑢𝑎𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝑔) ↔ ∃𝑥 ∈ (𝑎𝑏)∀𝑢𝑎𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺)))
1510, 14anbi12d 630 . . . . . 6 ((𝜑𝑔 = 𝐺) → (((𝑎 ∈ ran (LineG‘𝑔) ∧ 𝑏 ∈ ran (LineG‘𝑔)) ∧ ∃𝑥 ∈ (𝑎𝑏)∀𝑢𝑎𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝑔)) ↔ ((𝑎 ∈ ran 𝐿𝑏 ∈ ran 𝐿) ∧ ∃𝑥 ∈ (𝑎𝑏)∀𝑢𝑎𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺))))
1615opabbidv 5028 . . . . 5 ((𝜑𝑔 = 𝐺) → {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ran (LineG‘𝑔) ∧ 𝑏 ∈ ran (LineG‘𝑔)) ∧ ∃𝑥 ∈ (𝑎𝑏)∀𝑢𝑎𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝑔))} = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ran 𝐿𝑏 ∈ ran 𝐿) ∧ ∃𝑥 ∈ (𝑎𝑏)∀𝑢𝑎𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺))})
17 isperp.g . . . . . 6 (𝜑𝐺 ∈ TarskiG)
1817elexd 3457 . . . . 5 (𝜑𝐺 ∈ V)
195fvexi 6552 . . . . . . . 8 𝐿 ∈ V
20 rnexg 7470 . . . . . . . 8 (𝐿 ∈ V → ran 𝐿 ∈ V)
2119, 20mp1i 13 . . . . . . 7 (𝜑 → ran 𝐿 ∈ V)
2221, 21xpexd 7331 . . . . . 6 (𝜑 → (ran 𝐿 × ran 𝐿) ∈ V)
23 opabssxp 5529 . . . . . . 7 {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ran 𝐿𝑏 ∈ ran 𝐿) ∧ ∃𝑥 ∈ (𝑎𝑏)∀𝑢𝑎𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺))} ⊆ (ran 𝐿 × ran 𝐿)
2423a1i 11 . . . . . 6 (𝜑 → {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ran 𝐿𝑏 ∈ ran 𝐿) ∧ ∃𝑥 ∈ (𝑎𝑏)∀𝑢𝑎𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺))} ⊆ (ran 𝐿 × ran 𝐿))
2522, 24ssexd 5119 . . . . 5 (𝜑 → {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ran 𝐿𝑏 ∈ ran 𝐿) ∧ ∃𝑥 ∈ (𝑎𝑏)∀𝑢𝑎𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺))} ∈ V)
262, 16, 18, 25fvmptd2 6642 . . . 4 (𝜑 → (⟂G‘𝐺) = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ran 𝐿𝑏 ∈ ran 𝐿) ∧ ∃𝑥 ∈ (𝑎𝑏)∀𝑢𝑎𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺))})
2726eleq2d 2868 . . 3 (𝜑 → (⟨𝐴, 𝐵⟩ ∈ (⟂G‘𝐺) ↔ ⟨𝐴, 𝐵⟩ ∈ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ran 𝐿𝑏 ∈ ran 𝐿) ∧ ∃𝑥 ∈ (𝑎𝑏)∀𝑢𝑎𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺))}))
281, 27syl5bb 284 . 2 (𝜑 → (𝐴(⟂G‘𝐺)𝐵 ↔ ⟨𝐴, 𝐵⟩ ∈ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ran 𝐿𝑏 ∈ ran 𝐿) ∧ ∃𝑥 ∈ (𝑎𝑏)∀𝑢𝑎𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺))}))
29 isperp.a . . 3 (𝜑𝐴 ∈ ran 𝐿)
30 isperp.b . . 3 (𝜑𝐵 ∈ ran 𝐿)
31 ineq12 4104 . . . . 5 ((𝑎 = 𝐴𝑏 = 𝐵) → (𝑎𝑏) = (𝐴𝐵))
32 simpll 763 . . . . . 6 (((𝑎 = 𝐴𝑏 = 𝐵) ∧ 𝑥 ∈ (𝑎𝑏)) → 𝑎 = 𝐴)
33 simpllr 772 . . . . . . 7 ((((𝑎 = 𝐴𝑏 = 𝐵) ∧ 𝑥 ∈ (𝑎𝑏)) ∧ 𝑢𝑎) → 𝑏 = 𝐵)
3433raleqdv 3375 . . . . . 6 ((((𝑎 = 𝐴𝑏 = 𝐵) ∧ 𝑥 ∈ (𝑎𝑏)) ∧ 𝑢𝑎) → (∀𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺) ↔ ∀𝑣𝐵 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺)))
3532, 34raleqbidva 3385 . . . . 5 (((𝑎 = 𝐴𝑏 = 𝐵) ∧ 𝑥 ∈ (𝑎𝑏)) → (∀𝑢𝑎𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺) ↔ ∀𝑢𝐴𝑣𝐵 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺)))
3631, 35rexeqbidva 3386 . . . 4 ((𝑎 = 𝐴𝑏 = 𝐵) → (∃𝑥 ∈ (𝑎𝑏)∀𝑢𝑎𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺) ↔ ∃𝑥 ∈ (𝐴𝐵)∀𝑢𝐴𝑣𝐵 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺)))
3736opelopab2a 5312 . . 3 ((𝐴 ∈ ran 𝐿𝐵 ∈ ran 𝐿) → (⟨𝐴, 𝐵⟩ ∈ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ran 𝐿𝑏 ∈ ran 𝐿) ∧ ∃𝑥 ∈ (𝑎𝑏)∀𝑢𝑎𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺))} ↔ ∃𝑥 ∈ (𝐴𝐵)∀𝑢𝐴𝑣𝐵 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺)))
3829, 30, 37syl2anc 584 . 2 (𝜑 → (⟨𝐴, 𝐵⟩ ∈ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ran 𝐿𝑏 ∈ ran 𝐿) ∧ ∃𝑥 ∈ (𝑎𝑏)∀𝑢𝑎𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺))} ↔ ∃𝑥 ∈ (𝐴𝐵)∀𝑢𝐴𝑣𝐵 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺)))
3928, 38bitrd 280 1 (𝜑 → (𝐴(⟂G‘𝐺)𝐵 ↔ ∃𝑥 ∈ (𝐴𝐵)∀𝑢𝐴𝑣𝐵 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396   = wceq 1522  wcel 2081  wral 3105  wrex 3106  Vcvv 3437  cin 3858  wss 3859  cop 4478   class class class wbr 4962  {copab 5024   × cxp 5441  ran crn 5444  cfv 6225  ⟨“cs3 14040  Basecbs 16312  distcds 16403  TarskiGcstrkg 25898  Itvcitv 25904  LineGclng 25905  ∟Gcrag 26161  ⟂Gcperpg 26163
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-13 2344  ax-ext 2769  ax-sep 5094  ax-nul 5101  ax-pow 5157  ax-pr 5221  ax-un 7319
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-3an 1082  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-mo 2576  df-eu 2612  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-ral 3110  df-rex 3111  df-rab 3114  df-v 3439  df-sbc 3707  df-csb 3812  df-dif 3862  df-un 3864  df-in 3866  df-ss 3874  df-nul 4212  df-if 4382  df-pw 4455  df-sn 4473  df-pr 4475  df-op 4479  df-uni 4746  df-br 4963  df-opab 5025  df-mpt 5042  df-id 5348  df-xp 5449  df-rel 5450  df-cnv 5451  df-co 5452  df-dm 5453  df-rn 5454  df-iota 6189  df-fun 6227  df-fv 6233  df-perpg 26164
This theorem is referenced by:  perpcom  26181  perpneq  26182  isperp2  26183
  Copyright terms: Public domain W3C validator