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

Theorem iscgrg 28018
Description: The congruence property for sequences of points. (Contributed by Thierry Arnoux, 3-Apr-2019.)
Hypotheses
Ref Expression
iscgrg.p 𝑃 = (Baseβ€˜πΊ)
iscgrg.m βˆ’ = (distβ€˜πΊ)
iscgrg.e ∼ = (cgrGβ€˜πΊ)
Assertion
Ref Expression
iscgrg (𝐺 ∈ 𝑉 β†’ (𝐴 ∼ 𝐡 ↔ ((𝐴 ∈ (𝑃 ↑pm ℝ) ∧ 𝐡 ∈ (𝑃 ↑pm ℝ)) ∧ (dom 𝐴 = dom 𝐡 ∧ βˆ€π‘– ∈ dom π΄βˆ€π‘— ∈ dom 𝐴((π΄β€˜π‘–) βˆ’ (π΄β€˜π‘—)) = ((π΅β€˜π‘–) βˆ’ (π΅β€˜π‘—))))))
Distinct variable groups:   𝑖,𝑗,𝐺   𝐴,𝑖,𝑗   𝐡,𝑖,𝑗
Allowed substitution hints:   𝑃(𝑖,𝑗)   ∼ (𝑖,𝑗)   βˆ’ (𝑖,𝑗)   𝑉(𝑖,𝑗)

