Metamath Proof Explorer


Theorem inagflat

Description: Any point lies in a flat angle. (Contributed by Thierry Arnoux, 13-Feb-2023)

Ref Expression
Hypotheses isinag.p 𝑃 = ( Base ‘ 𝐺 )
isinag.i 𝐼 = ( Itv ‘ 𝐺 )
isinag.k 𝐾 = ( hlG ‘ 𝐺 )
isinag.x ( 𝜑𝑋𝑃 )
isinag.a ( 𝜑𝐴𝑃 )
isinag.b ( 𝜑𝐵𝑃 )
isinag.c ( 𝜑𝐶𝑃 )
inagflat.g ( 𝜑𝐺 ∈ TarskiG )
inagflat.x ( 𝜑𝑋𝑃 )
inagflat.1 ( 𝜑𝐴𝐵 )
inagflat.2 ( 𝜑𝐶𝐵 )
inagflat.3 ( 𝜑𝑋𝐵 )
inagflat.4 ( 𝜑𝐵 ∈ ( 𝐴 𝐼 𝐶 ) )
Assertion inagflat ( 𝜑𝑋 ( inA ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ )

Proof

Step Hyp Ref Expression
1 isinag.p 𝑃 = ( Base ‘ 𝐺 )
2 isinag.i 𝐼 = ( Itv ‘ 𝐺 )
3 isinag.k 𝐾 = ( hlG ‘ 𝐺 )
4 isinag.x ( 𝜑𝑋𝑃 )
5 isinag.a ( 𝜑𝐴𝑃 )
6 isinag.b ( 𝜑𝐵𝑃 )
7 isinag.c ( 𝜑𝐶𝑃 )
8 inagflat.g ( 𝜑𝐺 ∈ TarskiG )
9 inagflat.x ( 𝜑𝑋𝑃 )
10 inagflat.1 ( 𝜑𝐴𝐵 )
11 inagflat.2 ( 𝜑𝐶𝐵 )
12 inagflat.3 ( 𝜑𝑋𝐵 )
13 inagflat.4 ( 𝜑𝐵 ∈ ( 𝐴 𝐼 𝐶 ) )
14 eqidd ( 𝜑𝐵 = 𝐵 )
15 14 orcd ( 𝜑 → ( 𝐵 = 𝐵𝐵 ( 𝐾𝐵 ) 𝑋 ) )
16 1 2 3 4 5 6 7 8 6 10 11 12 13 15 isinagd ( 𝜑𝑋 ( inA ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ )