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 𝑃 = ( Base ‘ 𝐺 )
legval.d = ( dist ‘ 𝐺 )
legval.i 𝐼 = ( Itv ‘ 𝐺 )
legval.l = ( ≤G ‘ 𝐺 )
legval.g ( 𝜑𝐺 ∈ TarskiG )
legid.a ( 𝜑𝐴𝑃 )
legid.b ( 𝜑𝐵𝑃 )
legtrd.c ( 𝜑𝐶𝑃 )
legtrd.d ( 𝜑𝐷𝑃 )
Assertion leg0 ( 𝜑 → ( 𝐴 𝐴 ) ( 𝐶 𝐷 ) )

Proof

Step Hyp Ref Expression
1 legval.p 𝑃 = ( Base ‘ 𝐺 )
2 legval.d = ( dist ‘ 𝐺 )
3 legval.i 𝐼 = ( Itv ‘ 𝐺 )
4 legval.l = ( ≤G ‘ 𝐺 )
5 legval.g ( 𝜑𝐺 ∈ TarskiG )
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 ( 𝜑 → ( 𝐴 𝐴 ) ( 𝐶 𝐷 ) )