Metamath Proof Explorer

Theorem trgcopyeu

Description: Triangle construction: a copy of a given triangle can always be constructed in such a way that one side is lying on a half-line, and the third vertex is on a given half-plane: uniqueness part. Second part of Theorem 10.16 of Schwabhauser p. 92. (Contributed by Thierry Arnoux, 8-Aug-2020)

Ref Expression
Hypotheses trgcopy.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
trgcopy.m ⊢ − = ( dist ‘ 𝐺 )
trgcopy.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
trgcopy.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
trgcopy.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
trgcopy.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
trgcopy.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
trgcopy.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
trgcopy.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
trgcopy.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
trgcopy.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
trgcopy.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
trgcopy.1 ⊢ ( 𝜑 → ¬ ( 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) )
trgcopy.2 ⊢ ( 𝜑 → ¬ ( 𝐷 ∈ ( 𝐸 𝐿 𝐹 ) ∨ 𝐸 = 𝐹 ) )
trgcopy.3 ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = ( 𝐷 − 𝐸 ) )
Assertion trgcopyeu ( 𝜑 → ∃! 𝑓 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑓 ”⟩ ∧ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) )

Proof

Step Hyp Ref Expression
1 trgcopy.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 trgcopy.m ⊢ − = ( dist ‘ 𝐺 )
3 trgcopy.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 trgcopy.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
5 trgcopy.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
6 trgcopy.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
7 trgcopy.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
8 trgcopy.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
9 trgcopy.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
10 trgcopy.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
11 trgcopy.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
12 trgcopy.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
13 trgcopy.1 ⊢ ( 𝜑 → ¬ ( 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) )
14 trgcopy.2 ⊢ ( 𝜑 → ¬ ( 𝐷 ∈ ( 𝐸 𝐿 𝐹 ) ∨ 𝐸 = 𝐹 ) )
15 trgcopy.3 ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = ( 𝐷 − 𝐸 ) )
16 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 trgcopy ⊢ ( 𝜑 → ∃ 𝑓 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑓 ”⟩ ∧ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) )
17 6 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑓 ”⟩ ∧ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑘 ”⟩ ) ∧ 𝑘 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) → 𝐺 ∈ TarskiG )
18 7 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑓 ”⟩ ∧ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑘 ”⟩ ) ∧ 𝑘 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) → 𝐴 ∈ 𝑃 )
19 8 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑓 ”⟩ ∧ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑘 ”⟩ ) ∧ 𝑘 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) → 𝐵 ∈ 𝑃 )
20 9 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑓 ”⟩ ∧ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑘 ”⟩ ) ∧ 𝑘 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) → 𝐶 ∈ 𝑃 )
21 10 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑓 ”⟩ ∧ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑘 ”⟩ ) ∧ 𝑘 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) → 𝐷 ∈ 𝑃 )
22 11 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑓 ”⟩ ∧ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑘 ”⟩ ) ∧ 𝑘 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) → 𝐸 ∈ 𝑃 )
23 12 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑓 ”⟩ ∧ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑘 ”⟩ ) ∧ 𝑘 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) → 𝐹 ∈ 𝑃 )
24 13 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑓 ”⟩ ∧ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑘 ”⟩ ) ∧ 𝑘 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) → ¬ ( 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) )
25 14 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑓 ”⟩ ∧ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑘 ”⟩ ) ∧ 𝑘 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) → ¬ ( 𝐷 ∈ ( 𝐸 𝐿 𝐹 ) ∨ 𝐸 = 𝐹 ) )
26 15 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑓 ”⟩ ∧ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑘 ”⟩ ) ∧ 𝑘 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) → ( 𝐴 − 𝐵 ) = ( 𝐷 − 𝐸 ) )
27 simpl ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → 𝑥 = 𝑎 )
28 27 eleq1d ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → ( 𝑥 ∈ ( 𝑃 ∖ ( 𝐷 𝐿 𝐸 ) ) ↔ 𝑎 ∈ ( 𝑃 ∖ ( 𝐷 𝐿 𝐸 ) ) ) )
29 simpr ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → 𝑦 = 𝑏 )
30 29 eleq1d ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → ( 𝑦 ∈ ( 𝑃 ∖ ( 𝐷 𝐿 𝐸 ) ) ↔ 𝑏 ∈ ( 𝑃 ∖ ( 𝐷 𝐿 𝐸 ) ) ) )
31 28 30 anbi12d ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → ( ( 𝑥 ∈ ( 𝑃 ∖ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑦 ∈ ( 𝑃 ∖ ( 𝐷 𝐿 𝐸 ) ) ) ↔ ( 𝑎 ∈ ( 𝑃 ∖ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝐷 𝐿 𝐸 ) ) ) ) )
32 simpr ⊢ ( ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) ∧ 𝑧 = 𝑡 ) → 𝑧 = 𝑡 )
33 simpll ⊢ ( ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) ∧ 𝑧 = 𝑡 ) → 𝑥 = 𝑎 )
34 simplr ⊢ ( ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) ∧ 𝑧 = 𝑡 ) → 𝑦 = 𝑏 )
35 33 34 oveq12d ⊢ ( ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) ∧ 𝑧 = 𝑡 ) → ( 𝑥 𝐼 𝑦 ) = ( 𝑎 𝐼 𝑏 ) )
36 32 35 eleq12d ⊢ ( ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) ∧ 𝑧 = 𝑡 ) → ( 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ↔ 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) )
37 36 cbvrexdva ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → ( ∃ 𝑧 ∈ ( 𝐷 𝐿 𝐸 ) 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ↔ ∃ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) )
38 31 37 anbi12d ⊢ ( ( 𝑥 = 𝑎 ∧ 𝑦 = 𝑏 ) → ( ( ( 𝑥 ∈ ( 𝑃 ∖ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑦 ∈ ( 𝑃 ∖ ( 𝐷 𝐿 𝐸 ) ) ) ∧ ∃ 𝑧 ∈ ( 𝐷 𝐿 𝐸 ) 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ) ↔ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝐷 𝐿 𝐸 ) ) ) ∧ ∃ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) ) )
39 38 cbvopabv ⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( 𝑥 ∈ ( 𝑃 ∖ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑦 ∈ ( 𝑃 ∖ ( 𝐷 𝐿 𝐸 ) ) ) ∧ ∃ 𝑧 ∈ ( 𝐷 𝐿 𝐸 ) 𝑧 ∈ ( 𝑥 𝐼 𝑦 ) ) } = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝐷 𝐿 𝐸 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝐷 𝐿 𝐸 ) ) ) ∧ ∃ 𝑡 ∈ ( 𝐷 𝐿 𝐸 ) 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
40 simp-5r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑓 ”⟩ ∧ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑘 ”⟩ ) ∧ 𝑘 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) → 𝑓 ∈ 𝑃 )
41 simp-4r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑓 ”⟩ ∧ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑘 ”⟩ ) ∧ 𝑘 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) → 𝑘 ∈ 𝑃 )
42 simpllr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑓 ”⟩ ∧ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑘 ”⟩ ) ∧ 𝑘 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑓 ”⟩ ∧ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) )
43 42 simpld ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑓 ”⟩ ∧ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑘 ”⟩ ) ∧ 𝑘 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑓 ”⟩ )
44 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑓 ”⟩ ∧ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑘 ”⟩ ) ∧ 𝑘 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑘 ”⟩ )
45 42 simprd ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑓 ”⟩ ∧ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑘 ”⟩ ) ∧ 𝑘 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) → 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 )
46 simpr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑓 ”⟩ ∧ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑘 ”⟩ ) ∧ 𝑘 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) → 𝑘 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 )
47 1 2 3 4 5 17 18 19 20 21 22 23 24 25 26 39 40 41 43 44 45 46 trgcopyeulem ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑓 ”⟩ ∧ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑘 ”⟩ ) ∧ 𝑘 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) → 𝑓 = 𝑘 )
48 47 anasss ⊢ ( ( ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑓 ”⟩ ∧ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑘 ”⟩ ∧ 𝑘 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) → 𝑓 = 𝑘 )
49 48 expl ⊢ ( ( ( 𝜑 ∧ 𝑓 ∈ 𝑃 ) ∧ 𝑘 ∈ 𝑃 ) → ( ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑓 ”⟩ ∧ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑘 ”⟩ ∧ 𝑘 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) → 𝑓 = 𝑘 ) )
50 49 anasss ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ 𝑃 ∧ 𝑘 ∈ 𝑃 ) ) → ( ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑓 ”⟩ ∧ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑘 ”⟩ ∧ 𝑘 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) → 𝑓 = 𝑘 ) )
51 50 ralrimivva ⊢ ( 𝜑 → ∀ 𝑓 ∈ 𝑃 ∀ 𝑘 ∈ 𝑃 ( ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑓 ”⟩ ∧ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑘 ”⟩ ∧ 𝑘 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) → 𝑓 = 𝑘 ) )
52 eqidd ⊢ ( 𝑓 = 𝑘 → 𝐷 = 𝐷 )
53 eqidd ⊢ ( 𝑓 = 𝑘 → 𝐸 = 𝐸 )
54 id ⊢ ( 𝑓 = 𝑘 → 𝑓 = 𝑘 )
55 52 53 54 s3eqd ⊢ ( 𝑓 = 𝑘 → ⟨“ 𝐷 𝐸 𝑓 ”⟩ = ⟨“ 𝐷 𝐸 𝑘 ”⟩ )
56 55 breq2d ⊢ ( 𝑓 = 𝑘 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑓 ”⟩ ↔ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑘 ”⟩ ) )
57 breq1 ⊢ ( 𝑓 = 𝑘 → ( 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ↔ 𝑘 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) )
58 56 57 anbi12d ⊢ ( 𝑓 = 𝑘 → ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑓 ”⟩ ∧ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ↔ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑘 ”⟩ ∧ 𝑘 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) )
59 58 reu4 ⊢ ( ∃! 𝑓 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑓 ”⟩ ∧ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ↔ ( ∃ 𝑓 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑓 ”⟩ ∧ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ∧ ∀ 𝑓 ∈ 𝑃 ∀ 𝑘 ∈ 𝑃 ( ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑓 ”⟩ ∧ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑘 ”⟩ ∧ 𝑘 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) ) → 𝑓 = 𝑘 ) ) )
60 16 51 59 sylanbrc ⊢ ( 𝜑 → ∃! 𝑓 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑓 ”⟩ ∧ 𝑓 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐷 𝐿 𝐸 ) ) 𝐹 ) )