Metamath Proof Explorer

Theorem ltgseg

Description: The set E denotes the possible values of the congruence. (Contributed by Thierry Arnoux, 15-Dec-2019)

Ref Expression
Hypotheses legval.p 
|- P = ( Base ` G )
legval.d 
|- .- = ( dist ` G )
legval.i 
|- I = ( Itv ` G )
legval.l 
|- .<_ = ( leG ` G )
legval.g 
|- ( ph -> G e. TarskiG )
legso.a 
|- E = ( .- " ( P X. P ) )
legso.f 
|- ( ph -> Fun .- )
ltgseg.p 
|- ( ph -> A e. E )
Assertion ltgseg 
|- ( ph -> E. x e. P E. y e. P A = ( x .- y ) )

Proof

Step Hyp Ref Expression
1 legval.p 
 |-  P = ( Base ` G )
2 legval.d 
 |-  .- = ( dist ` G )
3 legval.i 
 |-  I = ( Itv ` G )
4 legval.l 
 |-  .<_ = ( leG ` G )
5 legval.g 
 |-  ( ph -> G e. TarskiG )
6 legso.a 
 |-  E = ( .- " ( P X. P ) )
7 legso.f 
 |-  ( ph -> Fun .- )
8 ltgseg.p 
 |-  ( ph -> A e. E )
9 simp-4r 
 |-  ( ( ( ( ( ( ph /\ a e. ( P X. P ) ) /\ ( .- ` a ) = A ) /\ x e. P ) /\ y e. P ) /\ a = <. x , y >. ) -> ( .- ` a ) = A )
10 simpr 
 |-  ( ( ( ( ( ( ph /\ a e. ( P X. P ) ) /\ ( .- ` a ) = A ) /\ x e. P ) /\ y e. P ) /\ a = <. x , y >. ) -> a = <. x , y >. )
11 10 fveq2d 
 |-  ( ( ( ( ( ( ph /\ a e. ( P X. P ) ) /\ ( .- ` a ) = A ) /\ x e. P ) /\ y e. P ) /\ a = <. x , y >. ) -> ( .- ` a ) = ( .- ` <. x , y >. ) )
12 9 11 eqtr3d 
 |-  ( ( ( ( ( ( ph /\ a e. ( P X. P ) ) /\ ( .- ` a ) = A ) /\ x e. P ) /\ y e. P ) /\ a = <. x , y >. ) -> A = ( .- ` <. x , y >. ) )
13 df-ov 
 |-  ( x .- y ) = ( .- ` <. x , y >. )
14 12 13 eqtr4di 
 |-  ( ( ( ( ( ( ph /\ a e. ( P X. P ) ) /\ ( .- ` a ) = A ) /\ x e. P ) /\ y e. P ) /\ a = <. x , y >. ) -> A = ( x .- y ) )
15 simplr 
 |-  ( ( ( ph /\ a e. ( P X. P ) ) /\ ( .- ` a ) = A ) -> a e. ( P X. P ) )
16 elxp2 
 |-  ( a e. ( P X. P ) <-> E. x e. P E. y e. P a = <. x , y >. )
17 15 16 sylib 
 |-  ( ( ( ph /\ a e. ( P X. P ) ) /\ ( .- ` a ) = A ) -> E. x e. P E. y e. P a = <. x , y >. )
18 14 17 reximddv2 
 |-  ( ( ( ph /\ a e. ( P X. P ) ) /\ ( .- ` a ) = A ) -> E. x e. P E. y e. P A = ( x .- y ) )
19 8 6 eleqtrdi 
 |-  ( ph -> A e. ( .- " ( P X. P ) ) )
20 fvelima 
 |-  ( ( Fun .- /\ A e. ( .- " ( P X. P ) ) ) -> E. a e. ( P X. P ) ( .- ` a ) = A )
21 7 19 20 syl2anc 
 |-  ( ph -> E. a e. ( P X. P ) ( .- ` a ) = A )
22 18 21 r19.29a 
 |-  ( ph -> E. x e. P E. y e. P A = ( x .- y ) )