Metamath Proof Explorer

Theorem iscgrad

Description: Sufficient conditions for angle congruence, deduction version. (Contributed by Thierry Arnoux, 1-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 ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
iscgrad.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
iscgrad.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
iscgrad.1 ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑋 𝐸 𝑌 ”⟩ )
iscgrad.2 ⊢ ( 𝜑 → 𝑋 ( 𝐾 ‘ 𝐸 ) 𝐷 )
iscgrad.3 ⊢ ( 𝜑 → 𝑌 ( 𝐾 ‘ 𝐸 ) 𝐹 )
Assertion iscgrad ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )

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 iscgrad.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
12 iscgrad.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
13 iscgrad.1 ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑋 𝐸 𝑌 ”⟩ )
14 iscgrad.2 ⊢ ( 𝜑 → 𝑋 ( 𝐾 ‘ 𝐸 ) 𝐷 )
15 iscgrad.3 ⊢ ( 𝜑 → 𝑌 ( 𝐾 ‘ 𝐸 ) 𝐹 )
16 id ⊢ ( 𝑥 = 𝑋 → 𝑥 = 𝑋 )
17 eqidd ⊢ ( 𝑥 = 𝑋 → 𝐸 = 𝐸 )
18 eqidd ⊢ ( 𝑥 = 𝑋 → 𝑦 = 𝑦 )
19 16 17 18 s3eqd ⊢ ( 𝑥 = 𝑋 → ⟨“ 𝑥 𝐸 𝑦 ”⟩ = ⟨“ 𝑋 𝐸 𝑦 ”⟩ )
20 19 breq2d ⊢ ( 𝑥 = 𝑋 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ↔ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑋 𝐸 𝑦 ”⟩ ) )
21 breq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ↔ 𝑋 ( 𝐾 ‘ 𝐸 ) 𝐷 ) )
22 20 21 3anbi12d ⊢ ( 𝑥 = 𝑋 → ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ↔ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑋 𝐸 𝑦 ”⟩ ∧ 𝑋 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) )
23 eqidd ⊢ ( 𝑦 = 𝑌 → 𝑋 = 𝑋 )
24 eqidd ⊢ ( 𝑦 = 𝑌 → 𝐸 = 𝐸 )
25 id ⊢ ( 𝑦 = 𝑌 → 𝑦 = 𝑌 )
26 23 24 25 s3eqd ⊢ ( 𝑦 = 𝑌 → ⟨“ 𝑋 𝐸 𝑦 ”⟩ = ⟨“ 𝑋 𝐸 𝑌 ”⟩ )
27 26 breq2d ⊢ ( 𝑦 = 𝑌 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑋 𝐸 𝑦 ”⟩ ↔ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑋 𝐸 𝑌 ”⟩ ) )
28 breq1 ⊢ ( 𝑦 = 𝑌 → ( 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ↔ 𝑌 ( 𝐾 ‘ 𝐸 ) 𝐹 ) )
29 27 28 3anbi13d ⊢ ( 𝑦 = 𝑌 → ( ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑋 𝐸 𝑦 ”⟩ ∧ 𝑋 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ↔ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑋 𝐸 𝑌 ”⟩ ∧ 𝑋 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑌 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) )
30 22 29 rspc2ev ⊢ ( ( 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑋 𝐸 𝑌 ”⟩ ∧ 𝑋 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑌 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) → ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) )
31 11 12 13 14 15 30 syl113anc ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) )
32 1 2 3 4 5 6 7 8 9 10 iscgra ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ↔ ∃ 𝑥 ∈ 𝑃 ∃ 𝑦 ∈ 𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾 ‘ 𝐸 ) 𝐷 ∧ 𝑦 ( 𝐾 ‘ 𝐸 ) 𝐹 ) ) )
33 31 32 mpbird ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )