Metamath Proof Explorer

Theorem leagne1

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 leagne1 ( 𝜑 → 𝐴 ≠ 𝐵 )

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 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑥 ”⟩ ) ) → 𝐺 ∈ TarskiG )
13 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑥 ”⟩ ) ) → 𝐴 ∈ 𝑃 )
14 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑥 ”⟩ ) ) → 𝐵 ∈ 𝑃 )
15 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑥 ”⟩ ) ) → 𝐶 ∈ 𝑃 )
16 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑥 ”⟩ ) ) → 𝐷 ∈ 𝑃 )
17 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑥 ”⟩ ) ) → 𝐸 ∈ 𝑃 )
18 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑥 ”⟩ ) ) → 𝑥 ∈ 𝑃 )
19 simprr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑥 ”⟩ ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑥 ”⟩ )
20 1 10 11 12 13 14 15 16 17 18 19 cgrane1 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑃 ) ∧ ( 𝑥 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑥 ”⟩ ) ) → 𝐴 ≠ 𝐵 )
21 1 2 3 4 5 6 7 8 isleag ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( ≤∠ ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ↔ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑥 ”⟩ ) ) )
22 9 21 mpbid ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 ( 𝑥 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑥 ”⟩ ) )
23 20 22 r19.29a ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )