Metamath Proof Explorer

Theorem mideulem

Description: Lemma for mideu . We can assume mideulem.9 "without loss of generality". (Contributed by Thierry Arnoux, 25-Nov-2019)

Ref Expression
Hypotheses colperpex.p 
|- P = ( Base ` G )
colperpex.d 
|- .- = ( dist ` G )
colperpex.i 
|- I = ( Itv ` G )
colperpex.l 
|- L = ( LineG ` G )
colperpex.g 
|- ( ph -> G e. TarskiG )
mideu.s 
|- S = ( pInvG ` G )
mideu.1 
|- ( ph -> A e. P )
mideu.2 
|- ( ph -> B e. P )
mideulem.1 
|- ( ph -> A =/= B )
mideulem.2 
|- ( ph -> Q e. P )
mideulem.3 
|- ( ph -> O e. P )
mideulem.4 
|- ( ph -> T e. P )
mideulem.5 
|- ( ph -> ( A L B ) ( perpG ` G ) ( Q L B ) )
mideulem.6 
|- ( ph -> ( A L B ) ( perpG ` G ) ( A L O ) )
mideulem.7 
|- ( ph -> T e. ( A L B ) )
mideulem.8 
|- ( ph -> T e. ( Q I O ) )
mideulem.9 
|- ( ph -> ( A .- O ) ( leG ` G ) ( B .- Q ) )
Assertion mideulem 
|- ( ph -> E. x e. P B = ( ( S ` x ) ` A ) )

Proof

Step Hyp Ref Expression
1 colperpex.p 
 |-  P = ( Base ` G )
2 colperpex.d 
 |-  .- = ( dist ` G )
3 colperpex.i 
 |-  I = ( Itv ` G )
4 colperpex.l 
 |-  L = ( LineG ` G )
5 colperpex.g 
 |-  ( ph -> G e. TarskiG )
6 mideu.s 
 |-  S = ( pInvG ` G )
7 mideu.1 
 |-  ( ph -> A e. P )
8 mideu.2 
 |-  ( ph -> B e. P )
9 mideulem.1 
 |-  ( ph -> A =/= B )
10 mideulem.2 
 |-  ( ph -> Q e. P )
11 mideulem.3 
 |-  ( ph -> O e. P )
12 mideulem.4 
 |-  ( ph -> T e. P )
13 mideulem.5 
 |-  ( ph -> ( A L B ) ( perpG ` G ) ( Q L B ) )
14 mideulem.6 
 |-  ( ph -> ( A L B ) ( perpG ` G ) ( A L O ) )
15 mideulem.7 
 |-  ( ph -> T e. ( A L B ) )
16 mideulem.8 
 |-  ( ph -> T e. ( Q I O ) )
17 mideulem.9 
 |-  ( ph -> ( A .- O ) ( leG ` G ) ( B .- Q ) )
18 simprrl 
 |-  ( ( ( ( ph /\ r e. P ) /\ ( r e. ( B I Q ) /\ ( A .- O ) = ( B .- r ) ) ) /\ ( x e. P /\ ( B = ( ( S ` x ) ` A ) /\ O = ( ( S ` x ) ` r ) ) ) ) -> B = ( ( S ` x ) ` A ) )
19 5 ad2antrr 
 |-  ( ( ( ph /\ r e. P ) /\ ( r e. ( B I Q ) /\ ( A .- O ) = ( B .- r ) ) ) -> G e. TarskiG )
20 7 ad2antrr 
 |-  ( ( ( ph /\ r e. P ) /\ ( r e. ( B I Q ) /\ ( A .- O ) = ( B .- r ) ) ) -> A e. P )
21 8 ad2antrr 
 |-  ( ( ( ph /\ r e. P ) /\ ( r e. ( B I Q ) /\ ( A .- O ) = ( B .- r ) ) ) -> B e. P )
22 9 ad2antrr 
 |-  ( ( ( ph /\ r e. P ) /\ ( r e. ( B I Q ) /\ ( A .- O ) = ( B .- r ) ) ) -> A =/= B )
23 10 ad2antrr 
 |-  ( ( ( ph /\ r e. P ) /\ ( r e. ( B I Q ) /\ ( A .- O ) = ( B .- r ) ) ) -> Q e. P )
24 11 ad2antrr 
 |-  ( ( ( ph /\ r e. P ) /\ ( r e. ( B I Q ) /\ ( A .- O ) = ( B .- r ) ) ) -> O e. P )
25 12 ad2antrr 
 |-  ( ( ( ph /\ r e. P ) /\ ( r e. ( B I Q ) /\ ( A .- O ) = ( B .- r ) ) ) -> T e. P )
26 13 ad2antrr 
 |-  ( ( ( ph /\ r e. P ) /\ ( r e. ( B I Q ) /\ ( A .- O ) = ( B .- r ) ) ) -> ( A L B ) ( perpG ` G ) ( Q L B ) )
27 14 ad2antrr 
 |-  ( ( ( ph /\ r e. P ) /\ ( r e. ( B I Q ) /\ ( A .- O ) = ( B .- r ) ) ) -> ( A L B ) ( perpG ` G ) ( A L O ) )
28 15 ad2antrr 
 |-  ( ( ( ph /\ r e. P ) /\ ( r e. ( B I Q ) /\ ( A .- O ) = ( B .- r ) ) ) -> T e. ( A L B ) )
29 16 ad2antrr 
 |-  ( ( ( ph /\ r e. P ) /\ ( r e. ( B I Q ) /\ ( A .- O ) = ( B .- r ) ) ) -> T e. ( Q I O ) )
30 simplr 
 |-  ( ( ( ph /\ r e. P ) /\ ( r e. ( B I Q ) /\ ( A .- O ) = ( B .- r ) ) ) -> r e. P )
31 simprl 
 |-  ( ( ( ph /\ r e. P ) /\ ( r e. ( B I Q ) /\ ( A .- O ) = ( B .- r ) ) ) -> r e. ( B I Q ) )
32 simprr 
 |-  ( ( ( ph /\ r e. P ) /\ ( r e. ( B I Q ) /\ ( A .- O ) = ( B .- r ) ) ) -> ( A .- O ) = ( B .- r ) )
33 1 2 3 4 19 6 20 21 22 23 24 25 26 27 28 29 30 31 32 opphllem 
 |-  ( ( ( ph /\ r e. P ) /\ ( r e. ( B I Q ) /\ ( A .- O ) = ( B .- r ) ) ) -> E. x e. P ( B = ( ( S ` x ) ` A ) /\ O = ( ( S ` x ) ` r ) ) )
34 18 33 reximddv 
 |-  ( ( ( ph /\ r e. P ) /\ ( r e. ( B I Q ) /\ ( A .- O ) = ( B .- r ) ) ) -> E. x e. P B = ( ( S ` x ) ` A ) )
35 eqid 
 |-  ( leG ` G ) = ( leG ` G )
36 1 2 3 35 5 7 11 8 10 legov 
 |-  ( ph -> ( ( A .- O ) ( leG ` G ) ( B .- Q ) <-> E. r e. P ( r e. ( B I Q ) /\ ( A .- O ) = ( B .- r ) ) ) )
37 17 36 mpbid 
 |-  ( ph -> E. r e. P ( r e. ( B I Q ) /\ ( A .- O ) = ( B .- r ) ) )
38 34 37 r19.29a 
 |-  ( ph -> E. x e. P B = ( ( S ` x ) ` A ) )