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 "> ) |
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 "> ) |