Metamath Proof Explorer

Theorem tgjustc2

Description: A justification for using distance equality instead of the textbook relation on pairs of points for congruence. (Contributed by Thierry Arnoux, 29-Jan-2023)

Ref Expression
Hypotheses tgjustc2.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
tgjustc2.d ⊢ 𝑅 Er ( 𝑃 × 𝑃 )
Assertion tgjustc2 ∃ 𝑑 ( 𝑑 Fn ( 𝑃 × 𝑃 ) ∧ ∀ 𝑤 ∈ 𝑃 ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ( ⟨ 𝑤 , 𝑥 ⟩ 𝑅 ⟨ 𝑦 , 𝑧 ⟩ ↔ ( 𝑤 𝑑 𝑥 ) = ( 𝑦 𝑑 𝑧 ) ) )

Proof

Step Hyp Ref Expression
1 tgjustc2.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 tgjustc2.d ⊢ 𝑅 Er ( 𝑃 × 𝑃 )
3 1 fvexi ⊢ 𝑃 ∈ V
4 3 3 xpex ⊢ ( 𝑃 × 𝑃 ) ∈ V
5 tgjustr ⊢ ( ( ( 𝑃 × 𝑃 ) ∈ V ∧ 𝑅 Er ( 𝑃 × 𝑃 ) ) → ∃ 𝑑 ( 𝑑 Fn ( 𝑃 × 𝑃 ) ∧ ∀ 𝑢 ∈ ( 𝑃 × 𝑃 ) ∀ 𝑣 ∈ ( 𝑃 × 𝑃 ) ( 𝑢 𝑅 𝑣 ↔ ( 𝑑 ‘ 𝑢 ) = ( 𝑑 ‘ 𝑣 ) ) ) )
6 4 2 5 mp2an ⊢ ∃ 𝑑 ( 𝑑 Fn ( 𝑃 × 𝑃 ) ∧ ∀ 𝑢 ∈ ( 𝑃 × 𝑃 ) ∀ 𝑣 ∈ ( 𝑃 × 𝑃 ) ( 𝑢 𝑅 𝑣 ↔ ( 𝑑 ‘ 𝑢 ) = ( 𝑑 ‘ 𝑣 ) ) )
7 simplrl ⊢ ( ( ( ∀ 𝑢 ∈ ( 𝑃 × 𝑃 ) ∀ 𝑣 ∈ ( 𝑃 × 𝑃 ) ( 𝑢 𝑅 𝑣 ↔ ( 𝑑 ‘ 𝑢 ) = ( 𝑑 ‘ 𝑣 ) ) ∧ ( 𝑤 ∈ 𝑃 ∧ 𝑥 ∈ 𝑃 ) ) ∧ ( 𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃 ) ) → 𝑤 ∈ 𝑃 )
8 simplrr ⊢ ( ( ( ∀ 𝑢 ∈ ( 𝑃 × 𝑃 ) ∀ 𝑣 ∈ ( 𝑃 × 𝑃 ) ( 𝑢 𝑅 𝑣 ↔ ( 𝑑 ‘ 𝑢 ) = ( 𝑑 ‘ 𝑣 ) ) ∧ ( 𝑤 ∈ 𝑃 ∧ 𝑥 ∈ 𝑃 ) ) ∧ ( 𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃 ) ) → 𝑥 ∈ 𝑃 )
9 7 8 opelxpd ⊢ ( ( ( ∀ 𝑢 ∈ ( 𝑃 × 𝑃 ) ∀ 𝑣 ∈ ( 𝑃 × 𝑃 ) ( 𝑢 𝑅 𝑣 ↔ ( 𝑑 ‘ 𝑢 ) = ( 𝑑 ‘ 𝑣 ) ) ∧ ( 𝑤 ∈ 𝑃 ∧ 𝑥 ∈ 𝑃 ) ) ∧ ( 𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃 ) ) → ⟨ 𝑤 , 𝑥 ⟩ ∈ ( 𝑃 × 𝑃 ) )
10 simprl ⊢ ( ( ( ∀ 𝑢 ∈ ( 𝑃 × 𝑃 ) ∀ 𝑣 ∈ ( 𝑃 × 𝑃 ) ( 𝑢 𝑅 𝑣 ↔ ( 𝑑 ‘ 𝑢 ) = ( 𝑑 ‘ 𝑣 ) ) ∧ ( 𝑤 ∈ 𝑃 ∧ 𝑥 ∈ 𝑃 ) ) ∧ ( 𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃 ) ) → 𝑦 ∈ 𝑃 )
11 simprr ⊢ ( ( ( ∀ 𝑢 ∈ ( 𝑃 × 𝑃 ) ∀ 𝑣 ∈ ( 𝑃 × 𝑃 ) ( 𝑢 𝑅 𝑣 ↔ ( 𝑑 ‘ 𝑢 ) = ( 𝑑 ‘ 𝑣 ) ) ∧ ( 𝑤 ∈ 𝑃 ∧ 𝑥 ∈ 𝑃 ) ) ∧ ( 𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃 ) ) → 𝑧 ∈ 𝑃 )
12 10 11 opelxpd ⊢ ( ( ( ∀ 𝑢 ∈ ( 𝑃 × 𝑃 ) ∀ 𝑣 ∈ ( 𝑃 × 𝑃 ) ( 𝑢 𝑅 𝑣 ↔ ( 𝑑 ‘ 𝑢 ) = ( 𝑑 ‘ 𝑣 ) ) ∧ ( 𝑤 ∈ 𝑃 ∧ 𝑥 ∈ 𝑃 ) ) ∧ ( 𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃 ) ) → ⟨ 𝑦 , 𝑧 ⟩ ∈ ( 𝑃 × 𝑃 ) )
13 simpll ⊢ ( ( ( ∀ 𝑢 ∈ ( 𝑃 × 𝑃 ) ∀ 𝑣 ∈ ( 𝑃 × 𝑃 ) ( 𝑢 𝑅 𝑣 ↔ ( 𝑑 ‘ 𝑢 ) = ( 𝑑 ‘ 𝑣 ) ) ∧ ( 𝑤 ∈ 𝑃 ∧ 𝑥 ∈ 𝑃 ) ) ∧ ( 𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃 ) ) → ∀ 𝑢 ∈ ( 𝑃 × 𝑃 ) ∀ 𝑣 ∈ ( 𝑃 × 𝑃 ) ( 𝑢 𝑅 𝑣 ↔ ( 𝑑 ‘ 𝑢 ) = ( 𝑑 ‘ 𝑣 ) ) )
14 breq1 ⊢ ( 𝑢 = ⟨ 𝑤 , 𝑥 ⟩ → ( 𝑢 𝑅 𝑣 ↔ ⟨ 𝑤 , 𝑥 ⟩ 𝑅 𝑣 ) )
15 fveq2 ⊢ ( 𝑢 = ⟨ 𝑤 , 𝑥 ⟩ → ( 𝑑 ‘ 𝑢 ) = ( 𝑑 ‘ ⟨ 𝑤 , 𝑥 ⟩ ) )
16 df-ov ⊢ ( 𝑤 𝑑 𝑥 ) = ( 𝑑 ‘ ⟨ 𝑤 , 𝑥 ⟩ )
17 15 16 eqtr4di ⊢ ( 𝑢 = ⟨ 𝑤 , 𝑥 ⟩ → ( 𝑑 ‘ 𝑢 ) = ( 𝑤 𝑑 𝑥 ) )
18 17 eqeq1d ⊢ ( 𝑢 = ⟨ 𝑤 , 𝑥 ⟩ → ( ( 𝑑 ‘ 𝑢 ) = ( 𝑑 ‘ 𝑣 ) ↔ ( 𝑤 𝑑 𝑥 ) = ( 𝑑 ‘ 𝑣 ) ) )
19 14 18 bibi12d ⊢ ( 𝑢 = ⟨ 𝑤 , 𝑥 ⟩ → ( ( 𝑢 𝑅 𝑣 ↔ ( 𝑑 ‘ 𝑢 ) = ( 𝑑 ‘ 𝑣 ) ) ↔ ( ⟨ 𝑤 , 𝑥 ⟩ 𝑅 𝑣 ↔ ( 𝑤 𝑑 𝑥 ) = ( 𝑑 ‘ 𝑣 ) ) ) )
20 breq2 ⊢ ( 𝑣 = ⟨ 𝑦 , 𝑧 ⟩ → ( ⟨ 𝑤 , 𝑥 ⟩ 𝑅 𝑣 ↔ ⟨ 𝑤 , 𝑥 ⟩ 𝑅 ⟨ 𝑦 , 𝑧 ⟩ ) )
21 fveq2 ⊢ ( 𝑣 = ⟨ 𝑦 , 𝑧 ⟩ → ( 𝑑 ‘ 𝑣 ) = ( 𝑑 ‘ ⟨ 𝑦 , 𝑧 ⟩ ) )
22 df-ov ⊢ ( 𝑦 𝑑 𝑧 ) = ( 𝑑 ‘ ⟨ 𝑦 , 𝑧 ⟩ )
23 21 22 eqtr4di ⊢ ( 𝑣 = ⟨ 𝑦 , 𝑧 ⟩ → ( 𝑑 ‘ 𝑣 ) = ( 𝑦 𝑑 𝑧 ) )
24 23 eqeq2d ⊢ ( 𝑣 = ⟨ 𝑦 , 𝑧 ⟩ → ( ( 𝑤 𝑑 𝑥 ) = ( 𝑑 ‘ 𝑣 ) ↔ ( 𝑤 𝑑 𝑥 ) = ( 𝑦 𝑑 𝑧 ) ) )
25 20 24 bibi12d ⊢ ( 𝑣 = ⟨ 𝑦 , 𝑧 ⟩ → ( ( ⟨ 𝑤 , 𝑥 ⟩ 𝑅 𝑣 ↔ ( 𝑤 𝑑 𝑥 ) = ( 𝑑 ‘ 𝑣 ) ) ↔ ( ⟨ 𝑤 , 𝑥 ⟩ 𝑅 ⟨ 𝑦 , 𝑧 ⟩ ↔ ( 𝑤 𝑑 𝑥 ) = ( 𝑦 𝑑 𝑧 ) ) ) )
26 19 25 rspc2va ⊢ ( ( ( ⟨ 𝑤 , 𝑥 ⟩ ∈ ( 𝑃 × 𝑃 ) ∧ ⟨ 𝑦 , 𝑧 ⟩ ∈ ( 𝑃 × 𝑃 ) ) ∧ ∀ 𝑢 ∈ ( 𝑃 × 𝑃 ) ∀ 𝑣 ∈ ( 𝑃 × 𝑃 ) ( 𝑢 𝑅 𝑣 ↔ ( 𝑑 ‘ 𝑢 ) = ( 𝑑 ‘ 𝑣 ) ) ) → ( ⟨ 𝑤 , 𝑥 ⟩ 𝑅 ⟨ 𝑦 , 𝑧 ⟩ ↔ ( 𝑤 𝑑 𝑥 ) = ( 𝑦 𝑑 𝑧 ) ) )
27 9 12 13 26 syl21anc ⊢ ( ( ( ∀ 𝑢 ∈ ( 𝑃 × 𝑃 ) ∀ 𝑣 ∈ ( 𝑃 × 𝑃 ) ( 𝑢 𝑅 𝑣 ↔ ( 𝑑 ‘ 𝑢 ) = ( 𝑑 ‘ 𝑣 ) ) ∧ ( 𝑤 ∈ 𝑃 ∧ 𝑥 ∈ 𝑃 ) ) ∧ ( 𝑦 ∈ 𝑃 ∧ 𝑧 ∈ 𝑃 ) ) → ( ⟨ 𝑤 , 𝑥 ⟩ 𝑅 ⟨ 𝑦 , 𝑧 ⟩ ↔ ( 𝑤 𝑑 𝑥 ) = ( 𝑦 𝑑 𝑧 ) ) )
28 27 ralrimivva ⊢ ( ( ∀ 𝑢 ∈ ( 𝑃 × 𝑃 ) ∀ 𝑣 ∈ ( 𝑃 × 𝑃 ) ( 𝑢 𝑅 𝑣 ↔ ( 𝑑 ‘ 𝑢 ) = ( 𝑑 ‘ 𝑣 ) ) ∧ ( 𝑤 ∈ 𝑃 ∧ 𝑥 ∈ 𝑃 ) ) → ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ( ⟨ 𝑤 , 𝑥 ⟩ 𝑅 ⟨ 𝑦 , 𝑧 ⟩ ↔ ( 𝑤 𝑑 𝑥 ) = ( 𝑦 𝑑 𝑧 ) ) )
29 28 ralrimivva ⊢ ( ∀ 𝑢 ∈ ( 𝑃 × 𝑃 ) ∀ 𝑣 ∈ ( 𝑃 × 𝑃 ) ( 𝑢 𝑅 𝑣 ↔ ( 𝑑 ‘ 𝑢 ) = ( 𝑑 ‘ 𝑣 ) ) → ∀ 𝑤 ∈ 𝑃 ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ( ⟨ 𝑤 , 𝑥 ⟩ 𝑅 ⟨ 𝑦 , 𝑧 ⟩ ↔ ( 𝑤 𝑑 𝑥 ) = ( 𝑦 𝑑 𝑧 ) ) )
30 29 anim2i ⊢ ( ( 𝑑 Fn ( 𝑃 × 𝑃 ) ∧ ∀ 𝑢 ∈ ( 𝑃 × 𝑃 ) ∀ 𝑣 ∈ ( 𝑃 × 𝑃 ) ( 𝑢 𝑅 𝑣 ↔ ( 𝑑 ‘ 𝑢 ) = ( 𝑑 ‘ 𝑣 ) ) ) → ( 𝑑 Fn ( 𝑃 × 𝑃 ) ∧ ∀ 𝑤 ∈ 𝑃 ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ( ⟨ 𝑤 , 𝑥 ⟩ 𝑅 ⟨ 𝑦 , 𝑧 ⟩ ↔ ( 𝑤 𝑑 𝑥 ) = ( 𝑦 𝑑 𝑧 ) ) ) )
31 6 30 eximii ⊢ ∃ 𝑑 ( 𝑑 Fn ( 𝑃 × 𝑃 ) ∧ ∀ 𝑤 ∈ 𝑃 ∀ 𝑥 ∈ 𝑃 ∀ 𝑦 ∈ 𝑃 ∀ 𝑧 ∈ 𝑃 ( ⟨ 𝑤 , 𝑥 ⟩ 𝑅 ⟨ 𝑦 , 𝑧 ⟩ ↔ ( 𝑤 𝑑 𝑥 ) = ( 𝑦 𝑑 𝑧 ) ) )