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
|- P = ( Base ` G )
isinag.i
|- I = ( Itv ` G )
isinag.k
|- K = ( hlG ` G )
isinag.x
|- ( ph -> X e. P )
isinag.a
|- ( ph -> A e. P )
isinag.b
|- ( ph -> B e. P )
isinag.c
|- ( ph -> C e. P )
inagflat.g
|- ( ph -> G e. TarskiG )
inagflat.x
|- ( ph -> X e. P )
inagflat.1
|- ( ph -> A =/= B )
inagflat.2
|- ( ph -> C =/= B )
inagflat.3
|- ( ph -> X =/= B )
inagflat.4
|- ( ph -> B e. ( A I C ) )
Assertion inagflat
|- ( ph -> X ( inA ` G ) <" A B C "> )

Proof

Step Hyp Ref Expression
1 isinag.p
 |-  P = ( Base ` G )
2 isinag.i
 |-  I = ( Itv ` G )
3 isinag.k
 |-  K = ( hlG ` G )
4 isinag.x
 |-  ( ph -> X e. P )
5 isinag.a
 |-  ( ph -> A e. P )
6 isinag.b
 |-  ( ph -> B e. P )
7 isinag.c
 |-  ( ph -> C e. P )
8 inagflat.g
 |-  ( ph -> G e. TarskiG )
9 inagflat.x
 |-  ( ph -> X e. P )
10 inagflat.1
 |-  ( ph -> A =/= B )
11 inagflat.2
 |-  ( ph -> C =/= B )
12 inagflat.3
 |-  ( ph -> X =/= B )
13 inagflat.4
 |-  ( ph -> B e. ( A I C ) )
14 eqidd
 |-  ( ph -> B = B )
15 14 orcd
 |-  ( ph -> ( B = B \/ B ( K ` B ) X ) )
16 1 2 3 4 5 6 7 8 6 10 11 12 13 15 isinagd
 |-  ( ph -> X ( inA ` G ) <" A B C "> )