Proof of Theorem iscgrg
Dummy variables π‘Ž 𝑏 𝑔 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 iscgrg.e . . . 4 ∼ = (cgrGβ€˜πΊ)
2 elex 3492 . . . . 5 (𝐺 ∈ 𝑉 β†’ 𝐺 ∈ V)
3 fveq2 6891 . . . . . . . . . . . 12 (𝑔 = 𝐺 β†’ (Baseβ€˜π‘”) = (Baseβ€˜πΊ))
4 iscgrg.p . . . . . . . . . . . 12 𝑃 = (Baseβ€˜πΊ)
53, 4eqtr4di 2790 . . . . . . . . . . 11 (𝑔 = 𝐺 β†’ (Baseβ€˜π‘”) = 𝑃)
65oveq1d 7426 . . . . . . . . . 10 (𝑔 = 𝐺 β†’ ((Baseβ€˜π‘”) ↑pm ℝ) = (𝑃 ↑pm ℝ))
76eleq2d 2819 . . . . . . . . 9 (𝑔 = 𝐺 β†’ (π‘Ž ∈ ((Baseβ€˜π‘”) ↑pm ℝ) ↔ π‘Ž ∈ (𝑃 ↑pm ℝ)))
86eleq2d 2819 . . . . . . . . 9 (𝑔 = 𝐺 β†’ (𝑏 ∈ ((Baseβ€˜π‘”) ↑pm ℝ) ↔ 𝑏 ∈ (𝑃 ↑pm ℝ)))
97, 8anbi12d 631 . . . . . . . 8 (𝑔 = 𝐺 β†’ ((π‘Ž ∈ ((Baseβ€˜π‘”) ↑pm ℝ) ∧ 𝑏 ∈ ((Baseβ€˜π‘”) ↑pm ℝ)) ↔ (π‘Ž ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ))))
10 fveq2 6891 . . . . . . . . . . . . 13 (𝑔 = 𝐺 β†’ (distβ€˜π‘”) = (distβ€˜πΊ))
11 iscgrg.m . . . . . . . . . . . . 13 βˆ’ = (distβ€˜πΊ)
1210, 11eqtr4di 2790 . . . . . . . . . . . 12 (𝑔 = 𝐺 β†’ (distβ€˜π‘”) = βˆ’ )
1312oveqd 7428 . . . . . . . . . . 11 (𝑔 = 𝐺 β†’ ((π‘Žβ€˜π‘–)(distβ€˜π‘”)(π‘Žβ€˜π‘—)) = ((π‘Žβ€˜π‘–) βˆ’ (π‘Žβ€˜π‘—)))
1412oveqd 7428 . . . . . . . . . . 11 (𝑔 = 𝐺 β†’ ((π‘β€˜π‘–)(distβ€˜π‘”)(π‘β€˜π‘—)) = ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—)))
1513, 14eqeq12d 2748 . . . . . . . . . 10 (𝑔 = 𝐺 β†’ (((π‘Žβ€˜π‘–)(distβ€˜π‘”)(π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–)(distβ€˜π‘”)(π‘β€˜π‘—)) ↔ ((π‘Žβ€˜π‘–) βˆ’ (π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—))))
16152ralbidv 3218 . . . . . . . . 9 (𝑔 = 𝐺 β†’ (βˆ€π‘– ∈ dom π‘Žβˆ€π‘— ∈ dom π‘Ž((π‘Žβ€˜π‘–)(distβ€˜π‘”)(π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–)(distβ€˜π‘”)(π‘β€˜π‘—)) ↔ βˆ€π‘– ∈ dom π‘Žβˆ€π‘— ∈ dom π‘Ž((π‘Žβ€˜π‘–) βˆ’ (π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—))))
1716anbi2d 629 . . . . . . . 8 (𝑔 = 𝐺 β†’ ((dom π‘Ž = dom 𝑏 ∧ βˆ€π‘– ∈ dom π‘Žβˆ€π‘— ∈ dom π‘Ž((π‘Žβ€˜π‘–)(distβ€˜π‘”)(π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–)(distβ€˜π‘”)(π‘β€˜π‘—))) ↔ (dom π‘Ž = dom 𝑏 ∧ βˆ€π‘– ∈ dom π‘Žβˆ€π‘— ∈ dom π‘Ž((π‘Žβ€˜π‘–) βˆ’ (π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—)))))
189, 17anbi12d 631 . . . . . . 7 (𝑔 = 𝐺 β†’ (((π‘Ž ∈ ((Baseβ€˜π‘”) ↑pm ℝ) ∧ 𝑏 ∈ ((Baseβ€˜π‘”) ↑pm ℝ)) ∧ (dom π‘Ž = dom 𝑏 ∧ βˆ€π‘– ∈ dom π‘Žβˆ€π‘— ∈ dom π‘Ž((π‘Žβ€˜π‘–)(distβ€˜π‘”)(π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–)(distβ€˜π‘”)(π‘β€˜π‘—)))) ↔ ((π‘Ž ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom π‘Ž = dom 𝑏 ∧ βˆ€π‘– ∈ dom π‘Žβˆ€π‘— ∈ dom π‘Ž((π‘Žβ€˜π‘–) βˆ’ (π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—))))))
1918opabbidv 5214 . . . . . 6 (𝑔 = 𝐺 β†’ {βŸ¨π‘Ž, π‘βŸ© ∣ ((π‘Ž ∈ ((Baseβ€˜π‘”) ↑pm ℝ) ∧ 𝑏 ∈ ((Baseβ€˜π‘”) ↑pm ℝ)) ∧ (dom π‘Ž = dom 𝑏 ∧ βˆ€π‘– ∈ dom π‘Žβˆ€π‘— ∈ dom π‘Ž((π‘Žβ€˜π‘–)(distβ€˜π‘”)(π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–)(distβ€˜π‘”)(π‘β€˜π‘—))))} = {βŸ¨π‘Ž, π‘βŸ© ∣ ((π‘Ž ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom π‘Ž = dom 𝑏 ∧ βˆ€π‘– ∈ dom π‘Žβˆ€π‘— ∈ dom π‘Ž((π‘Žβ€˜π‘–) βˆ’ (π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—))))})
20 df-cgrg 28017 . . . . . 6 cgrG = (𝑔 ∈ V ↦ {βŸ¨π‘Ž, π‘βŸ© ∣ ((π‘Ž ∈ ((Baseβ€˜π‘”) ↑pm ℝ) ∧ 𝑏 ∈ ((Baseβ€˜π‘”) ↑pm ℝ)) ∧ (dom π‘Ž = dom 𝑏 ∧ βˆ€π‘– ∈ dom π‘Žβˆ€π‘— ∈ dom π‘Ž((π‘Žβ€˜π‘–)(distβ€˜π‘”)(π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–)(distβ€˜π‘”)(π‘β€˜π‘—))))})
21 df-xp 5682 . . . . . . . 8 ((𝑃 ↑pm ℝ) Γ— (𝑃 ↑pm ℝ)) = {βŸ¨π‘Ž, π‘βŸ© ∣ (π‘Ž ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ))}
22 ovex 7444 . . . . . . . . 9 (𝑃 ↑pm ℝ) ∈ V
2322, 22xpex 7742 . . . . . . . 8 ((𝑃 ↑pm ℝ) Γ— (𝑃 ↑pm ℝ)) ∈ V
2421, 23eqeltrri 2830 . . . . . . 7 {βŸ¨π‘Ž, π‘βŸ© ∣ (π‘Ž ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ))} ∈ V
25 simpl 483 . . . . . . . 8 (((π‘Ž ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom π‘Ž = dom 𝑏 ∧ βˆ€π‘– ∈ dom π‘Žβˆ€π‘— ∈ dom π‘Ž((π‘Žβ€˜π‘–) βˆ’ (π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—)))) β†’ (π‘Ž ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)))
2625ssopab2i 5550 . . . . . . 7 {βŸ¨π‘Ž, π‘βŸ© ∣ ((π‘Ž ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom π‘Ž = dom 𝑏 ∧ βˆ€π‘– ∈ dom π‘Žβˆ€π‘— ∈ dom π‘Ž((π‘Žβ€˜π‘–) βˆ’ (π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—))))} βŠ† {βŸ¨π‘Ž, π‘βŸ© ∣ (π‘Ž ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ))}
2724, 26ssexi 5322 . . . . . 6 {βŸ¨π‘Ž, π‘βŸ© ∣ ((π‘Ž ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom π‘Ž = dom 𝑏 ∧ βˆ€π‘– ∈ dom π‘Žβˆ€π‘— ∈ dom π‘Ž((π‘Žβ€˜π‘–) βˆ’ (π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—))))} ∈ V
2819, 20, 27fvmpt 6998 . . . . 5 (𝐺 ∈ V β†’ (cgrGβ€˜πΊ) = {βŸ¨π‘Ž, π‘βŸ© ∣ ((π‘Ž ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom π‘Ž = dom 𝑏 ∧ βˆ€π‘– ∈ dom π‘Žβˆ€π‘— ∈ dom π‘Ž((π‘Žβ€˜π‘–) βˆ’ (π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—))))})
292, 28syl 17 . . . 4 (𝐺 ∈ 𝑉 β†’ (cgrGβ€˜πΊ) = {βŸ¨π‘Ž, π‘βŸ© ∣ ((π‘Ž ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom π‘Ž = dom 𝑏 ∧ βˆ€π‘– ∈ dom π‘Žβˆ€π‘— ∈ dom π‘Ž((π‘Žβ€˜π‘–) βˆ’ (π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—))))})
301, 29eqtrid 2784 . . 3 (𝐺 ∈ 𝑉 β†’ ∼ = {βŸ¨π‘Ž, π‘βŸ© ∣ ((π‘Ž ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom π‘Ž = dom 𝑏 ∧ βˆ€π‘– ∈ dom π‘Žβˆ€π‘— ∈ dom π‘Ž((π‘Žβ€˜π‘–) βˆ’ (π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—))))})
3130breqd 5159 . 2 (𝐺 ∈ 𝑉 β†’ (𝐴 ∼ 𝐡 ↔ 𝐴{βŸ¨π‘Ž, π‘βŸ© ∣ ((π‘Ž ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom π‘Ž = dom 𝑏 ∧ βˆ€π‘– ∈ dom π‘Žβˆ€π‘— ∈ dom π‘Ž((π‘Žβ€˜π‘–) βˆ’ (π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—))))}𝐡))
32 dmeq 5903 . . . . . 6 (π‘Ž = 𝐴 β†’ dom π‘Ž = dom 𝐴)
3332eqeq1d 2734 . . . . 5 (π‘Ž = 𝐴 β†’ (dom π‘Ž = dom 𝑏 ↔ dom 𝐴 = dom 𝑏))
3432adantr 481 . . . . . . 7 ((π‘Ž = 𝐴 ∧ 𝑖 ∈ dom π‘Ž) β†’ dom π‘Ž = dom 𝐴)
35 simpll 765 . . . . . . . . . 10 (((π‘Ž = 𝐴 ∧ 𝑖 ∈ dom π‘Ž) ∧ 𝑗 ∈ dom π‘Ž) β†’ π‘Ž = 𝐴)
3635fveq1d 6893 . . . . . . . . 9 (((π‘Ž = 𝐴 ∧ 𝑖 ∈ dom π‘Ž) ∧ 𝑗 ∈ dom π‘Ž) β†’ (π‘Žβ€˜π‘–) = (π΄β€˜π‘–))
3735fveq1d 6893 . . . . . . . . 9 (((π‘Ž = 𝐴 ∧ 𝑖 ∈ dom π‘Ž) ∧ 𝑗 ∈ dom π‘Ž) β†’ (π‘Žβ€˜π‘—) = (π΄β€˜π‘—))
3836, 37oveq12d 7429 . . . . . . . 8 (((π‘Ž = 𝐴 ∧ 𝑖 ∈ dom π‘Ž) ∧ 𝑗 ∈ dom π‘Ž) β†’ ((π‘Žβ€˜π‘–) βˆ’ (π‘Žβ€˜π‘—)) = ((π΄β€˜π‘–) βˆ’ (π΄β€˜π‘—)))
3938eqeq1d 2734 . . . . . . 7 (((π‘Ž = 𝐴 ∧ 𝑖 ∈ dom π‘Ž) ∧ 𝑗 ∈ dom π‘Ž) β†’ (((π‘Žβ€˜π‘–) βˆ’ (π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—)) ↔ ((π΄β€˜π‘–) βˆ’ (π΄β€˜π‘—)) = ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—))))
4034, 39raleqbidva 3327 . . . . . 6 ((π‘Ž = 𝐴 ∧ 𝑖 ∈ dom π‘Ž) β†’ (βˆ€π‘— ∈ dom π‘Ž((π‘Žβ€˜π‘–) βˆ’ (π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—)) ↔ βˆ€π‘— ∈ dom 𝐴((π΄β€˜π‘–) βˆ’ (π΄β€˜π‘—)) = ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—))))
4132, 40raleqbidva 3327 . . . . 5 (π‘Ž = 𝐴 β†’ (βˆ€π‘– ∈ dom π‘Žβˆ€π‘— ∈ dom π‘Ž((π‘Žβ€˜π‘–) βˆ’ (π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—)) ↔ βˆ€π‘– ∈ dom π΄βˆ€π‘— ∈ dom 𝐴((π΄β€˜π‘–) βˆ’ (π΄β€˜π‘—)) = ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—))))
4233, 41anbi12d 631 . . . 4 (π‘Ž = 𝐴 β†’ ((dom π‘Ž = dom 𝑏 ∧ βˆ€π‘– ∈ dom π‘Žβˆ€π‘— ∈ dom π‘Ž((π‘Žβ€˜π‘–) βˆ’ (π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—))) ↔ (dom 𝐴 = dom 𝑏 ∧ βˆ€π‘– ∈ dom π΄βˆ€π‘— ∈ dom 𝐴((π΄β€˜π‘–) βˆ’ (π΄β€˜π‘—)) = ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—)))))
43 dmeq 5903 . . . . . 6 (𝑏 = 𝐡 β†’ dom 𝑏 = dom 𝐡)
4443eqeq2d 2743 . . . . 5 (𝑏 = 𝐡 β†’ (dom 𝐴 = dom 𝑏 ↔ dom 𝐴 = dom 𝐡))
45 fveq1 6890 . . . . . . . 8 (𝑏 = 𝐡 β†’ (π‘β€˜π‘–) = (π΅β€˜π‘–))
46 fveq1 6890 . . . . . . . 8 (𝑏 = 𝐡 β†’ (π‘β€˜π‘—) = (π΅β€˜π‘—))
4745, 46oveq12d 7429 . . . . . . 7 (𝑏 = 𝐡 β†’ ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—)) = ((π΅β€˜π‘–) βˆ’ (π΅β€˜π‘—)))
4847eqeq2d 2743 . . . . . 6 (𝑏 = 𝐡 β†’ (((π΄β€˜π‘–) βˆ’ (π΄β€˜π‘—)) = ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—)) ↔ ((π΄β€˜π‘–) βˆ’ (π΄β€˜π‘—)) = ((π΅β€˜π‘–) βˆ’ (π΅β€˜π‘—))))
49482ralbidv 3218 . . . . 5 (𝑏 = 𝐡 β†’ (βˆ€π‘– ∈ dom π΄βˆ€π‘— ∈ dom 𝐴((π΄β€˜π‘–) βˆ’ (π΄β€˜π‘—)) = ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—)) ↔ βˆ€π‘– ∈ dom π΄βˆ€π‘— ∈ dom 𝐴((π΄β€˜π‘–) βˆ’ (π΄β€˜π‘—)) = ((π΅β€˜π‘–) βˆ’ (π΅β€˜π‘—))))
5044, 49anbi12d 631 . . . 4 (𝑏 = 𝐡 β†’ ((dom 𝐴 = dom 𝑏 ∧ βˆ€π‘– ∈ dom π΄βˆ€π‘— ∈ dom 𝐴((π΄β€˜π‘–) βˆ’ (π΄β€˜π‘—)) = ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—))) ↔ (dom 𝐴 = dom 𝐡 ∧ βˆ€π‘– ∈ dom π΄βˆ€π‘— ∈ dom 𝐴((π΄β€˜π‘–) βˆ’ (π΄β€˜π‘—)) = ((π΅β€˜π‘–) βˆ’ (π΅β€˜π‘—)))))
5142, 50sylan9bb 510 . . 3 ((π‘Ž = 𝐴 ∧ 𝑏 = 𝐡) β†’ ((dom π‘Ž = dom 𝑏 ∧ βˆ€π‘– ∈ dom π‘Žβˆ€π‘— ∈ dom π‘Ž((π‘Žβ€˜π‘–) βˆ’ (π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—))) ↔ (dom 𝐴 = dom 𝐡 ∧ βˆ€π‘– ∈ dom π΄βˆ€π‘— ∈ dom 𝐴((π΄β€˜π‘–) βˆ’ (π΄β€˜π‘—)) = ((π΅β€˜π‘–) βˆ’ (π΅β€˜π‘—)))))
52 eqid 2732 . . 3 {βŸ¨π‘Ž, π‘βŸ© ∣ ((π‘Ž ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom π‘Ž = dom 𝑏 ∧ βˆ€π‘– ∈ dom π‘Žβˆ€π‘— ∈ dom π‘Ž((π‘Žβ€˜π‘–) βˆ’ (π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—))))} = {βŸ¨π‘Ž, π‘βŸ© ∣ ((π‘Ž ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom π‘Ž = dom 𝑏 ∧ βˆ€π‘– ∈ dom π‘Žβˆ€π‘— ∈ dom π‘Ž((π‘Žβ€˜π‘–) βˆ’ (π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—))))}
5351, 52brab2a 5769 . 2 (𝐴{βŸ¨π‘Ž, π‘βŸ© ∣ ((π‘Ž ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom π‘Ž = dom 𝑏 ∧ βˆ€π‘– ∈ dom π‘Žβˆ€π‘— ∈ dom π‘Ž((π‘Žβ€˜π‘–) βˆ’ (π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—))))}𝐡 ↔ ((𝐴 ∈ (𝑃 ↑pm ℝ) ∧ 𝐡 ∈ (𝑃 ↑pm ℝ)) ∧ (dom 𝐴 = dom 𝐡 ∧ βˆ€π‘– ∈ dom π΄βˆ€π‘— ∈ dom 𝐴((π΄β€˜π‘–) βˆ’ (π΄β€˜π‘—)) = ((π΅β€˜π‘–) βˆ’ (π΅β€˜π‘—)))))
5431, 53bitrdi 286 1 (𝐺 ∈ 𝑉 β†’ (𝐴 ∼ 𝐡 ↔ ((𝐴 ∈ (𝑃 ↑pm ℝ) ∧ 𝐡 ∈ (𝑃 ↑pm ℝ)) ∧ (dom 𝐴 = dom 𝐡 ∧ βˆ€π‘– ∈ dom π΄βˆ€π‘— ∈ dom 𝐴((π΄β€˜π‘–) βˆ’ (π΄β€˜π‘—)) = ((π΅β€˜π‘–) βˆ’ (π΅β€˜π‘—))))))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 396   = wceq 1541   ∈ wcel 2106  βˆ€wral 3061  Vcvv 3474   class class class wbr 5148  {copab 5210   Γ— cxp 5674  dom cdm 5676  β€˜cfv 6543  (class class class)co 7411   ↑pm cpm 8823  β„cr 11111  Basecbs 17148  distcds 17210  cgrGccgrg 28016
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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7727
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-eu 2563  df-clab 2710  df-cleq 2724  df-clel 2810  df-nfc 2885  df-ne 2941  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-iota 6495  df-fun 6545  df-fv 6551  df-ov 7414  df-cgrg 28017
This theorem is referenced by:  iscgrgd  28019  ercgrg  28023
  Copyright terms: Public domain W3C validator