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

Theorem iscgrg 27763
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 3493 . . . . 5 (𝐺 ∈ 𝑉 β†’ 𝐺 ∈ V)
3 fveq2 6892 . . . . . . . . . . . 12 (𝑔 = 𝐺 β†’ (Baseβ€˜π‘”) = (Baseβ€˜πΊ))
4 iscgrg.p . . . . . . . . . . . 12 𝑃 = (Baseβ€˜πΊ)
53, 4eqtr4di 2791 . . . . . . . . . . 11 (𝑔 = 𝐺 β†’ (Baseβ€˜π‘”) = 𝑃)
65oveq1d 7424 . . . . . . . . . 10 (𝑔 = 𝐺 β†’ ((Baseβ€˜π‘”) ↑pm ℝ) = (𝑃 ↑pm ℝ))
76eleq2d 2820 . . . . . . . . 9 (𝑔 = 𝐺 β†’ (π‘Ž ∈ ((Baseβ€˜π‘”) ↑pm ℝ) ↔ π‘Ž ∈ (𝑃 ↑pm ℝ)))
86eleq2d 2820 . . . . . . . . 9 (𝑔 = 𝐺 β†’ (𝑏 ∈ ((Baseβ€˜π‘”) ↑pm ℝ) ↔ 𝑏 ∈ (𝑃 ↑pm ℝ)))
97, 8anbi12d 632 . . . . . . . 8 (𝑔 = 𝐺 β†’ ((π‘Ž ∈ ((Baseβ€˜π‘”) ↑pm ℝ) ∧ 𝑏 ∈ ((Baseβ€˜π‘”) ↑pm ℝ)) ↔ (π‘Ž ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ))))
10 fveq2 6892 . . . . . . . . . . . . 13 (𝑔 = 𝐺 β†’ (distβ€˜π‘”) = (distβ€˜πΊ))
11 iscgrg.m . . . . . . . . . . . . 13 βˆ’ = (distβ€˜πΊ)
1210, 11eqtr4di 2791 . . . . . . . . . . . 12 (𝑔 = 𝐺 β†’ (distβ€˜π‘”) = βˆ’ )
1312oveqd 7426 . . . . . . . . . . 11 (𝑔 = 𝐺 β†’ ((π‘Žβ€˜π‘–)(distβ€˜π‘”)(π‘Žβ€˜π‘—)) = ((π‘Žβ€˜π‘–) βˆ’ (π‘Žβ€˜π‘—)))
1412oveqd 7426 . . . . . . . . . . 11 (𝑔 = 𝐺 β†’ ((π‘β€˜π‘–)(distβ€˜π‘”)(π‘β€˜π‘—)) = ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—)))
1513, 14eqeq12d 2749 . . . . . . . . . 10 (𝑔 = 𝐺 β†’ (((π‘Žβ€˜π‘–)(distβ€˜π‘”)(π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–)(distβ€˜π‘”)(π‘β€˜π‘—)) ↔ ((π‘Žβ€˜π‘–) βˆ’ (π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—))))
16152ralbidv 3219 . . . . . . . . 9 (𝑔 = 𝐺 β†’ (βˆ€π‘– ∈ dom π‘Žβˆ€π‘— ∈ dom π‘Ž((π‘Žβ€˜π‘–)(distβ€˜π‘”)(π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–)(distβ€˜π‘”)(π‘β€˜π‘—)) ↔ βˆ€π‘– ∈ dom π‘Žβˆ€π‘— ∈ dom π‘Ž((π‘Žβ€˜π‘–) βˆ’ (π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—))))
1716anbi2d 630 . . . . . . . 8 (𝑔 = 𝐺 β†’ ((dom π‘Ž = dom 𝑏 ∧ βˆ€π‘– ∈ dom π‘Žβˆ€π‘— ∈ dom π‘Ž((π‘Žβ€˜π‘–)(distβ€˜π‘”)(π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–)(distβ€˜π‘”)(π‘β€˜π‘—))) ↔ (dom π‘Ž = dom 𝑏 ∧ βˆ€π‘– ∈ dom π‘Žβˆ€π‘— ∈ dom π‘Ž((π‘Žβ€˜π‘–) βˆ’ (π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—)))))
189, 17anbi12d 632 . . . . . . 7 (𝑔 = 𝐺 β†’ (((π‘Ž ∈ ((Baseβ€˜π‘”) ↑pm ℝ) ∧ 𝑏 ∈ ((Baseβ€˜π‘”) ↑pm ℝ)) ∧ (dom π‘Ž = dom 𝑏 ∧ βˆ€π‘– ∈ dom π‘Žβˆ€π‘— ∈ dom π‘Ž((π‘Žβ€˜π‘–)(distβ€˜π‘”)(π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–)(distβ€˜π‘”)(π‘β€˜π‘—)))) ↔ ((π‘Ž ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom π‘Ž = dom 𝑏 ∧ βˆ€π‘– ∈ dom π‘Žβˆ€π‘— ∈ dom π‘Ž((π‘Žβ€˜π‘–) βˆ’ (π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—))))))
1918opabbidv 5215 . . . . . 6 (𝑔 = 𝐺 β†’ {βŸ¨π‘Ž, π‘βŸ© ∣ ((π‘Ž ∈ ((Baseβ€˜π‘”) ↑pm ℝ) ∧ 𝑏 ∈ ((Baseβ€˜π‘”) ↑pm ℝ)) ∧ (dom π‘Ž = dom 𝑏 ∧ βˆ€π‘– ∈ dom π‘Žβˆ€π‘— ∈ dom π‘Ž((π‘Žβ€˜π‘–)(distβ€˜π‘”)(π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–)(distβ€˜π‘”)(π‘β€˜π‘—))))} = {βŸ¨π‘Ž, π‘βŸ© ∣ ((π‘Ž ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom π‘Ž = dom 𝑏 ∧ βˆ€π‘– ∈ dom π‘Žβˆ€π‘— ∈ dom π‘Ž((π‘Žβ€˜π‘–) βˆ’ (π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—))))})
20 df-cgrg 27762 . . . . . 6 cgrG = (𝑔 ∈ V ↦ {βŸ¨π‘Ž, π‘βŸ© ∣ ((π‘Ž ∈ ((Baseβ€˜π‘”) ↑pm ℝ) ∧ 𝑏 ∈ ((Baseβ€˜π‘”) ↑pm ℝ)) ∧ (dom π‘Ž = dom 𝑏 ∧ βˆ€π‘– ∈ dom π‘Žβˆ€π‘— ∈ dom π‘Ž((π‘Žβ€˜π‘–)(distβ€˜π‘”)(π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–)(distβ€˜π‘”)(π‘β€˜π‘—))))})
21 df-xp 5683 . . . . . . . 8 ((𝑃 ↑pm ℝ) Γ— (𝑃 ↑pm ℝ)) = {βŸ¨π‘Ž, π‘βŸ© ∣ (π‘Ž ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ))}
22 ovex 7442 . . . . . . . . 9 (𝑃 ↑pm ℝ) ∈ V
2322, 22xpex 7740 . . . . . . . 8 ((𝑃 ↑pm ℝ) Γ— (𝑃 ↑pm ℝ)) ∈ V
2421, 23eqeltrri 2831 . . . . . . 7 {βŸ¨π‘Ž, π‘βŸ© ∣ (π‘Ž ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ))} ∈ V
25 simpl 484 . . . . . . . 8 (((π‘Ž ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom π‘Ž = dom 𝑏 ∧ βˆ€π‘– ∈ dom π‘Žβˆ€π‘— ∈ dom π‘Ž((π‘Žβ€˜π‘–) βˆ’ (π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—)))) β†’ (π‘Ž ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)))
2625ssopab2i 5551 . . . . . . 7 {βŸ¨π‘Ž, π‘βŸ© ∣ ((π‘Ž ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom π‘Ž = dom 𝑏 ∧ βˆ€π‘– ∈ dom π‘Žβˆ€π‘— ∈ dom π‘Ž((π‘Žβ€˜π‘–) βˆ’ (π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—))))} βŠ† {βŸ¨π‘Ž, π‘βŸ© ∣ (π‘Ž ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ))}
2724, 26ssexi 5323 . . . . . 6 {βŸ¨π‘Ž, π‘βŸ© ∣ ((π‘Ž ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom π‘Ž = dom 𝑏 ∧ βˆ€π‘– ∈ dom π‘Žβˆ€π‘— ∈ dom π‘Ž((π‘Žβ€˜π‘–) βˆ’ (π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—))))} ∈ V
2819, 20, 27fvmpt 6999 . . . . 5 (𝐺 ∈ V β†’ (cgrGβ€˜πΊ) = {βŸ¨π‘Ž, π‘βŸ© ∣ ((π‘Ž ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom π‘Ž = dom 𝑏 ∧ βˆ€π‘– ∈ dom π‘Žβˆ€π‘— ∈ dom π‘Ž((π‘Žβ€˜π‘–) βˆ’ (π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—))))})
292, 28syl 17 . . . 4 (𝐺 ∈ 𝑉 β†’ (cgrGβ€˜πΊ) = {βŸ¨π‘Ž, π‘βŸ© ∣ ((π‘Ž ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom π‘Ž = dom 𝑏 ∧ βˆ€π‘– ∈ dom π‘Žβˆ€π‘— ∈ dom π‘Ž((π‘Žβ€˜π‘–) βˆ’ (π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—))))})
301, 29eqtrid 2785 . . 3 (𝐺 ∈ 𝑉 β†’ ∼ = {βŸ¨π‘Ž, π‘βŸ© ∣ ((π‘Ž ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom π‘Ž = dom 𝑏 ∧ βˆ€π‘– ∈ dom π‘Žβˆ€π‘— ∈ dom π‘Ž((π‘Žβ€˜π‘–) βˆ’ (π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—))))})
3130breqd 5160 . 2 (𝐺 ∈ 𝑉 β†’ (𝐴 ∼ 𝐡 ↔ 𝐴{βŸ¨π‘Ž, π‘βŸ© ∣ ((π‘Ž ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom π‘Ž = dom 𝑏 ∧ βˆ€π‘– ∈ dom π‘Žβˆ€π‘— ∈ dom π‘Ž((π‘Žβ€˜π‘–) βˆ’ (π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—))))}𝐡))
32 dmeq 5904 . . . . . 6 (π‘Ž = 𝐴 β†’ dom π‘Ž = dom 𝐴)
3332eqeq1d 2735 . . . . 5 (π‘Ž = 𝐴 β†’ (dom π‘Ž = dom 𝑏 ↔ dom 𝐴 = dom 𝑏))
3432adantr 482 . . . . . . 7 ((π‘Ž = 𝐴 ∧ 𝑖 ∈ dom π‘Ž) β†’ dom π‘Ž = dom 𝐴)
35 simpll 766 . . . . . . . . . 10 (((π‘Ž = 𝐴 ∧ 𝑖 ∈ dom π‘Ž) ∧ 𝑗 ∈ dom π‘Ž) β†’ π‘Ž = 𝐴)
3635fveq1d 6894 . . . . . . . . 9 (((π‘Ž = 𝐴 ∧ 𝑖 ∈ dom π‘Ž) ∧ 𝑗 ∈ dom π‘Ž) β†’ (π‘Žβ€˜π‘–) = (π΄β€˜π‘–))
3735fveq1d 6894 . . . . . . . . 9 (((π‘Ž = 𝐴 ∧ 𝑖 ∈ dom π‘Ž) ∧ 𝑗 ∈ dom π‘Ž) β†’ (π‘Žβ€˜π‘—) = (π΄β€˜π‘—))
3836, 37oveq12d 7427 . . . . . . . 8 (((π‘Ž = 𝐴 ∧ 𝑖 ∈ dom π‘Ž) ∧ 𝑗 ∈ dom π‘Ž) β†’ ((π‘Žβ€˜π‘–) βˆ’ (π‘Žβ€˜π‘—)) = ((π΄β€˜π‘–) βˆ’ (π΄β€˜π‘—)))
3938eqeq1d 2735 . . . . . . 7 (((π‘Ž = 𝐴 ∧ 𝑖 ∈ dom π‘Ž) ∧ 𝑗 ∈ dom π‘Ž) β†’ (((π‘Žβ€˜π‘–) βˆ’ (π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—)) ↔ ((π΄β€˜π‘–) βˆ’ (π΄β€˜π‘—)) = ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—))))
4034, 39raleqbidva 3328 . . . . . 6 ((π‘Ž = 𝐴 ∧ 𝑖 ∈ dom π‘Ž) β†’ (βˆ€π‘— ∈ dom π‘Ž((π‘Žβ€˜π‘–) βˆ’ (π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—)) ↔ βˆ€π‘— ∈ dom 𝐴((π΄β€˜π‘–) βˆ’ (π΄β€˜π‘—)) = ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—))))
4132, 40raleqbidva 3328 . . . . 5 (π‘Ž = 𝐴 β†’ (βˆ€π‘– ∈ dom π‘Žβˆ€π‘— ∈ dom π‘Ž((π‘Žβ€˜π‘–) βˆ’ (π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—)) ↔ βˆ€π‘– ∈ dom π΄βˆ€π‘— ∈ dom 𝐴((π΄β€˜π‘–) βˆ’ (π΄β€˜π‘—)) = ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—))))
4233, 41anbi12d 632 . . . 4 (π‘Ž = 𝐴 β†’ ((dom π‘Ž = dom 𝑏 ∧ βˆ€π‘– ∈ dom π‘Žβˆ€π‘— ∈ dom π‘Ž((π‘Žβ€˜π‘–) βˆ’ (π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—))) ↔ (dom 𝐴 = dom 𝑏 ∧ βˆ€π‘– ∈ dom π΄βˆ€π‘— ∈ dom 𝐴((π΄β€˜π‘–) βˆ’ (π΄β€˜π‘—)) = ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—)))))
43 dmeq 5904 . . . . . 6 (𝑏 = 𝐡 β†’ dom 𝑏 = dom 𝐡)
4443eqeq2d 2744 . . . . 5 (𝑏 = 𝐡 β†’ (dom 𝐴 = dom 𝑏 ↔ dom 𝐴 = dom 𝐡))
45 fveq1 6891 . . . . . . . 8 (𝑏 = 𝐡 β†’ (π‘β€˜π‘–) = (π΅β€˜π‘–))
46 fveq1 6891 . . . . . . . 8 (𝑏 = 𝐡 β†’ (π‘β€˜π‘—) = (π΅β€˜π‘—))
4745, 46oveq12d 7427 . . . . . . 7 (𝑏 = 𝐡 β†’ ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—)) = ((π΅β€˜π‘–) βˆ’ (π΅β€˜π‘—)))
4847eqeq2d 2744 . . . . . 6 (𝑏 = 𝐡 β†’ (((π΄β€˜π‘–) βˆ’ (π΄β€˜π‘—)) = ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—)) ↔ ((π΄β€˜π‘–) βˆ’ (π΄β€˜π‘—)) = ((π΅β€˜π‘–) βˆ’ (π΅β€˜π‘—))))
49482ralbidv 3219 . . . . 5 (𝑏 = 𝐡 β†’ (βˆ€π‘– ∈ dom π΄βˆ€π‘— ∈ dom 𝐴((π΄β€˜π‘–) βˆ’ (π΄β€˜π‘—)) = ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—)) ↔ βˆ€π‘– ∈ dom π΄βˆ€π‘— ∈ dom 𝐴((π΄β€˜π‘–) βˆ’ (π΄β€˜π‘—)) = ((π΅β€˜π‘–) βˆ’ (π΅β€˜π‘—))))
5044, 49anbi12d 632 . . . 4 (𝑏 = 𝐡 β†’ ((dom 𝐴 = dom 𝑏 ∧ βˆ€π‘– ∈ dom π΄βˆ€π‘— ∈ dom 𝐴((π΄β€˜π‘–) βˆ’ (π΄β€˜π‘—)) = ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—))) ↔ (dom 𝐴 = dom 𝐡 ∧ βˆ€π‘– ∈ dom π΄βˆ€π‘— ∈ dom 𝐴((π΄β€˜π‘–) βˆ’ (π΄β€˜π‘—)) = ((π΅β€˜π‘–) βˆ’ (π΅β€˜π‘—)))))
5142, 50sylan9bb 511 . . 3 ((π‘Ž = 𝐴 ∧ 𝑏 = 𝐡) β†’ ((dom π‘Ž = dom 𝑏 ∧ βˆ€π‘– ∈ dom π‘Žβˆ€π‘— ∈ dom π‘Ž((π‘Žβ€˜π‘–) βˆ’ (π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—))) ↔ (dom 𝐴 = dom 𝐡 ∧ βˆ€π‘– ∈ dom π΄βˆ€π‘— ∈ dom 𝐴((π΄β€˜π‘–) βˆ’ (π΄β€˜π‘—)) = ((π΅β€˜π‘–) βˆ’ (π΅β€˜π‘—)))))
52 eqid 2733 . . 3 {βŸ¨π‘Ž, π‘βŸ© ∣ ((π‘Ž ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom π‘Ž = dom 𝑏 ∧ βˆ€π‘– ∈ dom π‘Žβˆ€π‘— ∈ dom π‘Ž((π‘Žβ€˜π‘–) βˆ’ (π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—))))} = {βŸ¨π‘Ž, π‘βŸ© ∣ ((π‘Ž ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom π‘Ž = dom 𝑏 ∧ βˆ€π‘– ∈ dom π‘Žβˆ€π‘— ∈ dom π‘Ž((π‘Žβ€˜π‘–) βˆ’ (π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—))))}
5351, 52brab2a 5770 . 2 (𝐴{βŸ¨π‘Ž, π‘βŸ© ∣ ((π‘Ž ∈ (𝑃 ↑pm ℝ) ∧ 𝑏 ∈ (𝑃 ↑pm ℝ)) ∧ (dom π‘Ž = dom 𝑏 ∧ βˆ€π‘– ∈ dom π‘Žβˆ€π‘— ∈ dom π‘Ž((π‘Žβ€˜π‘–) βˆ’ (π‘Žβ€˜π‘—)) = ((π‘β€˜π‘–) βˆ’ (π‘β€˜π‘—))))}𝐡 ↔ ((𝐴 ∈ (𝑃 ↑pm ℝ) ∧ 𝐡 ∈ (𝑃 ↑pm ℝ)) ∧ (dom 𝐴 = dom 𝐡 ∧ βˆ€π‘– ∈ dom π΄βˆ€π‘— ∈ dom 𝐴((π΄β€˜π‘–) βˆ’ (π΄β€˜π‘—)) = ((π΅β€˜π‘–) βˆ’ (π΅β€˜π‘—)))))
5431, 53bitrdi 287 1 (𝐺 ∈ 𝑉 β†’ (𝐴 ∼ 𝐡 ↔ ((𝐴 ∈ (𝑃 ↑pm ℝ) ∧ 𝐡 ∈ (𝑃 ↑pm ℝ)) ∧ (dom 𝐴 = dom 𝐡 ∧ βˆ€π‘– ∈ dom π΄βˆ€π‘— ∈ dom 𝐴((π΄β€˜π‘–) βˆ’ (π΄β€˜π‘—)) = ((π΅β€˜π‘–) βˆ’ (π΅β€˜π‘—))))))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   = wceq 1542   ∈ wcel 2107  βˆ€wral 3062  Vcvv 3475   class class class wbr 5149  {copab 5211   Γ— cxp 5675  dom cdm 5677  β€˜cfv 6544  (class class class)co 7409   ↑pm cpm 8821  β„cr 11109  Basecbs 17144  distcds 17206  cgrGccgrg 27761
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-iota 6496  df-fun 6546  df-fv 6552  df-ov 7412  df-cgrg 27762
This theorem is referenced by:  iscgrgd  27764  ercgrg  27768
  Copyright terms: Public domain W3C validator