Metamath Proof Explorer

Theorem leacgra2

Description: Target-side leA transport: replacing the larger angle by a congruent angle preserves the angle order. Proved from leawittrg and isleag , the witness form of leA . (Contributed by JAG, 12-Aug-2026)

Ref Expression
Hypotheses leacgra2.p 
|- P = ( Base ` G )
leacgra2.i 
|- I = ( Itv ` G )
leacgra2.k 
|- K = ( hlG ` G )
leacgra2.g 
|- ( ph -> G e. TarskiG )
leacgra2.a 
|- ( ph -> A e. P )
leacgra2.b 
|- ( ph -> B e. P )
leacgra2.c 
|- ( ph -> C e. P )
leacgra2.x 
|- ( ph -> X e. P )
leacgra2.y 
|- ( ph -> Y e. P )
leacgra2.z 
|- ( ph -> Z e. P )
leacgra2.d 
|- ( ph -> D e. P )
leacgra2.e 
|- ( ph -> E e. P )
leacgra2.f 
|- ( ph -> F e. P )
leacgra2.1 
|- ( ph -> <" A B C "> ( leA ` G ) <" X Y Z "> )
leacgra2.2 
|- ( ph -> <" X Y Z "> ( cgrA ` G ) <" D E F "> )
Assertion leacgra2 
|- ( ph -> <" A B C "> ( leA ` G ) <" D E F "> )

Proof

Step Hyp Ref Expression
1 leacgra2.p 
 |-  P = ( Base ` G )
2 leacgra2.i 
 |-  I = ( Itv ` G )
3 leacgra2.k 
 |-  K = ( hlG ` G )
4 leacgra2.g 
 |-  ( ph -> G e. TarskiG )
5 leacgra2.a 
 |-  ( ph -> A e. P )
6 leacgra2.b 
 |-  ( ph -> B e. P )
7 leacgra2.c 
 |-  ( ph -> C e. P )
8 leacgra2.x 
 |-  ( ph -> X e. P )
9 leacgra2.y 
 |-  ( ph -> Y e. P )
10 leacgra2.z 
 |-  ( ph -> Z e. P )
11 leacgra2.d 
 |-  ( ph -> D e. P )
12 leacgra2.e 
 |-  ( ph -> E e. P )
13 leacgra2.f 
 |-  ( ph -> F e. P )
14 leacgra2.1 
 |-  ( ph -> <" A B C "> ( leA ` G ) <" X Y Z "> )
