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=BaseG
isinag.i I=ItvG
isinag.k K=hl𝒢G
isinag.x φXP
isinag.a φAP
isinag.b φBP
isinag.c φCP
inagflat.g φG𝒢Tarski
inagflat.x φXP
inagflat.1 φAB
inagflat.2 φCB
inagflat.3 φXB
inagflat.4 φBAIC
Assertion inagflat φX𝒢G⟨“ABC”⟩

Proof

Step Hyp Ref Expression
1 isinag.p P=BaseG
2 isinag.i I=ItvG
3 isinag.k K=hl𝒢G
4 isinag.x φXP
5 isinag.a φAP
6 isinag.b φBP
7 isinag.c φCP
8 inagflat.g φG𝒢Tarski
9 inagflat.x φXP
10 inagflat.1 φAB
11 inagflat.2 φCB
12 inagflat.3 φXB
13 inagflat.4 φBAIC
14 eqidd φB=B
15 14 orcd φB=BBKBX
16 1 2 3 4 5 6 7 8 6 10 11 12 13 15 isinagd φX𝒢G⟨“ABC”⟩