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

Theorem iscgrgd 26317
 Description: The property for two sequences 𝐴 and 𝐵 of points to be congruent. (Contributed by Thierry Arnoux, 3-Apr-2019.)
Hypotheses
Ref Expression
iscgrg.p 𝑃 = (Base‘𝐺)
iscgrg.m = (dist‘𝐺)
iscgrg.e = (cgrG‘𝐺)
iscgrgd.g (𝜑𝐺𝑉)
iscgrgd.d (𝜑𝐷 ⊆ ℝ)
iscgrgd.a (𝜑𝐴:𝐷𝑃)
iscgrgd.b (𝜑𝐵:𝐷𝑃)
Assertion
Ref Expression
iscgrgd (𝜑 → (𝐴 𝐵 ↔ ∀𝑖 ∈ dom 𝐴𝑗 ∈ dom 𝐴((𝐴𝑖) (𝐴𝑗)) = ((𝐵𝑖) (𝐵𝑗))))
Distinct variable groups:   𝑖,𝑗,𝐺   𝐴,𝑖,𝑗   𝐵,𝑖,𝑗
Allowed substitution hints:   𝜑(𝑖,𝑗)   𝐷(𝑖,𝑗)   𝑃(𝑖,𝑗)   (𝑖,𝑗)   (𝑖,𝑗)   𝑉(𝑖,𝑗)

Proof of Theorem iscgrgd
StepHypRef Expression
1 iscgrgd.a . . . . 5 (𝜑𝐴:𝐷𝑃)
2 iscgrgd.d . . . . 5 (𝜑𝐷 ⊆ ℝ)
3 iscgrg.p . . . . . . 7 𝑃 = (Base‘𝐺)
43fvexi 6660 . . . . . 6 𝑃 ∈ V
5 reex 10620 . . . . . 6 ℝ ∈ V
6 elpm2r 8410 . . . . . 6 (((𝑃 ∈ V ∧ ℝ ∈ V) ∧ (𝐴:𝐷𝑃𝐷 ⊆ ℝ)) → 𝐴 ∈ (𝑃pm ℝ))
74, 5, 6mpanl12 701 . . . . 5 ((𝐴:𝐷𝑃𝐷 ⊆ ℝ) → 𝐴 ∈ (𝑃pm ℝ))
81, 2, 7syl2anc 587 . . . 4 (𝜑𝐴 ∈ (𝑃pm ℝ))
9 iscgrgd.b . . . . 5 (𝜑𝐵:𝐷𝑃)
10 elpm2r 8410 . . . . . 6 (((𝑃 ∈ V ∧ ℝ ∈ V) ∧ (𝐵:𝐷𝑃𝐷 ⊆ ℝ)) → 𝐵 ∈ (𝑃pm ℝ))
114, 5, 10mpanl12 701 . . . . 5 ((𝐵:𝐷𝑃𝐷 ⊆ ℝ) → 𝐵 ∈ (𝑃pm ℝ))
129, 2, 11syl2anc 587 . . . 4 (𝜑𝐵 ∈ (𝑃pm ℝ))
138, 12jca 515 . . 3 (𝜑 → (𝐴 ∈ (𝑃pm ℝ) ∧ 𝐵 ∈ (𝑃pm ℝ)))
1413biantrurd 536 . 2 (𝜑 → ((dom 𝐴 = dom 𝐵 ∧ ∀𝑖 ∈ dom 𝐴𝑗 ∈ dom 𝐴((𝐴𝑖) (𝐴𝑗)) = ((𝐵𝑖) (𝐵𝑗))) ↔ ((𝐴 ∈ (𝑃pm ℝ) ∧ 𝐵 ∈ (𝑃pm ℝ)) ∧ (dom 𝐴 = dom 𝐵 ∧ ∀𝑖 ∈ dom 𝐴𝑗 ∈ dom 𝐴((𝐴𝑖) (𝐴𝑗)) = ((𝐵𝑖) (𝐵𝑗))))))
151fdmd 6498 . . . 4 (𝜑 → dom 𝐴 = 𝐷)
169fdmd 6498 . . . 4 (𝜑 → dom 𝐵 = 𝐷)
1715, 16eqtr4d 2836 . . 3 (𝜑 → dom 𝐴 = dom 𝐵)
1817biantrurd 536 . 2 (𝜑 → (∀𝑖 ∈ dom 𝐴𝑗 ∈ dom 𝐴((𝐴𝑖) (𝐴𝑗)) = ((𝐵𝑖) (𝐵𝑗)) ↔ (dom 𝐴 = dom 𝐵 ∧ ∀𝑖 ∈ dom 𝐴𝑗 ∈ dom 𝐴((𝐴𝑖) (𝐴𝑗)) = ((𝐵𝑖) (𝐵𝑗)))))
19 iscgrgd.g . . 3 (𝜑𝐺𝑉)
20 iscgrg.m . . . 4 = (dist‘𝐺)
21 iscgrg.e . . . 4 = (cgrG‘𝐺)
223, 20, 21iscgrg 26316 . . 3 (𝐺𝑉 → (𝐴 𝐵 ↔ ((𝐴 ∈ (𝑃pm ℝ) ∧ 𝐵 ∈ (𝑃pm ℝ)) ∧ (dom 𝐴 = dom 𝐵 ∧ ∀𝑖 ∈ dom 𝐴𝑗 ∈ dom 𝐴((𝐴𝑖) (𝐴𝑗)) = ((𝐵𝑖) (𝐵𝑗))))))
2319, 22syl 17 . 2 (𝜑 → (𝐴 𝐵 ↔ ((𝐴 ∈ (𝑃pm ℝ) ∧ 𝐵 ∈ (𝑃pm ℝ)) ∧ (dom 𝐴 = dom 𝐵 ∧ ∀𝑖 ∈ dom 𝐴𝑗 ∈ dom 𝐴((𝐴𝑖) (𝐴𝑗)) = ((𝐵𝑖) (𝐵𝑗))))))
2414, 18, 233bitr4rd 315 1 (𝜑 → (𝐴 𝐵 ↔ ∀𝑖 ∈ dom 𝐴𝑗 ∈ dom 𝐴((𝐴𝑖) (𝐴𝑗)) = ((𝐵𝑖) (𝐵𝑗))))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ∀wral 3106  Vcvv 3441   ⊆ wss 3881   class class class wbr 5031  dom cdm 5520  ⟶wf 6321  ‘cfv 6325  (class class class)co 7136   ↑pm cpm 8393  ℝcr 10528  Basecbs 16478  distcds 16569  cgrGccgrg 26314 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 5168  ax-nul 5175  ax-pow 5232  ax-pr 5296  ax-un 7444  ax-cnex 10585  ax-resscn 10586 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 3443  df-sbc 3721  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-br 5032  df-opab 5094  df-mpt 5112  df-id 5426  df-xp 5526  df-rel 5527  df-cnv 5528  df-co 5529  df-dm 5530  df-rn 5531  df-iota 6284  df-fun 6327  df-fn 6328  df-f 6329  df-fv 6333  df-ov 7139  df-oprab 7140  df-mpo 7141  df-pm 8395  df-cgrg 26315 This theorem is referenced by:  iscgrglt  26318  trgcgrg  26319  motcgrg  26348
 Copyright terms: Public domain W3C validator