Step |
Hyp |
Ref |
Expression |
1 |
|
ercgrg.p |
⊢ 𝑃 = ( Base ‘ 𝐺 ) |
2 |
|
df-cgrg |
⊢ cgrG = ( 𝑔 ∈ V ↦ { 〈 𝑎 , 𝑏 〉 ∣ ( ( 𝑎 ∈ ( ( Base ‘ 𝑔 ) ↑pm ℝ ) ∧ 𝑏 ∈ ( ( Base ‘ 𝑔 ) ↑pm ℝ ) ) ∧ ( dom 𝑎 = dom 𝑏 ∧ ∀ 𝑖 ∈ dom 𝑎 ∀ 𝑗 ∈ dom 𝑎 ( ( 𝑎 ‘ 𝑖 ) ( dist ‘ 𝑔 ) ( 𝑎 ‘ 𝑗 ) ) = ( ( 𝑏 ‘ 𝑖 ) ( dist ‘ 𝑔 ) ( 𝑏 ‘ 𝑗 ) ) ) ) } ) |
3 |
2
|
relmptopab |
⊢ Rel ( cgrG ‘ 𝐺 ) |
4 |
3
|
a1i |
⊢ ( 𝐺 ∈ TarskiG → Rel ( cgrG ‘ 𝐺 ) ) |
5 |
|
eqid |
⊢ ( dist ‘ 𝐺 ) = ( dist ‘ 𝐺 ) |
6 |
|
eqid |
⊢ ( cgrG ‘ 𝐺 ) = ( cgrG ‘ 𝐺 ) |
7 |
1 5 6
|
iscgrg |
⊢ ( 𝐺 ∈ TarskiG → ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ↔ ( ( 𝑥 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑦 ∈ ( 𝑃 ↑pm ℝ ) ) ∧ ( dom 𝑥 = dom 𝑦 ∧ ∀ 𝑖 ∈ dom 𝑥 ∀ 𝑗 ∈ dom 𝑥 ( ( 𝑥 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥 ‘ 𝑗 ) ) = ( ( 𝑦 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑦 ‘ 𝑗 ) ) ) ) ) ) |
8 |
7
|
biimpa |
⊢ ( ( 𝐺 ∈ TarskiG ∧ 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ) → ( ( 𝑥 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑦 ∈ ( 𝑃 ↑pm ℝ ) ) ∧ ( dom 𝑥 = dom 𝑦 ∧ ∀ 𝑖 ∈ dom 𝑥 ∀ 𝑗 ∈ dom 𝑥 ( ( 𝑥 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥 ‘ 𝑗 ) ) = ( ( 𝑦 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑦 ‘ 𝑗 ) ) ) ) ) |
9 |
8
|
simpld |
⊢ ( ( 𝐺 ∈ TarskiG ∧ 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ) → ( 𝑥 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑦 ∈ ( 𝑃 ↑pm ℝ ) ) ) |
10 |
9
|
ancomd |
⊢ ( ( 𝐺 ∈ TarskiG ∧ 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ) → ( 𝑦 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑥 ∈ ( 𝑃 ↑pm ℝ ) ) ) |
11 |
8
|
simprd |
⊢ ( ( 𝐺 ∈ TarskiG ∧ 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ) → ( dom 𝑥 = dom 𝑦 ∧ ∀ 𝑖 ∈ dom 𝑥 ∀ 𝑗 ∈ dom 𝑥 ( ( 𝑥 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥 ‘ 𝑗 ) ) = ( ( 𝑦 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑦 ‘ 𝑗 ) ) ) ) |
12 |
11
|
simpld |
⊢ ( ( 𝐺 ∈ TarskiG ∧ 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ) → dom 𝑥 = dom 𝑦 ) |
13 |
12
|
eqcomd |
⊢ ( ( 𝐺 ∈ TarskiG ∧ 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ) → dom 𝑦 = dom 𝑥 ) |
14 |
|
simpl |
⊢ ( ( ( 𝐺 ∈ TarskiG ∧ 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ) ∧ ( 𝑖 ∈ dom 𝑦 ∧ 𝑗 ∈ dom 𝑦 ) ) → ( 𝐺 ∈ TarskiG ∧ 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ) ) |
15 |
|
simprl |
⊢ ( ( ( 𝐺 ∈ TarskiG ∧ 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ) ∧ ( 𝑖 ∈ dom 𝑦 ∧ 𝑗 ∈ dom 𝑦 ) ) → 𝑖 ∈ dom 𝑦 ) |
16 |
12
|
adantr |
⊢ ( ( ( 𝐺 ∈ TarskiG ∧ 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ) ∧ ( 𝑖 ∈ dom 𝑦 ∧ 𝑗 ∈ dom 𝑦 ) ) → dom 𝑥 = dom 𝑦 ) |
17 |
15 16
|
eleqtrrd |
⊢ ( ( ( 𝐺 ∈ TarskiG ∧ 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ) ∧ ( 𝑖 ∈ dom 𝑦 ∧ 𝑗 ∈ dom 𝑦 ) ) → 𝑖 ∈ dom 𝑥 ) |
18 |
|
simprr |
⊢ ( ( ( 𝐺 ∈ TarskiG ∧ 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ) ∧ ( 𝑖 ∈ dom 𝑦 ∧ 𝑗 ∈ dom 𝑦 ) ) → 𝑗 ∈ dom 𝑦 ) |
19 |
18 16
|
eleqtrrd |
⊢ ( ( ( 𝐺 ∈ TarskiG ∧ 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ) ∧ ( 𝑖 ∈ dom 𝑦 ∧ 𝑗 ∈ dom 𝑦 ) ) → 𝑗 ∈ dom 𝑥 ) |
20 |
11
|
simprd |
⊢ ( ( 𝐺 ∈ TarskiG ∧ 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ) → ∀ 𝑖 ∈ dom 𝑥 ∀ 𝑗 ∈ dom 𝑥 ( ( 𝑥 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥 ‘ 𝑗 ) ) = ( ( 𝑦 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑦 ‘ 𝑗 ) ) ) |
21 |
20
|
r19.21bi |
⊢ ( ( ( 𝐺 ∈ TarskiG ∧ 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ) ∧ 𝑖 ∈ dom 𝑥 ) → ∀ 𝑗 ∈ dom 𝑥 ( ( 𝑥 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥 ‘ 𝑗 ) ) = ( ( 𝑦 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑦 ‘ 𝑗 ) ) ) |
22 |
21
|
r19.21bi |
⊢ ( ( ( ( 𝐺 ∈ TarskiG ∧ 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ) ∧ 𝑖 ∈ dom 𝑥 ) ∧ 𝑗 ∈ dom 𝑥 ) → ( ( 𝑥 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥 ‘ 𝑗 ) ) = ( ( 𝑦 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑦 ‘ 𝑗 ) ) ) |
23 |
14 17 19 22
|
syl21anc |
⊢ ( ( ( 𝐺 ∈ TarskiG ∧ 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ) ∧ ( 𝑖 ∈ dom 𝑦 ∧ 𝑗 ∈ dom 𝑦 ) ) → ( ( 𝑥 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥 ‘ 𝑗 ) ) = ( ( 𝑦 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑦 ‘ 𝑗 ) ) ) |
24 |
23
|
eqcomd |
⊢ ( ( ( 𝐺 ∈ TarskiG ∧ 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ) ∧ ( 𝑖 ∈ dom 𝑦 ∧ 𝑗 ∈ dom 𝑦 ) ) → ( ( 𝑦 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑦 ‘ 𝑗 ) ) = ( ( 𝑥 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥 ‘ 𝑗 ) ) ) |
25 |
24
|
ralrimivva |
⊢ ( ( 𝐺 ∈ TarskiG ∧ 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ) → ∀ 𝑖 ∈ dom 𝑦 ∀ 𝑗 ∈ dom 𝑦 ( ( 𝑦 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑦 ‘ 𝑗 ) ) = ( ( 𝑥 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥 ‘ 𝑗 ) ) ) |
26 |
13 25
|
jca |
⊢ ( ( 𝐺 ∈ TarskiG ∧ 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ) → ( dom 𝑦 = dom 𝑥 ∧ ∀ 𝑖 ∈ dom 𝑦 ∀ 𝑗 ∈ dom 𝑦 ( ( 𝑦 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑦 ‘ 𝑗 ) ) = ( ( 𝑥 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥 ‘ 𝑗 ) ) ) ) |
27 |
1 5 6
|
iscgrg |
⊢ ( 𝐺 ∈ TarskiG → ( 𝑦 ( cgrG ‘ 𝐺 ) 𝑥 ↔ ( ( 𝑦 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑥 ∈ ( 𝑃 ↑pm ℝ ) ) ∧ ( dom 𝑦 = dom 𝑥 ∧ ∀ 𝑖 ∈ dom 𝑦 ∀ 𝑗 ∈ dom 𝑦 ( ( 𝑦 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑦 ‘ 𝑗 ) ) = ( ( 𝑥 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥 ‘ 𝑗 ) ) ) ) ) ) |
28 |
27
|
adantr |
⊢ ( ( 𝐺 ∈ TarskiG ∧ 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ) → ( 𝑦 ( cgrG ‘ 𝐺 ) 𝑥 ↔ ( ( 𝑦 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑥 ∈ ( 𝑃 ↑pm ℝ ) ) ∧ ( dom 𝑦 = dom 𝑥 ∧ ∀ 𝑖 ∈ dom 𝑦 ∀ 𝑗 ∈ dom 𝑦 ( ( 𝑦 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑦 ‘ 𝑗 ) ) = ( ( 𝑥 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥 ‘ 𝑗 ) ) ) ) ) ) |
29 |
10 26 28
|
mpbir2and |
⊢ ( ( 𝐺 ∈ TarskiG ∧ 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ) → 𝑦 ( cgrG ‘ 𝐺 ) 𝑥 ) |
30 |
9
|
simpld |
⊢ ( ( 𝐺 ∈ TarskiG ∧ 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ) → 𝑥 ∈ ( 𝑃 ↑pm ℝ ) ) |
31 |
30
|
adantrr |
⊢ ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ∧ 𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) → 𝑥 ∈ ( 𝑃 ↑pm ℝ ) ) |
32 |
1 5 6
|
iscgrg |
⊢ ( 𝐺 ∈ TarskiG → ( 𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ↔ ( ( 𝑦 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑧 ∈ ( 𝑃 ↑pm ℝ ) ) ∧ ( dom 𝑦 = dom 𝑧 ∧ ∀ 𝑖 ∈ dom 𝑦 ∀ 𝑗 ∈ dom 𝑦 ( ( 𝑦 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑦 ‘ 𝑗 ) ) = ( ( 𝑧 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑧 ‘ 𝑗 ) ) ) ) ) ) |
33 |
32
|
biimpa |
⊢ ( ( 𝐺 ∈ TarskiG ∧ 𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) → ( ( 𝑦 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑧 ∈ ( 𝑃 ↑pm ℝ ) ) ∧ ( dom 𝑦 = dom 𝑧 ∧ ∀ 𝑖 ∈ dom 𝑦 ∀ 𝑗 ∈ dom 𝑦 ( ( 𝑦 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑦 ‘ 𝑗 ) ) = ( ( 𝑧 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑧 ‘ 𝑗 ) ) ) ) ) |
34 |
33
|
adantrl |
⊢ ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ∧ 𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) → ( ( 𝑦 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑧 ∈ ( 𝑃 ↑pm ℝ ) ) ∧ ( dom 𝑦 = dom 𝑧 ∧ ∀ 𝑖 ∈ dom 𝑦 ∀ 𝑗 ∈ dom 𝑦 ( ( 𝑦 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑦 ‘ 𝑗 ) ) = ( ( 𝑧 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑧 ‘ 𝑗 ) ) ) ) ) |
35 |
34
|
simpld |
⊢ ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ∧ 𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) → ( 𝑦 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑧 ∈ ( 𝑃 ↑pm ℝ ) ) ) |
36 |
35
|
simprd |
⊢ ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ∧ 𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) → 𝑧 ∈ ( 𝑃 ↑pm ℝ ) ) |
37 |
31 36
|
jca |
⊢ ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ∧ 𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) → ( 𝑥 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑧 ∈ ( 𝑃 ↑pm ℝ ) ) ) |
38 |
8
|
adantrr |
⊢ ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ∧ 𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) → ( ( 𝑥 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑦 ∈ ( 𝑃 ↑pm ℝ ) ) ∧ ( dom 𝑥 = dom 𝑦 ∧ ∀ 𝑖 ∈ dom 𝑥 ∀ 𝑗 ∈ dom 𝑥 ( ( 𝑥 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥 ‘ 𝑗 ) ) = ( ( 𝑦 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑦 ‘ 𝑗 ) ) ) ) ) |
39 |
38
|
simprd |
⊢ ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ∧ 𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) → ( dom 𝑥 = dom 𝑦 ∧ ∀ 𝑖 ∈ dom 𝑥 ∀ 𝑗 ∈ dom 𝑥 ( ( 𝑥 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥 ‘ 𝑗 ) ) = ( ( 𝑦 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑦 ‘ 𝑗 ) ) ) ) |
40 |
39
|
simpld |
⊢ ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ∧ 𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) → dom 𝑥 = dom 𝑦 ) |
41 |
34
|
simprd |
⊢ ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ∧ 𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) → ( dom 𝑦 = dom 𝑧 ∧ ∀ 𝑖 ∈ dom 𝑦 ∀ 𝑗 ∈ dom 𝑦 ( ( 𝑦 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑦 ‘ 𝑗 ) ) = ( ( 𝑧 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑧 ‘ 𝑗 ) ) ) ) |
42 |
41
|
simpld |
⊢ ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ∧ 𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) → dom 𝑦 = dom 𝑧 ) |
43 |
40 42
|
eqtrd |
⊢ ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ∧ 𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) → dom 𝑥 = dom 𝑧 ) |
44 |
39
|
simprd |
⊢ ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ∧ 𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) → ∀ 𝑖 ∈ dom 𝑥 ∀ 𝑗 ∈ dom 𝑥 ( ( 𝑥 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥 ‘ 𝑗 ) ) = ( ( 𝑦 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑦 ‘ 𝑗 ) ) ) |
45 |
44
|
r19.21bi |
⊢ ( ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ∧ 𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) ∧ 𝑖 ∈ dom 𝑥 ) → ∀ 𝑗 ∈ dom 𝑥 ( ( 𝑥 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥 ‘ 𝑗 ) ) = ( ( 𝑦 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑦 ‘ 𝑗 ) ) ) |
46 |
45
|
r19.21bi |
⊢ ( ( ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ∧ 𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) ∧ 𝑖 ∈ dom 𝑥 ) ∧ 𝑗 ∈ dom 𝑥 ) → ( ( 𝑥 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥 ‘ 𝑗 ) ) = ( ( 𝑦 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑦 ‘ 𝑗 ) ) ) |
47 |
46
|
anasss |
⊢ ( ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ∧ 𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) ∧ ( 𝑖 ∈ dom 𝑥 ∧ 𝑗 ∈ dom 𝑥 ) ) → ( ( 𝑥 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥 ‘ 𝑗 ) ) = ( ( 𝑦 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑦 ‘ 𝑗 ) ) ) |
48 |
|
simpl |
⊢ ( ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ∧ 𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) ∧ ( 𝑖 ∈ dom 𝑥 ∧ 𝑗 ∈ dom 𝑥 ) ) → ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ∧ 𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) ) |
49 |
|
simprl |
⊢ ( ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ∧ 𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) ∧ ( 𝑖 ∈ dom 𝑥 ∧ 𝑗 ∈ dom 𝑥 ) ) → 𝑖 ∈ dom 𝑥 ) |
50 |
40
|
adantr |
⊢ ( ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ∧ 𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) ∧ ( 𝑖 ∈ dom 𝑥 ∧ 𝑗 ∈ dom 𝑥 ) ) → dom 𝑥 = dom 𝑦 ) |
51 |
49 50
|
eleqtrd |
⊢ ( ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ∧ 𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) ∧ ( 𝑖 ∈ dom 𝑥 ∧ 𝑗 ∈ dom 𝑥 ) ) → 𝑖 ∈ dom 𝑦 ) |
52 |
|
simprr |
⊢ ( ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ∧ 𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) ∧ ( 𝑖 ∈ dom 𝑥 ∧ 𝑗 ∈ dom 𝑥 ) ) → 𝑗 ∈ dom 𝑥 ) |
53 |
52 50
|
eleqtrd |
⊢ ( ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ∧ 𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) ∧ ( 𝑖 ∈ dom 𝑥 ∧ 𝑗 ∈ dom 𝑥 ) ) → 𝑗 ∈ dom 𝑦 ) |
54 |
41
|
simprd |
⊢ ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ∧ 𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) → ∀ 𝑖 ∈ dom 𝑦 ∀ 𝑗 ∈ dom 𝑦 ( ( 𝑦 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑦 ‘ 𝑗 ) ) = ( ( 𝑧 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑧 ‘ 𝑗 ) ) ) |
55 |
54
|
r19.21bi |
⊢ ( ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ∧ 𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) ∧ 𝑖 ∈ dom 𝑦 ) → ∀ 𝑗 ∈ dom 𝑦 ( ( 𝑦 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑦 ‘ 𝑗 ) ) = ( ( 𝑧 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑧 ‘ 𝑗 ) ) ) |
56 |
55
|
r19.21bi |
⊢ ( ( ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ∧ 𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) ∧ 𝑖 ∈ dom 𝑦 ) ∧ 𝑗 ∈ dom 𝑦 ) → ( ( 𝑦 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑦 ‘ 𝑗 ) ) = ( ( 𝑧 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑧 ‘ 𝑗 ) ) ) |
57 |
48 51 53 56
|
syl21anc |
⊢ ( ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ∧ 𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) ∧ ( 𝑖 ∈ dom 𝑥 ∧ 𝑗 ∈ dom 𝑥 ) ) → ( ( 𝑦 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑦 ‘ 𝑗 ) ) = ( ( 𝑧 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑧 ‘ 𝑗 ) ) ) |
58 |
47 57
|
eqtrd |
⊢ ( ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ∧ 𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) ∧ ( 𝑖 ∈ dom 𝑥 ∧ 𝑗 ∈ dom 𝑥 ) ) → ( ( 𝑥 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥 ‘ 𝑗 ) ) = ( ( 𝑧 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑧 ‘ 𝑗 ) ) ) |
59 |
58
|
ralrimivva |
⊢ ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ∧ 𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) → ∀ 𝑖 ∈ dom 𝑥 ∀ 𝑗 ∈ dom 𝑥 ( ( 𝑥 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥 ‘ 𝑗 ) ) = ( ( 𝑧 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑧 ‘ 𝑗 ) ) ) |
60 |
43 59
|
jca |
⊢ ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ∧ 𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) → ( dom 𝑥 = dom 𝑧 ∧ ∀ 𝑖 ∈ dom 𝑥 ∀ 𝑗 ∈ dom 𝑥 ( ( 𝑥 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥 ‘ 𝑗 ) ) = ( ( 𝑧 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑧 ‘ 𝑗 ) ) ) ) |
61 |
1 5 6
|
iscgrg |
⊢ ( 𝐺 ∈ TarskiG → ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑧 ↔ ( ( 𝑥 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑧 ∈ ( 𝑃 ↑pm ℝ ) ) ∧ ( dom 𝑥 = dom 𝑧 ∧ ∀ 𝑖 ∈ dom 𝑥 ∀ 𝑗 ∈ dom 𝑥 ( ( 𝑥 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥 ‘ 𝑗 ) ) = ( ( 𝑧 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑧 ‘ 𝑗 ) ) ) ) ) ) |
62 |
61
|
adantr |
⊢ ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ∧ 𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) → ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑧 ↔ ( ( 𝑥 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑧 ∈ ( 𝑃 ↑pm ℝ ) ) ∧ ( dom 𝑥 = dom 𝑧 ∧ ∀ 𝑖 ∈ dom 𝑥 ∀ 𝑗 ∈ dom 𝑥 ( ( 𝑥 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥 ‘ 𝑗 ) ) = ( ( 𝑧 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑧 ‘ 𝑗 ) ) ) ) ) ) |
63 |
37 60 62
|
mpbir2and |
⊢ ( ( 𝐺 ∈ TarskiG ∧ ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑦 ∧ 𝑦 ( cgrG ‘ 𝐺 ) 𝑧 ) ) → 𝑥 ( cgrG ‘ 𝐺 ) 𝑧 ) |
64 |
|
pm4.24 |
⊢ ( 𝑥 ∈ ( 𝑃 ↑pm ℝ ) ↔ ( 𝑥 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑥 ∈ ( 𝑃 ↑pm ℝ ) ) ) |
65 |
|
eqid |
⊢ dom 𝑥 = dom 𝑥 |
66 |
|
eqidd |
⊢ ( ( 𝑖 ∈ dom 𝑥 ∧ 𝑗 ∈ dom 𝑥 ) → ( ( 𝑥 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥 ‘ 𝑗 ) ) = ( ( 𝑥 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥 ‘ 𝑗 ) ) ) |
67 |
66
|
rgen2 |
⊢ ∀ 𝑖 ∈ dom 𝑥 ∀ 𝑗 ∈ dom 𝑥 ( ( 𝑥 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥 ‘ 𝑗 ) ) = ( ( 𝑥 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥 ‘ 𝑗 ) ) |
68 |
65 67
|
pm3.2i |
⊢ ( dom 𝑥 = dom 𝑥 ∧ ∀ 𝑖 ∈ dom 𝑥 ∀ 𝑗 ∈ dom 𝑥 ( ( 𝑥 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥 ‘ 𝑗 ) ) = ( ( 𝑥 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥 ‘ 𝑗 ) ) ) |
69 |
68
|
biantru |
⊢ ( ( 𝑥 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑥 ∈ ( 𝑃 ↑pm ℝ ) ) ↔ ( ( 𝑥 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑥 ∈ ( 𝑃 ↑pm ℝ ) ) ∧ ( dom 𝑥 = dom 𝑥 ∧ ∀ 𝑖 ∈ dom 𝑥 ∀ 𝑗 ∈ dom 𝑥 ( ( 𝑥 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥 ‘ 𝑗 ) ) = ( ( 𝑥 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥 ‘ 𝑗 ) ) ) ) ) |
70 |
64 69
|
bitri |
⊢ ( 𝑥 ∈ ( 𝑃 ↑pm ℝ ) ↔ ( ( 𝑥 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑥 ∈ ( 𝑃 ↑pm ℝ ) ) ∧ ( dom 𝑥 = dom 𝑥 ∧ ∀ 𝑖 ∈ dom 𝑥 ∀ 𝑗 ∈ dom 𝑥 ( ( 𝑥 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥 ‘ 𝑗 ) ) = ( ( 𝑥 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥 ‘ 𝑗 ) ) ) ) ) |
71 |
1 5 6
|
iscgrg |
⊢ ( 𝐺 ∈ TarskiG → ( 𝑥 ( cgrG ‘ 𝐺 ) 𝑥 ↔ ( ( 𝑥 ∈ ( 𝑃 ↑pm ℝ ) ∧ 𝑥 ∈ ( 𝑃 ↑pm ℝ ) ) ∧ ( dom 𝑥 = dom 𝑥 ∧ ∀ 𝑖 ∈ dom 𝑥 ∀ 𝑗 ∈ dom 𝑥 ( ( 𝑥 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥 ‘ 𝑗 ) ) = ( ( 𝑥 ‘ 𝑖 ) ( dist ‘ 𝐺 ) ( 𝑥 ‘ 𝑗 ) ) ) ) ) ) |
72 |
70 71
|
bitr4id |
⊢ ( 𝐺 ∈ TarskiG → ( 𝑥 ∈ ( 𝑃 ↑pm ℝ ) ↔ 𝑥 ( cgrG ‘ 𝐺 ) 𝑥 ) ) |
73 |
4 29 63 72
|
iserd |
⊢ ( 𝐺 ∈ TarskiG → ( cgrG ‘ 𝐺 ) Er ( 𝑃 ↑pm ℝ ) ) |