Metamath Proof Explorer

Theorem leacgra

Description: GeoCoq l11__30 analogue: leA is preserved when both compared angles are replaced by congruent angles. (Contributed by JAG, 12-Aug-2026)

Ref Expression
Hypotheses leacgra.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
leacgra.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
leacgra.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
leacgra.s ⊢ ≤ = ( ≤∠ ‘ 𝐺 )
leacgra.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
leacgra.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
leacgra.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
leacgra.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
leacgra.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
leacgra.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
leacgra.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
leacgra.h ⊢ ( 𝜑 → 𝐻 ∈ 𝑃 )
leacgra.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑃 )
leacgra.j ⊢ ( 𝜑 → 𝐽 ∈ 𝑃 )
leacgra.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
leacgra.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
leacgra.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
leacgra.1 ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ≤ ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
leacgra.2 ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐻 𝑈 𝐽 ”⟩ )
leacgra.3 ⊢ ( 𝜑 → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ )
Assertion leacgra ( 𝜑 → ⟨“ 𝐻 𝑈 𝐽 ”⟩ ≤ ⟨“ 𝑋 𝑌 𝑍 ”⟩ )

Proof

Step Hyp Ref Expression
1 leacgra.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 leacgra.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
3 leacgra.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
4 leacgra.s ⊢ ≤ = ( ≤∠ ‘ 𝐺 )
5 leacgra.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6 leacgra.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
7 leacgra.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
8 leacgra.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
9 leacgra.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
10 leacgra.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
11 leacgra.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
12 leacgra.h ⊢ ( 𝜑 → 𝐻 ∈ 𝑃 )
13 leacgra.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑃 )
14 leacgra.j ⊢ ( 𝜑 → 𝐽 ∈ 𝑃 )
15 leacgra.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
16 leacgra.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
17 leacgra.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
18 leacgra.1 ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ≤ ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
19 leacgra.2 ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐻 𝑈 𝐽 ”⟩ )
20 leacgra.3 ⊢ ( 𝜑 → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ )
21 4 breqi ⊢ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ≤ ⟨“ 𝐷 𝐸 𝐹 ”⟩ ↔ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( ≤∠ ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
22 18 21 sylib ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( ≤∠ ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
23 1 2 3 5 6 7 8 9 10 11 12 13 14 22 19 leacgra1 ⊢ ( 𝜑 → ⟨“ 𝐻 𝑈 𝐽 ”⟩ ( ≤∠ ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
24 1 2 3 5 12 13 14 9 10 11 15 16 17 23 20 leacgra2 ⊢ ( 𝜑 → ⟨“ 𝐻 𝑈 𝐽 ”⟩ ( ≤∠ ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ )
25 4 breqi ⊢ ( ⟨“ 𝐻 𝑈 𝐽 ”⟩ ≤ ⟨“ 𝑋 𝑌 𝑍 ”⟩ ↔ ⟨“ 𝐻 𝑈 𝐽 ”⟩ ( ≤∠ ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ )
26 24 25 sylibr ⊢ ( 𝜑 → ⟨“ 𝐻 𝑈 𝐽 ”⟩ ≤ ⟨“ 𝑋 𝑌 𝑍 ”⟩ )