Metamath Proof Explorer

Theorem leacgra1

Description: Source-side leA transport: replacing the smaller angle by a congruent angle preserves the angle order. The counterpart of leacgra2 , proved directly from the witness form of leA ( isleag , isleagd ). (Contributed by JAG, 12-Aug-2026)

Ref Expression
Hypotheses leacgra1.p 
|- P = ( Base ` G )
leacgra1.i 
|- I = ( Itv ` G )
leacgra1.k 
|- K = ( hlG ` G )
leacgra1.g 
|- ( ph -> G e. TarskiG )
leacgra1.a 
|- ( ph -> A e. P )
leacgra1.b 
|- ( ph -> B e. P )
leacgra1.c 
|- ( ph -> C e. P )
leacgra1.d 
|- ( ph -> D e. P )
leacgra1.e 
|- ( ph -> E e. P )
leacgra1.f 
|- ( ph -> F e. P )
leacgra1.h 
|- ( ph -> H e. P )
leacgra1.u 
|- ( ph -> U e. P )
leacgra1.j 
|- ( ph -> J e. P )
leacgra1.1 
|- ( ph -> <" A B C "> ( leA ` G ) <" D E F "> )
leacgra1.2 
|- ( ph -> <" A B C "> ( cgrA ` G ) <" H U J "> )
Assertion leacgra1 
|- ( ph -> <" H U J "> ( leA ` G ) <" D E F "> )

Proof

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