Description: Degenerated (zero-length) segments are minimal. Proposition 5.11 of Schwabhauser p. 42. (Contributed by Thierry Arnoux, 27-Jun-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | legval.p | |
|
legval.d | |
||
legval.i | |
||
legval.l | |
||
legval.g | |
||
legid.a | |
||
legid.b | |
||
legtrd.c | |
||
legtrd.d | |
||
Assertion | leg0 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | legval.p | |
|
2 | legval.d | |
|
3 | legval.i | |
|
4 | legval.l | |
|
5 | legval.g | |
|
6 | legid.a | |
|
7 | legid.b | |
|
8 | legtrd.c | |
|
9 | legtrd.d | |
|
10 | 1 2 3 5 8 9 | tgbtwntriv1 | |
11 | 1 2 3 5 6 8 | tgcgrtriv | |
12 | eleq1 | |
|
13 | oveq2 | |
|
14 | 13 | eqeq2d | |
15 | 12 14 | anbi12d | |
16 | 15 | rspcev | |
17 | 8 10 11 16 | syl12anc | |
18 | 1 2 3 4 5 6 6 8 9 | legov | |
19 | 17 18 | mpbird | |