Metamath Proof Explorer


Theorem inagne1

Description: Deduce inequality from the in-angle relation. (Contributed by Thierry Arnoux, 29-Oct-2021)

Ref Expression
Hypotheses isinag.p 𝑃 = ( Base ‘ 𝐺 )
isinag.i 𝐼 = ( Itv ‘ 𝐺 )
isinag.k 𝐾 = ( hlG ‘ 𝐺 )
isinag.x ( 𝜑𝑋𝑃 )
isinag.a ( 𝜑𝐴𝑃 )
isinag.b ( 𝜑𝐵𝑃 )
isinag.c ( 𝜑𝐶𝑃 )
inagflat.g ( 𝜑𝐺 ∈ TarskiG )
inagswap.1 ( 𝜑𝑋 ( inA ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ )
Assertion inagne1 ( 𝜑𝐴𝐵 )

Proof

Step Hyp Ref Expression
1 isinag.p 𝑃 = ( Base ‘ 𝐺 )
2 isinag.i 𝐼 = ( Itv ‘ 𝐺 )
3 isinag.k 𝐾 = ( hlG ‘ 𝐺 )
4 isinag.x ( 𝜑𝑋𝑃 )
5 isinag.a ( 𝜑𝐴𝑃 )
6 isinag.b ( 𝜑𝐵𝑃 )
7 isinag.c ( 𝜑𝐶𝑃 )
8 inagflat.g ( 𝜑𝐺 ∈ TarskiG )
9 inagswap.1 ( 𝜑𝑋 ( inA ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ )
10 1 2 3 4 5 6 7 8 isinag ( 𝜑 → ( 𝑋 ( inA ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ ↔ ( ( 𝐴𝐵𝐶𝐵𝑋𝐵 ) ∧ ∃ 𝑥𝑃 ( 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ∧ ( 𝑥 = 𝐵𝑥 ( 𝐾𝐵 ) 𝑋 ) ) ) ) )
11 9 10 mpbid ( 𝜑 → ( ( 𝐴𝐵𝐶𝐵𝑋𝐵 ) ∧ ∃ 𝑥𝑃 ( 𝑥 ∈ ( 𝐴 𝐼 𝐶 ) ∧ ( 𝑥 = 𝐵𝑥 ( 𝐾𝐵 ) 𝑋 ) ) ) )
12 11 simpld ( 𝜑 → ( 𝐴𝐵𝐶𝐵𝑋𝐵 ) )
13 12 simp1d ( 𝜑𝐴𝐵 )