15 leacgra2.2 
 |-  ( ph -> <" X Y Z "> ( cgrA ` G ) <" D E F "> )
16 4 adantr 
 |-  ( ( ph /\ w e. P ) -> G e. TarskiG )
17 16 adantr 
 |-  ( ( ( ph /\ w e. P ) /\ ( w ( inA ` G ) <" X Y Z "> /\ <" A B C "> ( cgrA ` G ) <" X Y w "> ) ) -> G e. TarskiG )
18 8 adantr 
 |-  ( ( ph /\ w e. P ) -> X e. P )
19 18 adantr 
 |-  ( ( ( ph /\ w e. P ) /\ ( w ( inA ` G ) <" X Y Z "> /\ <" A B C "> ( cgrA ` G ) <" X Y w "> ) ) -> X e. P )
20 9 adantr 
 |-  ( ( ph /\ w e. P ) -> Y e. P )
21 20 adantr 
 |-  ( ( ( ph /\ w e. P ) /\ ( w ( inA ` G ) <" X Y Z "> /\ <" A B C "> ( cgrA ` G ) <" X Y w "> ) ) -> Y e. P )
22 10 adantr 
 |-  ( ( ph /\ w e. P ) -> Z e. P )
23 22 adantr 
 |-  ( ( ( ph /\ w e. P ) /\ ( w ( inA ` G ) <" X Y Z "> /\ <" A B C "> ( cgrA ` G ) <" X Y w "> ) ) -> Z e. P )
24 11 adantr 
 |-  ( ( ph /\ w e. P ) -> D e. P )
25 24 adantr 
 |-  ( ( ( ph /\ w e. P ) /\ ( w ( inA ` G ) <" X Y Z "> /\ <" A B C "> ( cgrA ` G ) <" X Y w "> ) ) -> D e. P )
26 12 adantr 
 |-  ( ( ph /\ w e. P ) -> E e. P )
27 26 adantr 
 |-  ( ( ( ph /\ w e. P ) /\ ( w ( inA ` G ) <" X Y Z "> /\ <" A B C "> ( cgrA ` G ) <" X Y w "> ) ) -> E e. P )
28 13 adantr 
 |-  ( ( ph /\ w e. P ) -> F e. P )
29 28 adantr 
 |-  ( ( ( ph /\ w e. P ) /\ ( w ( inA ` G ) <" X Y Z "> /\ <" A B C "> ( cgrA ` G ) <" X Y w "> ) ) -> F e. P )
30 5 adantr 
 |-  ( ( ph /\ w e. P ) -> A e. P )
31 30 adantr 
 |-  ( ( ( ph /\ w e. P ) /\ ( w ( inA ` G ) <" X Y Z "> /\ <" A B C "> ( cgrA ` G ) <" X Y w "> ) ) -> A e. P )
32 6 adantr 
 |-  ( ( ph /\ w e. P ) -> B e. P )
33 32 adantr 
 |-  ( ( ( ph /\ w e. P ) /\ ( w ( inA ` G ) <" X Y Z "> /\ <" A B C "> ( cgrA ` G ) <" X Y w "> ) ) -> B e. P )
34 7 adantr 
 |-  ( ( ph /\ w e. P ) -> C e. P )
35 34 adantr 
 |-  ( ( ( ph /\ w e. P ) /\ ( w ( inA ` G ) <" X Y Z "> /\ <" A B C "> ( cgrA ` G ) <" X Y w "> ) ) -> C e. P )
36 simpl 
 |-  ( ( ( ph /\ w e. P ) /\ ( w ( inA ` G ) <" X Y Z "> /\ <" A B C "> ( cgrA ` G ) <" X Y w "> ) ) -> ( ph /\ w e. P ) )
37 36 simprd 
 |-  ( ( ( ph /\ w e. P ) /\ ( w ( inA ` G ) <" X Y Z "> /\ <" A B C "> ( cgrA ` G ) <" X Y w "> ) ) -> w e. P )
38 simpr 
 |-  ( ( ( ph /\ w e. P ) /\ ( w ( inA ` G ) <" X Y Z "> /\ <" A B C "> ( cgrA ` G ) <" X Y w "> ) ) -> ( w ( inA ` G ) <" X Y Z "> /\ <" A B C "> ( cgrA ` G ) <" X Y w "> ) )
39 38 simpld 
 |-  ( ( ( ph /\ w e. P ) /\ ( w ( inA ` G ) <" X Y Z "> /\ <" A B C "> ( cgrA ` G ) <" X Y w "> ) ) -> w ( inA ` G ) <" X Y Z "> )
40 38 simprd 
 |-  ( ( ( ph /\ w e. P ) /\ ( w ( inA ` G ) <" X Y Z "> /\ <" A B C "> ( cgrA ` G ) <" X Y w "> ) ) -> <" A B C "> ( cgrA ` G ) <" X Y w "> )
41 15 adantr 
 |-  ( ( ph /\ w e. P ) -> <" X Y Z "> ( cgrA ` G ) <" D E F "> )
42 41 adantr 
 |-  ( ( ( ph /\ w e. P ) /\ ( w ( inA ` G ) <" X Y Z "> /\ <" A B C "> ( cgrA ` G ) <" X Y w "> ) ) -> <" X Y Z "> ( cgrA ` G ) <" D E F "> )
43 1 2 3 17 19 21 23 25 27 29 31 33 35 37 39 40 42 leawittrg 
 |-  ( ( ( ph /\ w e. P ) /\ ( w ( inA ` G ) <" X Y Z "> /\ <" A B C "> ( cgrA ` G ) <" X Y w "> ) ) -> E. v e. P ( v ( inA ` G ) <" D E F "> /\ <" A B C "> ( cgrA ` G ) <" D E v "> ) )
44 1 4 5 6 7 8 9 10 isleag 
 |-  ( ph -> ( <" A B C "> ( leA ` G ) <" X Y Z "> <-> E. w e. P ( w ( inA ` G ) <" X Y Z "> /\ <" A B C "> ( cgrA ` G ) <" X Y w "> ) ) )
45 14 44 mpbid 
 |-  ( ph -> E. w e. P ( w ( inA ` G ) <" X Y Z "> /\ <" A B C "> ( cgrA ` G ) <" X Y w "> ) )
46 43 45 r19.29a 
 |-  ( ph -> E. v e. P ( v ( inA ` G ) <" D E F "> /\ <" A B C "> ( cgrA ` G ) <" D E v "> ) )
47 1 4 5 6 7 11 12 13 isleag 
 |-  ( ph -> ( <" A B C "> ( leA ` G ) <" D E F "> <-> E. v e. P ( v ( inA ` G ) <" D E F "> /\ <" A B C "> ( cgrA ` G ) <" D E v "> ) ) )
48 46 47 mpbird 
 |-  ( ph -> <" A B C "> ( leA ` G ) <" D E F "> )