Metamath Proof Explorer


Theorem leg0

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 P=BaseG
legval.d -˙=distG
legval.i I=ItvG
legval.l ˙=𝒢G
legval.g φG𝒢Tarski
legid.a φAP
legid.b φBP
legtrd.c φCP
legtrd.d φDP
Assertion leg0 φA-˙A˙C-˙D

Proof

Step Hyp Ref Expression
1 legval.p P=BaseG
2 legval.d -˙=distG
3 legval.i I=ItvG
4 legval.l ˙=𝒢G
5 legval.g φG𝒢Tarski
6 legid.a φAP
7 legid.b φBP
8 legtrd.c φCP
9 legtrd.d φDP
10 1 2 3 5 8 9 tgbtwntriv1 φCCID
11 1 2 3 5 6 8 tgcgrtriv φA-˙A=C-˙C
12 eleq1 x=CxCIDCCID
13 oveq2 x=CC-˙x=C-˙C
14 13 eqeq2d x=CA-˙A=C-˙xA-˙A=C-˙C
15 12 14 anbi12d x=CxCIDA-˙A=C-˙xCCIDA-˙A=C-˙C
16 15 rspcev CPCCIDA-˙A=C-˙CxPxCIDA-˙A=C-˙x
17 8 10 11 16 syl12anc φxPxCIDA-˙A=C-˙x
18 1 2 3 4 5 6 6 8 9 legov φA-˙A˙C-˙DxPxCIDA-˙A=C-˙x
19 17 18 mpbird φA-˙A˙C-˙D