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

Theorem ltgseg 27246
Description: The set 𝐸 denotes the possible values of the congruence. (Contributed by Thierry Arnoux, 15-Dec-2019.)
Hypotheses
Ref Expression
legval.p 𝑃 = (Baseβ€˜πΊ)
legval.d βˆ’ = (distβ€˜πΊ)
legval.i 𝐼 = (Itvβ€˜πΊ)
legval.l ≀ = (≀Gβ€˜πΊ)
legval.g (πœ‘ β†’ 𝐺 ∈ TarskiG)
legso.a 𝐸 = ( βˆ’ β€œ (𝑃 Γ— 𝑃))
legso.f (πœ‘ β†’ Fun βˆ’ )
ltgseg.p (πœ‘ β†’ 𝐴 ∈ 𝐸)
Assertion
Ref Expression
ltgseg (πœ‘ β†’ βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 𝐴 = (π‘₯ βˆ’ 𝑦))
Distinct variable groups:   π‘₯, βˆ’ ,𝑦   π‘₯,𝐴,𝑦   π‘₯,𝑃,𝑦   πœ‘,π‘₯,𝑦
Allowed substitution hints:   𝐸(π‘₯,𝑦)   𝐺(π‘₯,𝑦)   𝐼(π‘₯,𝑦)   ≀ (π‘₯,𝑦)

Proof of Theorem ltgseg
Dummy variable π‘Ž is distinct from all other variables.
StepHypRef Expression
1 simp-4r 781 . . . . 5 ((((((πœ‘ ∧ π‘Ž ∈ (𝑃 Γ— 𝑃)) ∧ ( βˆ’ β€˜π‘Ž) = 𝐴) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ π‘Ž = ⟨π‘₯, π‘¦βŸ©) β†’ ( βˆ’ β€˜π‘Ž) = 𝐴)
2 simpr 485 . . . . . 6 ((((((πœ‘ ∧ π‘Ž ∈ (𝑃 Γ— 𝑃)) ∧ ( βˆ’ β€˜π‘Ž) = 𝐴) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ π‘Ž = ⟨π‘₯, π‘¦βŸ©) β†’ π‘Ž = ⟨π‘₯, π‘¦βŸ©)
32fveq2d 6829 . . . . 5 ((((((πœ‘ ∧ π‘Ž ∈ (𝑃 Γ— 𝑃)) ∧ ( βˆ’ β€˜π‘Ž) = 𝐴) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ π‘Ž = ⟨π‘₯, π‘¦βŸ©) β†’ ( βˆ’ β€˜π‘Ž) = ( βˆ’ β€˜βŸ¨π‘₯, π‘¦βŸ©))
41, 3eqtr3d 2778 . . . 4 ((((((πœ‘ ∧ π‘Ž ∈ (𝑃 Γ— 𝑃)) ∧ ( βˆ’ β€˜π‘Ž) = 𝐴) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ π‘Ž = ⟨π‘₯, π‘¦βŸ©) β†’ 𝐴 = ( βˆ’ β€˜βŸ¨π‘₯, π‘¦βŸ©))
5 df-ov 7340 . . . 4 (π‘₯ βˆ’ 𝑦) = ( βˆ’ β€˜βŸ¨π‘₯, π‘¦βŸ©)
64, 5eqtr4di 2794 . . 3 ((((((πœ‘ ∧ π‘Ž ∈ (𝑃 Γ— 𝑃)) ∧ ( βˆ’ β€˜π‘Ž) = 𝐴) ∧ π‘₯ ∈ 𝑃) ∧ 𝑦 ∈ 𝑃) ∧ π‘Ž = ⟨π‘₯, π‘¦βŸ©) β†’ 𝐴 = (π‘₯ βˆ’ 𝑦))
7 simplr 766 . . . 4 (((πœ‘ ∧ π‘Ž ∈ (𝑃 Γ— 𝑃)) ∧ ( βˆ’ β€˜π‘Ž) = 𝐴) β†’ π‘Ž ∈ (𝑃 Γ— 𝑃))
8 elxp2 5644 . . . 4 (π‘Ž ∈ (𝑃 Γ— 𝑃) ↔ βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 π‘Ž = ⟨π‘₯, π‘¦βŸ©)
97, 8sylib 217 . . 3 (((πœ‘ ∧ π‘Ž ∈ (𝑃 Γ— 𝑃)) ∧ ( βˆ’ β€˜π‘Ž) = 𝐴) β†’ βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 π‘Ž = ⟨π‘₯, π‘¦βŸ©)
106, 9reximddv2 3202 . 2 (((πœ‘ ∧ π‘Ž ∈ (𝑃 Γ— 𝑃)) ∧ ( βˆ’ β€˜π‘Ž) = 𝐴) β†’ βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 𝐴 = (π‘₯ βˆ’ 𝑦))
11 legso.f . . 3 (πœ‘ β†’ Fun βˆ’ )
12 ltgseg.p . . . 4 (πœ‘ β†’ 𝐴 ∈ 𝐸)
13 legso.a . . . 4 𝐸 = ( βˆ’ β€œ (𝑃 Γ— 𝑃))
1412, 13eleqtrdi 2847 . . 3 (πœ‘ β†’ 𝐴 ∈ ( βˆ’ β€œ (𝑃 Γ— 𝑃)))
15 fvelima 6891 . . 3 ((Fun βˆ’ ∧ 𝐴 ∈ ( βˆ’ β€œ (𝑃 Γ— 𝑃))) β†’ βˆƒπ‘Ž ∈ (𝑃 Γ— 𝑃)( βˆ’ β€˜π‘Ž) = 𝐴)
1611, 14, 15syl2anc 584 . 2 (πœ‘ β†’ βˆƒπ‘Ž ∈ (𝑃 Γ— 𝑃)( βˆ’ β€˜π‘Ž) = 𝐴)
1710, 16r19.29a 3155 1 (πœ‘ β†’ βˆƒπ‘₯ ∈ 𝑃 βˆƒπ‘¦ ∈ 𝑃 𝐴 = (π‘₯ βˆ’ 𝑦))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 396   = wceq 1540   ∈ wcel 2105  βˆƒwrex 3070  βŸ¨cop 4579   Γ— cxp 5618   β€œ cima 5623  Fun wfun 6473  β€˜cfv 6479  (class class class)co 7337  Basecbs 17009  distcds 17068  TarskiGcstrkg 27077  Itvcitv 27083  β‰€Gcleg 27232
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-12 2170  ax-ext 2707  ax-sep 5243  ax-nul 5250  ax-pr 5372
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-ral 3062  df-rex 3071  df-rab 3404  df-v 3443  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4270  df-if 4474  df-sn 4574  df-pr 4576  df-op 4580  df-uni 4853  df-br 5093  df-opab 5155  df-id 5518  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-iota 6431  df-fun 6481  df-fv 6487  df-ov 7340
This theorem is referenced by:  legso  27249
  Copyright terms: Public domain W3C validator