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

Theorem perpln2 26549
 Description: Derive a line from perpendicularity. (Contributed by Thierry Arnoux, 27-Nov-2019.)
Hypotheses
Ref Expression
perpln.l 𝐿 = (LineG‘𝐺)
perpln.1 (𝜑𝐺 ∈ TarskiG)
perpln.2 (𝜑𝐴(⟂G‘𝐺)𝐵)
Assertion
Ref Expression
perpln2 (𝜑𝐵 ∈ ran 𝐿)

Proof of Theorem perpln2
Dummy variables 𝑎 𝑏 𝑔 𝑢 𝑣 𝑥 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-perpg 26534 . . . . . 6 ⟂G = (𝑔 ∈ V ↦ {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ran (LineG‘𝑔) ∧ 𝑏 ∈ ran (LineG‘𝑔)) ∧ ∃𝑥 ∈ (𝑎𝑏)∀𝑢𝑎𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝑔))})
2 simpr 488 . . . . . . . . . . . . 13 ((𝜑𝑔 = 𝐺) → 𝑔 = 𝐺)
32fveq2d 6659 . . . . . . . . . . . 12 ((𝜑𝑔 = 𝐺) → (LineG‘𝑔) = (LineG‘𝐺))
4 perpln.l . . . . . . . . . . . 12 𝐿 = (LineG‘𝐺)
53, 4eqtr4di 2851 . . . . . . . . . . 11 ((𝜑𝑔 = 𝐺) → (LineG‘𝑔) = 𝐿)
65rneqd 5778 . . . . . . . . . 10 ((𝜑𝑔 = 𝐺) → ran (LineG‘𝑔) = ran 𝐿)
76eleq2d 2875 . . . . . . . . 9 ((𝜑𝑔 = 𝐺) → (𝑎 ∈ ran (LineG‘𝑔) ↔ 𝑎 ∈ ran 𝐿))
86eleq2d 2875 . . . . . . . . 9 ((𝜑𝑔 = 𝐺) → (𝑏 ∈ ran (LineG‘𝑔) ↔ 𝑏 ∈ ran 𝐿))
97, 8anbi12d 633 . . . . . . . 8 ((𝜑𝑔 = 𝐺) → ((𝑎 ∈ ran (LineG‘𝑔) ∧ 𝑏 ∈ ran (LineG‘𝑔)) ↔ (𝑎 ∈ ran 𝐿𝑏 ∈ ran 𝐿)))
102fveq2d 6659 . . . . . . . . . . 11 ((𝜑𝑔 = 𝐺) → (∟G‘𝑔) = (∟G‘𝐺))
1110eleq2d 2875 . . . . . . . . . 10 ((𝜑𝑔 = 𝐺) → (⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝑔) ↔ ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺)))
1211ralbidv 3162 . . . . . . . . 9 ((𝜑𝑔 = 𝐺) → (∀𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝑔) ↔ ∀𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺)))
1312rexralbidv 3261 . . . . . . . 8 ((𝜑𝑔 = 𝐺) → (∃𝑥 ∈ (𝑎𝑏)∀𝑢𝑎𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝑔) ↔ ∃𝑥 ∈ (𝑎𝑏)∀𝑢𝑎𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺)))
149, 13anbi12d 633 . . . . . . 7 ((𝜑𝑔 = 𝐺) → (((𝑎 ∈ ran (LineG‘𝑔) ∧ 𝑏 ∈ ran (LineG‘𝑔)) ∧ ∃𝑥 ∈ (𝑎𝑏)∀𝑢𝑎𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝑔)) ↔ ((𝑎 ∈ ran 𝐿𝑏 ∈ ran 𝐿) ∧ ∃𝑥 ∈ (𝑎𝑏)∀𝑢𝑎𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺))))
1514opabbidv 5100 . . . . . 6 ((𝜑𝑔 = 𝐺) → {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ran (LineG‘𝑔) ∧ 𝑏 ∈ ran (LineG‘𝑔)) ∧ ∃𝑥 ∈ (𝑎𝑏)∀𝑢𝑎𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝑔))} = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ran 𝐿𝑏 ∈ ran 𝐿) ∧ ∃𝑥 ∈ (𝑎𝑏)∀𝑢𝑎𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺))})
16 perpln.1 . . . . . . 7 (𝜑𝐺 ∈ TarskiG)
1716elexd 3462 . . . . . 6 (𝜑𝐺 ∈ V)
184fvexi 6669 . . . . . . . . 9 𝐿 ∈ V
19 rnexg 7608 . . . . . . . . 9 (𝐿 ∈ V → ran 𝐿 ∈ V)
2018, 19mp1i 13 . . . . . . . 8 (𝜑 → ran 𝐿 ∈ V)
2120, 20xpexd 7467 . . . . . . 7 (𝜑 → (ran 𝐿 × ran 𝐿) ∈ V)
22 opabssxp 5611 . . . . . . . 8 {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ran 𝐿𝑏 ∈ ran 𝐿) ∧ ∃𝑥 ∈ (𝑎𝑏)∀𝑢𝑎𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺))} ⊆ (ran 𝐿 × ran 𝐿)
2322a1i 11 . . . . . . 7 (𝜑 → {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ran 𝐿𝑏 ∈ ran 𝐿) ∧ ∃𝑥 ∈ (𝑎𝑏)∀𝑢𝑎𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺))} ⊆ (ran 𝐿 × ran 𝐿))
2421, 23ssexd 5196 . . . . . 6 (𝜑 → {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ran 𝐿𝑏 ∈ ran 𝐿) ∧ ∃𝑥 ∈ (𝑎𝑏)∀𝑢𝑎𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺))} ∈ V)
251, 15, 17, 24fvmptd2 6763 . . . . 5 (𝜑 → (⟂G‘𝐺) = {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ran 𝐿𝑏 ∈ ran 𝐿) ∧ ∃𝑥 ∈ (𝑎𝑏)∀𝑢𝑎𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺))})
2625rneqd 5778 . . . 4 (𝜑 → ran (⟂G‘𝐺) = ran {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ran 𝐿𝑏 ∈ ran 𝐿) ∧ ∃𝑥 ∈ (𝑎𝑏)∀𝑢𝑎𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺))})
2722rnssi 5780 . . . 4 ran {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ran 𝐿𝑏 ∈ ran 𝐿) ∧ ∃𝑥 ∈ (𝑎𝑏)∀𝑢𝑎𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺))} ⊆ ran (ran 𝐿 × ran 𝐿)
2826, 27eqsstrdi 3971 . . 3 (𝜑 → ran (⟂G‘𝐺) ⊆ ran (ran 𝐿 × ran 𝐿))
29 rnxpss 6000 . . 3 ran (ran 𝐿 × ran 𝐿) ⊆ ran 𝐿
3028, 29sstrdi 3929 . 2 (𝜑 → ran (⟂G‘𝐺) ⊆ ran 𝐿)
31 relopab 5664 . . . . . 6 Rel {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ran 𝐿𝑏 ∈ ran 𝐿) ∧ ∃𝑥 ∈ (𝑎𝑏)∀𝑢𝑎𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺))}
3225releqd 5621 . . . . . 6 (𝜑 → (Rel (⟂G‘𝐺) ↔ Rel {⟨𝑎, 𝑏⟩ ∣ ((𝑎 ∈ ran 𝐿𝑏 ∈ ran 𝐿) ∧ ∃𝑥 ∈ (𝑎𝑏)∀𝑢𝑎𝑣𝑏 ⟨“𝑢𝑥𝑣”⟩ ∈ (∟G‘𝐺))}))
3331, 32mpbiri 261 . . . . 5 (𝜑 → Rel (⟂G‘𝐺))
34 perpln.2 . . . . 5 (𝜑𝐴(⟂G‘𝐺)𝐵)
35 brrelex12 5572 . . . . 5 ((Rel (⟂G‘𝐺) ∧ 𝐴(⟂G‘𝐺)𝐵) → (𝐴 ∈ V ∧ 𝐵 ∈ V))
3633, 34, 35syl2anc 587 . . . 4 (𝜑 → (𝐴 ∈ V ∧ 𝐵 ∈ V))
3736simpld 498 . . 3 (𝜑𝐴 ∈ V)
3836simprd 499 . . 3 (𝜑𝐵 ∈ V)
39 brelrng 5781 . . 3 ((𝐴 ∈ V ∧ 𝐵 ∈ V ∧ 𝐴(⟂G‘𝐺)𝐵) → 𝐵 ∈ ran (⟂G‘𝐺))
4037, 38, 34, 39syl3anc 1368 . 2 (𝜑𝐵 ∈ ran (⟂G‘𝐺))
4130, 40sseldd 3918 1 (𝜑𝐵 ∈ ran 𝐿)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ∀wral 3106  ∃wrex 3107  Vcvv 3442   ∩ cin 3882   ⊆ wss 3883   class class class wbr 5034  {copab 5096   × cxp 5521  ran crn 5524  Rel wrel 5528  ‘cfv 6332  ⟨“cs3 14215  TarskiGcstrkg 26268  LineGclng 26275  ∟Gcrag 26531  ⟂Gcperpg 26533 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5171  ax-nul 5178  ax-pow 5235  ax-pr 5299  ax-un 7454 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 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-rab 3115  df-v 3444  df-sbc 3723  df-csb 3831  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4247  df-if 4429  df-pw 4502  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4805  df-br 5035  df-opab 5097  df-mpt 5115  df-id 5429  df-xp 5529  df-rel 5530  df-cnv 5531  df-co 5532  df-dm 5533  df-rn 5534  df-iota 6291  df-fun 6334  df-fv 6340  df-perpg 26534 This theorem is referenced by:  hlperpnel  26563  mideulem2  26572  opphllem  26573  opphllem3  26587  opphllem5  26589  opphllem6  26590  trgcopy  26642
 Copyright terms: Public domain W3C validator