Metamath Proof Explorer


Theorem cgrane3

Description: Angles imply inequality. (Contributed by Thierry Arnoux, 1-Aug-2020)

Ref Expression
Hypotheses iscgra.p 𝑃 = ( Base ‘ 𝐺 )
iscgra.i 𝐼 = ( Itv ‘ 𝐺 )
iscgra.k 𝐾 = ( hlG ‘ 𝐺 )
iscgra.g ( 𝜑𝐺 ∈ TarskiG )
iscgra.a ( 𝜑𝐴𝑃 )
iscgra.b ( 𝜑𝐵𝑃 )
iscgra.c ( 𝜑𝐶𝑃 )
iscgra.d ( 𝜑𝐷𝑃 )
iscgra.e ( 𝜑𝐸𝑃 )
iscgra.f ( 𝜑𝐹𝑃 )
cgrahl1.2 ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
Assertion cgrane3 ( 𝜑𝐸𝐷 )

Proof

Step Hyp Ref Expression
1 iscgra.p 𝑃 = ( Base ‘ 𝐺 )
2 iscgra.i 𝐼 = ( Itv ‘ 𝐺 )
3 iscgra.k 𝐾 = ( hlG ‘ 𝐺 )
4 iscgra.g ( 𝜑𝐺 ∈ TarskiG )
5 iscgra.a ( 𝜑𝐴𝑃 )
6 iscgra.b ( 𝜑𝐵𝑃 )
7 iscgra.c ( 𝜑𝐶𝑃 )
8 iscgra.d ( 𝜑𝐷𝑃 )
9 iscgra.e ( 𝜑𝐸𝑃 )
10 iscgra.f ( 𝜑𝐹𝑃 )
11 cgrahl1.2 ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
12 simpllr ( ( ( ( 𝜑𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾𝐸 ) 𝐷𝑦 ( 𝐾𝐸 ) 𝐹 ) ) → 𝑥𝑃 )
13 8 ad3antrrr ( ( ( ( 𝜑𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾𝐸 ) 𝐷𝑦 ( 𝐾𝐸 ) 𝐹 ) ) → 𝐷𝑃 )
14 9 ad3antrrr ( ( ( ( 𝜑𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾𝐸 ) 𝐷𝑦 ( 𝐾𝐸 ) 𝐹 ) ) → 𝐸𝑃 )
15 4 ad3antrrr ( ( ( ( 𝜑𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾𝐸 ) 𝐷𝑦 ( 𝐾𝐸 ) 𝐹 ) ) → 𝐺 ∈ TarskiG )
16 simpr2 ( ( ( ( 𝜑𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾𝐸 ) 𝐷𝑦 ( 𝐾𝐸 ) 𝐹 ) ) → 𝑥 ( 𝐾𝐸 ) 𝐷 )
17 1 2 3 12 13 14 15 16 hlne2 ( ( ( ( 𝜑𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾𝐸 ) 𝐷𝑦 ( 𝐾𝐸 ) 𝐹 ) ) → 𝐷𝐸 )
18 17 necomd ( ( ( ( 𝜑𝑥𝑃 ) ∧ 𝑦𝑃 ) ∧ ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾𝐸 ) 𝐷𝑦 ( 𝐾𝐸 ) 𝐹 ) ) → 𝐸𝐷 )
19 1 2 3 4 5 6 7 8 9 10 iscgra ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ↔ ∃ 𝑥𝑃𝑦𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾𝐸 ) 𝐷𝑦 ( 𝐾𝐸 ) 𝐹 ) ) )
20 11 19 mpbid ( 𝜑 → ∃ 𝑥𝑃𝑦𝑃 ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝑥 𝐸 𝑦 ”⟩ ∧ 𝑥 ( 𝐾𝐸 ) 𝐷𝑦 ( 𝐾𝐸 ) 𝐹 ) )
21 18 20 r19.29vva ( 𝜑𝐸𝐷 )