Metamath Proof Explorer

Theorem leagne4

Description: Deduce inequality from the less-than angle relation. (Contributed by Thierry Arnoux, 25-Feb-2023)

Ref Expression
Hypotheses isleag.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
isleag.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
isleag.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
isleag.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
isleag.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
isleag.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
isleag.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
isleag.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
leagne.1 ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( ≤∠ ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
Assertion leagne4 ( 𝜑 → 𝐹 ≠ 𝐸 )

Proof

Step Hyp Ref Expression
1 isleag.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 isleag.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
3 isleag.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
4 isleag.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
5 isleag.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
6 isleag.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
7 isleag.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
8 isleag.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
9 leagne.1 ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( ≤∠ ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
10 eqid ⊢ ( Itv ‘ 𝐺 ) = ( Itv ‘ 𝐺 )
11 eqid ⊢ ( hlG ‘ 𝐺 ) = ( hlG ‘ 𝐺 )
12 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑥 ”⟩ ) ) → 𝑥 ∈ 𝑃 )
13 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑥 ”⟩ ) ) → 𝐷 ∈ 𝑃 )
14 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑥 ”⟩ ) ) → 𝐸 ∈ 𝑃 )
15 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑥 ”⟩ ) ) → 𝐹 ∈ 𝑃 )
16 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑥 ”⟩ ) ) → 𝐺 ∈ TarskiG )
17 simprl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑥 ”⟩ ) ) → 𝑥 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
18 1 10 11 12 13 14 15 16 17 inagne2 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑥 ”⟩ ) ) → 𝐹 ≠ 𝐸 )
19 1 2 3 4 5 6 7 8 isleag ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( ≤∠ ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ↔ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑥 ”⟩ ) ) )
20 9 19 mpbid ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 ( 𝑥 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑥 ”⟩ ) )
21 18 20 r19.29a ⊢ ( 𝜑 → 𝐹 ≠ 𝐸 )