Metamath Proof Explorer

Theorem hpgtr

Description: The half-plane relation is transitive. Theorem 9.13 of Schwabhauser p. 72. (Contributed by Thierry Arnoux, 4-Mar-2020)

Ref Expression
Hypotheses hpgid.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
hpgid.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
hpgid.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
hpgid.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
hpgid.d ⊢ ( 𝜑 → 𝐷 ∈ ran 𝐿 )
hpgid.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
hpgid.o ⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐷 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐷 ) ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
hpgcom.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
hpgcom.1 ⊢ ( 𝜑 → 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 )
hpgtr.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
hpgtr.1 ⊢ ( 𝜑 → 𝐵 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐶 )
Assertion hpgtr ( 𝜑 → 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐶 )

Proof

Step Hyp Ref Expression
1 hpgid.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 hpgid.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
3 hpgid.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
4 hpgid.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5 hpgid.d ⊢ ( 𝜑 → 𝐷 ∈ ran 𝐿 )
6 hpgid.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
7 hpgid.o ⊢ 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ 𝐷 ) ∧ 𝑏 ∈ ( 𝑃 ∖ 𝐷 ) ) ∧ ∃ 𝑡 ∈ 𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
8 hpgcom.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
9 hpgcom.1 ⊢ ( 𝜑 → 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 )
10 hpgtr.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
11 hpgtr.1 ⊢ ( 𝜑 → 𝐵 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐶 )
12 1 2 3 7 4 5 6 8 hpgbr ⊢ ( 𝜑 → ( 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐵 ↔ ∃ 𝑐 ∈ 𝑃 ( 𝐴 𝑂 𝑐 ∧ 𝐵 𝑂 𝑐 ) ) )
13 9 12 mpbid ⊢ ( 𝜑 → ∃ 𝑐 ∈ 𝑃 ( 𝐴 𝑂 𝑐 ∧ 𝐵 𝑂 𝑐 ) )
14 simprl ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑐 ∧ 𝐵 𝑂 𝑐 ) ) → 𝐴 𝑂 𝑐 )
15 11 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑐 ∧ 𝐵 𝑂 𝑐 ) ) → 𝐵 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐶 )
16 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑐 ∧ 𝐵 𝑂 𝑐 ) ) → 𝐺 ∈ TarskiG )
17 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑐 ∧ 𝐵 𝑂 𝑐 ) ) → 𝐷 ∈ ran 𝐿 )
18 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑐 ∧ 𝐵 𝑂 𝑐 ) ) → 𝐵 ∈ 𝑃 )
19 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑐 ∧ 𝐵 𝑂 𝑐 ) ) → 𝐶 ∈ 𝑃 )
20 simplr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑐 ∧ 𝐵 𝑂 𝑐 ) ) → 𝑐 ∈ 𝑃 )
21 simprr ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑐 ∧ 𝐵 𝑂 𝑐 ) ) → 𝐵 𝑂 𝑐 )
22 1 2 3 7 16 17 18 19 20 21 lnopp2hpgb ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑐 ∧ 𝐵 𝑂 𝑐 ) ) → ( 𝐶 𝑂 𝑐 ↔ 𝐵 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐶 ) )
23 15 22 mpbird ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑐 ∧ 𝐵 𝑂 𝑐 ) ) → 𝐶 𝑂 𝑐 )
24 14 23 jca ⊢ ( ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) ∧ ( 𝐴 𝑂 𝑐 ∧ 𝐵 𝑂 𝑐 ) ) → ( 𝐴 𝑂 𝑐 ∧ 𝐶 𝑂 𝑐 ) )
25 24 ex ⊢ ( ( 𝜑 ∧ 𝑐 ∈ 𝑃 ) → ( ( 𝐴 𝑂 𝑐 ∧ 𝐵 𝑂 𝑐 ) → ( 𝐴 𝑂 𝑐 ∧ 𝐶 𝑂 𝑐 ) ) )
26 25 reximdva ⊢ ( 𝜑 → ( ∃ 𝑐 ∈ 𝑃 ( 𝐴 𝑂 𝑐 ∧ 𝐵 𝑂 𝑐 ) → ∃ 𝑐 ∈ 𝑃 ( 𝐴 𝑂 𝑐 ∧ 𝐶 𝑂 𝑐 ) ) )
27 13 26 mpd ⊢ ( 𝜑 → ∃ 𝑐 ∈ 𝑃 ( 𝐴 𝑂 𝑐 ∧ 𝐶 𝑂 𝑐 ) )
28 1 2 3 7 4 5 6 10 hpgbr ⊢ ( 𝜑 → ( 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐶 ↔ ∃ 𝑐 ∈ 𝑃 ( 𝐴 𝑂 𝑐 ∧ 𝐶 𝑂 𝑐 ) ) )
29 27 28 mpbird ⊢ ( 𝜑 → 𝐴 ( ( hpG ‘ 𝐺 ) ‘ 𝐷 ) 𝐶 )