Metamath Proof Explorer

Theorem iscgra1

Description: A special version of iscgra where one distance is known to be equal. In this case, angle congruence can be written with only one quantifier. (Contributed by Thierry Arnoux, 9-Aug-2020)

Ref Expression
Hypotheses iscgra.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
iscgra.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
iscgra.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
iscgra.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
iscgra.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
iscgra.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
iscgra.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
iscgra.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
iscgra.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
iscgra.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
iscgra1.m ⊢ − = ( dist ‘ 𝐺 )
iscgra1.1 ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
iscgra1.2 ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = ( 𝐷 − 𝐸 ) )
Assertion iscgra1 ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ↔ ∃ 𝑥 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 iscgra.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 iscgra.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
3 iscgra.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
4 iscgra.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5 iscgra.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
6 iscgra.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
7 iscgra.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
8 iscgra.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
9 iscgra.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
10 iscgra.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
11 iscgra1.m ⊢ − = ( dist ‘ 𝐺 )
12 iscgra1.1 ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
13 iscgra1.2 ⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = ( 𝐷 − 𝐸 ) )
14 1 2 3 4 5 6 7 8 9 10 iscgra ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ↔ ∃ 𝑦 ∈ 𝑃 ∃ 𝑥 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑦 𝐸 𝑥 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) )
15 9 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑦 𝐸 𝑥 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝐸 ∈ 𝑃 )
16 6 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑦 𝐸 𝑥 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝐵 ∈ 𝑃 )
17 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑦 𝐸 𝑥 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝐴 ∈ 𝑃 )
18 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑦 𝐸 𝑥 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝐺 ∈ TarskiG )
19 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑦 𝐸 𝑥 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝐷 ∈ 𝑃 )
20 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑦 𝐸 𝑥 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝑦 ∈ 𝑃 )
21 simpr2 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑦 𝐸 𝑥 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐷 )
22 1 2 3 20 19 15 18 21 hlne2 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑦 𝐸 𝑥 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝐷 ≠ 𝐸 )
23 12 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑦 𝐸 𝑥 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝐴 ≠ 𝐵 )
24 23 necomd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑦 𝐸 𝑥 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝐵 ≠ 𝐴 )
25 1 2 3 19 15 15 18 22 hlid ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑦 𝐸 𝑥 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝐷 ( 𝐾 ‘ 𝐸 ) 𝐷 )
26 eqid ⊢ ( cgrG ‘ 𝐺 ) = ( cgrG ‘ 𝐺 )
27 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑦 𝐸 𝑥 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝐶 ∈ 𝑃 )
28 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑦 𝐸 𝑥 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝑥 ∈ 𝑃 )
29 simpr1 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑦 𝐸 𝑥 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑦 𝐸 𝑥 ”⟩ )
30 1 11 2 26 18 17 16 27 20 15 28 29 cgr3simp1 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑦 𝐸 𝑥 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ( 𝐴 − 𝐵 ) = ( 𝑦 − 𝐸 ) )
31 30 eqcomd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑦 𝐸 𝑥 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ( 𝑦 − 𝐸 ) = ( 𝐴 − 𝐵 ) )
32 1 11 2 18 20 15 17 16 31 tgcgrcomlr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑦 𝐸 𝑥 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ( 𝐸 − 𝑦 ) = ( 𝐵 − 𝐴 ) )
33 13 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑦 𝐸 𝑥 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ( 𝐴 − 𝐵 ) = ( 𝐷 − 𝐸 ) )
34 33 eqcomd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑦 𝐸 𝑥 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ( 𝐷 − 𝐸 ) = ( 𝐴 − 𝐵 ) )
35 1 11 2 18 19 15 17 16 34 tgcgrcomlr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑦 𝐸 𝑥 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ( 𝐸 − 𝐷 ) = ( 𝐵 − 𝐴 ) )
36 1 2 3 15 16 17 18 19 11 22 24 20 19 21 25 32 35 hlcgreulem ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑦 𝐸 𝑥 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝑦 = 𝐷 )
37 simpr3 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑦 𝐸 𝑥 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 )
38 36 29 37 jca32 ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑦 𝐸 𝑥 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ( 𝑦 = 𝐷 ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑦 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) )
39 simprrl ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑦 = 𝐷 ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑦 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑦 𝐸 𝑥 ”⟩ )
40 simprl ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑦 = 𝐷 ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑦 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) ) → 𝑦 = 𝐷 )
41 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑦 = 𝐷 ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑦 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) ) → 𝐷 ∈ 𝑃 )
42 9 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑦 = 𝐷 ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑦 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) ) → 𝐸 ∈ 𝑃 )
43 4 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑦 = 𝐷 ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑦 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) ) → 𝐺 ∈ TarskiG )
44 1 11 2 4 5 6 8 9 13 12 tgcgrneq ⊢ ( 𝜑 → 𝐷 ≠ 𝐸 )
45 44 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑦 = 𝐷 ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑦 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) ) → 𝐷 ≠ 𝐸 )
46 1 2 3 41 41 42 43 45 hlid ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑦 = 𝐷 ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑦 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) ) → 𝐷 ( 𝐾 ‘ 𝐸 ) 𝐷 )
47 40 46 eqbrtrd ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑦 = 𝐷 ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑦 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) ) → 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐷 )
48 simprrr ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑦 = 𝐷 ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑦 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) ) → 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 )
49 39 47 48 3jca ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑦 = 𝐷 ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑦 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑦 𝐸 𝑥 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 ) )
50 38 49 impbida ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) ∧ 𝑥 ∈ 𝑃 ) → ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑦 𝐸 𝑥 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ↔ ( 𝑦 = 𝐷 ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑦 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) ) )
51 50 rexbidva ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) → ( ∃ 𝑥 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑦 𝐸 𝑥 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ↔ ∃ 𝑥 ∈ 𝑃 ( 𝑦 = 𝐷 ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑦 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) ) )
52 r19.42v ⊢ ( ∃ 𝑥 ∈ 𝑃 ( 𝑦 = 𝐷 ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑦 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) ↔ ( 𝑦 = 𝐷 ∧ ∃ 𝑥 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑦 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) )
53 51 52 bitrdi ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑃 ) → ( ∃ 𝑥 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑦 𝐸 𝑥 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ↔ ( 𝑦 = 𝐷 ∧ ∃ 𝑥 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑦 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) ) )
54 53 rexbidva ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ 𝑃 ∃ 𝑥 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑦 𝐸 𝑥 ”⟩ ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ↔ ∃ 𝑦 ∈ 𝑃 ( 𝑦 = 𝐷 ∧ ∃ 𝑥 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑦 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) ) )
55 id ⊢ ( 𝑦 = 𝐷 → 𝑦 = 𝐷 )
56 eqidd ⊢ ( 𝑦 = 𝐷 → 𝐸 = 𝐸 )
57 eqidd ⊢ ( 𝑦 = 𝐷 → 𝑥 = 𝑥 )
58 55 56 57 s3eqd ⊢ ( 𝑦 = 𝐷 → ⟨“ 𝑦 𝐸 𝑥 ”⟩ = ⟨“ 𝐷 𝐸 𝑥 ”⟩ )
59 58 breq2d ⊢ ( 𝑦 = 𝐷 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑦 𝐸 𝑥 ”⟩ ↔ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑥 ”⟩ ) )
60 59 anbi1d ⊢ ( 𝑦 = 𝐷 → ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑦 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ↔ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) )
61 60 rexbidv ⊢ ( 𝑦 = 𝐷 → ( ∃ 𝑥 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑦 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ↔ ∃ 𝑥 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) )
62 61 ceqsrexv ⊢ ( 𝐷 ∈ 𝑃 → ( ∃ 𝑦 ∈ 𝑃 ( 𝑦 = 𝐷 ∧ ∃ 𝑥 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑦 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) ↔ ∃ 𝑥 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) )
63 8 62 syl ⊢ ( 𝜑 → ( ∃ 𝑦 ∈ 𝑃 ( 𝑦 = 𝐷 ∧ ∃ 𝑥 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑦 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) ↔ ∃ 𝑥 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) )
64 14 54 63 3bitrd ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ↔ ∃ 𝑥 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑥 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) )