Metamath Proof Explorer

Theorem isleagd

Description: Sufficient condition for "less than" angle relation, deduction version (Contributed by Thierry Arnoux, 12-Oct-2020)

Ref Expression
Hypotheses isleag.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
isleag.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
isleag.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
isleag.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
isleag.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
isleag.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
isleag.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
isleag.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
isleagd.s ⊢ ≤ = ( ≤∠ ‘ 𝐺 )
isleagd.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
isleagd.1 ⊢ ( 𝜑 → 𝑋 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
isleagd.2 ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑋 ”⟩ )
Assertion isleagd ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ≤ ⟨“ 𝐷 𝐸 𝐹 ”⟩ )

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 isleagd.s ⊢ ≤ = ( ≤∠ ‘ 𝐺 )
10 isleagd.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
11 isleagd.1 ⊢ ( 𝜑 → 𝑋 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
12 isleagd.2 ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑋 ”⟩ )
13 9 eqcomi ⊢ ( ≤∠ ‘ 𝐺 ) = ≤
14 13 a1i ⊢ ( 𝜑 → ( ≤∠ ‘ 𝐺 ) = ≤ )
15 simpr ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → 𝑥 = 𝑋 )
16 15 breq1d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( 𝑥 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ↔ 𝑋 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ) )
17 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → 𝐷 = 𝐷 )
18 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → 𝐸 = 𝐸 )
19 17 18 15 s3eqd ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ⟨“ 𝐷 𝐸 𝑥 ”⟩ = ⟨“ 𝐷 𝐸 𝑋 ”⟩ )
20 19 breq2d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑥 ”⟩ ↔ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑋 ”⟩ ) )
21 16 20 anbi12d ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑋 ) → ( ( 𝑥 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑥 ”⟩ ) ↔ ( 𝑋 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑋 ”⟩ ) ) )
22 11 12 jca ⊢ ( 𝜑 → ( 𝑋 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑋 ”⟩ ) )
23 10 21 22 rspcedvd ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 ( 𝑥 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑥 ”⟩ ) )
24 1 2 3 4 5 6 7 8 isleag ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( ≤∠ ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ↔ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑥 ”⟩ ) ) )
25 23 24 mpbird ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( ≤∠ ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
26 14 25 breqdi ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ≤ ⟨“ 𝐷 𝐸 𝐹 ”⟩ )