Metamath Proof Explorer

Theorem inagswap

Description: Swap the order of the half lines delimiting the angle. Theorem 11.24 of Schwabhauser p. 101. (Contributed by Thierry Arnoux, 15-Aug-2020)

Ref Expression
Hypotheses isinag.p 
|- P = ( Base ` G )
isinag.i 
|- I = ( Itv ` G )
isinag.k 
|- K = ( hlG ` G )
isinag.x 
|- ( ph -> X e. P )
isinag.a 
|- ( ph -> A e. P )
isinag.b 
|- ( ph -> B e. P )
isinag.c 
|- ( ph -> C e. P )
inagflat.g 
|- ( ph -> G e. TarskiG )
inagswap.1 
|- ( ph -> X ( inA ` G ) <" A B C "> )
Assertion inagswap 
|- ( ph -> X ( inA ` G ) <" C B A "> )

Proof

Step Hyp Ref Expression
1 isinag.p 
 |-  P = ( Base ` G )
2 isinag.i 
 |-  I = ( Itv ` G )
3 isinag.k 
 |-  K = ( hlG ` G )
4 isinag.x 
 |-  ( ph -> X e. P )
5 isinag.a 
 |-  ( ph -> A e. P )
6 isinag.b 
 |-  ( ph -> B e. P )
7 isinag.c 
 |-  ( ph -> C e. P )
8 inagflat.g 
 |-  ( ph -> G e. TarskiG )
9 inagswap.1 
 |-  ( ph -> X ( inA ` G ) <" A B C "> )
10 1 2 3 4 5 6 7 8 isinag 
 |-  ( ph -> ( X ( inA ` G ) <" A B C "> <-> ( ( A =/= B /\ C =/= B /\ X =/= B ) /\ E. x e. P ( x e. ( A I C ) /\ ( x = B \/ x ( K ` B ) X ) ) ) ) )
11 9 10 mpbid 
 |-  ( ph -> ( ( A =/= B /\ C =/= B /\ X =/= B ) /\ E. x e. P ( x e. ( A I C ) /\ ( x = B \/ x ( K ` B ) X ) ) ) )
12 11 simpld 
 |-  ( ph -> ( A =/= B /\ C =/= B /\ X =/= B ) )
13 12 simp2d 
 |-  ( ph -> C =/= B )
14 12 simp1d 
 |-  ( ph -> A =/= B )
15 12 simp3d 
 |-  ( ph -> X =/= B )
16 13 14 15 3jca 
 |-  ( ph -> ( C =/= B /\ A =/= B /\ X =/= B ) )
17 11 simprd 
 |-  ( ph -> E. x e. P ( x e. ( A I C ) /\ ( x = B \/ x ( K ` B ) X ) ) )
18 eqid 
 |-  ( dist ` G ) = ( dist ` G )
19 8 3ad2ant1 
 |-  ( ( ph /\ x e. P /\ x e. ( A I C ) ) -> G e. TarskiG )
20 5 3ad2ant1 
 |-  ( ( ph /\ x e. P /\ x e. ( A I C ) ) -> A e. P )
21 simp2 
 |-  ( ( ph /\ x e. P /\ x e. ( A I C ) ) -> x e. P )
22 7 3ad2ant1 
 |-  ( ( ph /\ x e. P /\ x e. ( A I C ) ) -> C e. P )
23 simp3 
 |-  ( ( ph /\ x e. P /\ x e. ( A I C ) ) -> x e. ( A I C ) )
24 1 18 2 19 20 21 22 23 tgbtwncom 
 |-  ( ( ph /\ x e. P /\ x e. ( A I C ) ) -> x e. ( C I A ) )
25 24 3expia 
 |-  ( ( ph /\ x e. P ) -> ( x e. ( A I C ) -> x e. ( C I A ) ) )
26 25 anim1d 
 |-  ( ( ph /\ x e. P ) -> ( ( x e. ( A I C ) /\ ( x = B \/ x ( K ` B ) X ) ) -> ( x e. ( C I A ) /\ ( x = B \/ x ( K ` B ) X ) ) ) )
27 26 reximdva 
 |-  ( ph -> ( E. x e. P ( x e. ( A I C ) /\ ( x = B \/ x ( K ` B ) X ) ) -> E. x e. P ( x e. ( C I A ) /\ ( x = B \/ x ( K ` B ) X ) ) ) )
28 17 27 mpd 
 |-  ( ph -> E. x e. P ( x e. ( C I A ) /\ ( x = B \/ x ( K ` B ) X ) ) )
29 1 2 3 4 7 6 5 8 isinag 
 |-  ( ph -> ( X ( inA ` G ) <" C B A "> <-> ( ( C =/= B /\ A =/= B /\ X =/= B ) /\ E. x e. P ( x e. ( C I A ) /\ ( x = B \/ x ( K ` B ) X ) ) ) ) )
30 16 28 29 mpbir2and 
 |-  ( ph -> X ( inA ` G ) <" C B A "> )