Description: GeoCoq l11__30 analogue: leA is preserved when both compared angles are replaced by congruent angles. (Contributed by JAG, 12-Aug-2026)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | leacgra.p | |- P = ( Base ` G ) |
|
| leacgra.i | |- I = ( Itv ` G ) |
||
| leacgra.k | |- K = ( hlG ` G ) |
||
| leacgra.s | |- .<_ = ( leA ` G ) |
||
| leacgra.g | |- ( ph -> G e. TarskiG ) |
||
| leacgra.a | |- ( ph -> A e. P ) |
||
| leacgra.b | |- ( ph -> B e. P ) |
||
| leacgra.c | |- ( ph -> C e. P ) |
||
| leacgra.d | |- ( ph -> D e. P ) |
||
| leacgra.e | |- ( ph -> E e. P ) |
||
| leacgra.f | |- ( ph -> F e. P ) |
||
| leacgra.h | |- ( ph -> H e. P ) |
||
| leacgra.u | |- ( ph -> U e. P ) |
||
| leacgra.j | |- ( ph -> J e. P ) |
||
| leacgra.x | |- ( ph -> X e. P ) |
||
| leacgra.y | |- ( ph -> Y e. P ) |
||
| leacgra.z | |- ( ph -> Z e. P ) |
||
| leacgra.1 | |- ( ph -> <" A B C "> .<_ <" D E F "> ) |
||
| leacgra.2 | |- ( ph -> <" A B C "> ( cgrA ` G ) <" H U J "> ) |
||
| leacgra.3 | |- ( ph -> <" D E F "> ( cgrA ` G ) <" X Y Z "> ) |
||
| Assertion | leacgra | |- ( ph -> <" H U J "> .<_ <" X Y Z "> ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | leacgra.p | |- P = ( Base ` G ) |
|
| 2 | leacgra.i | |- I = ( Itv ` G ) |
|
| 3 | leacgra.k | |- K = ( hlG ` G ) |
|
| 4 | leacgra.s | |- .<_ = ( leA ` G ) |
|
| 5 | leacgra.g | |- ( ph -> G e. TarskiG ) |
|
| 6 | leacgra.a | |- ( ph -> A e. P ) |
|
| 7 | leacgra.b | |- ( ph -> B e. P ) |
|
| 8 | leacgra.c | |- ( ph -> C e. P ) |
|
| 9 | leacgra.d | |- ( ph -> D e. P ) |
|
| 10 | leacgra.e | |- ( ph -> E e. P ) |
|
| 11 | leacgra.f | |- ( ph -> F e. P ) |
|
| 12 | leacgra.h | |- ( ph -> H e. P ) |
|
| 13 | leacgra.u | |- ( ph -> U e. P ) |
|
| 14 | leacgra.j | |- ( ph -> J e. P ) |
|
| 15 | leacgra.x | |- ( ph -> X e. P ) |
|
| 16 | leacgra.y | |- ( ph -> Y e. P ) |
|
| 17 | leacgra.z | |- ( ph -> Z e. P ) |
|
| 18 | leacgra.1 | |- ( ph -> <" A B C "> .<_ <" D E F "> ) |
|
| 19 | leacgra.2 | |- ( ph -> <" A B C "> ( cgrA ` G ) <" H U J "> ) |
|
| 20 | leacgra.3 | |- ( ph -> <" D E F "> ( cgrA ` G ) <" X Y Z "> ) |
|
| 21 | 4 | breqi | |- ( <" A B C "> .<_ <" D E F "> <-> <" A B C "> ( leA ` G ) <" D E F "> ) |
| 22 | 18 21 | sylib | |- ( ph -> <" A B C "> ( leA ` G ) <" D E F "> ) |
| 23 | 1 2 3 5 6 7 8 9 10 11 12 13 14 22 19 | leacgra1 | |- ( ph -> <" H U J "> ( leA ` G ) <" D E F "> ) |
| 24 | 1 2 3 5 12 13 14 9 10 11 15 16 17 23 20 | leacgra2 | |- ( ph -> <" H U J "> ( leA ` G ) <" X Y Z "> ) |
| 25 | 4 | breqi | |- ( <" H U J "> .<_ <" X Y Z "> <-> <" H U J "> ( leA ` G ) <" X Y Z "> ) |
| 26 | 24 25 | sylibr | |- ( ph -> <" H U J "> .<_ <" X Y Z "> ) |