Metamath Proof Explorer

Theorem iscgrad

Description: Sufficient conditions for angle congruence, deduction version. (Contributed by Thierry Arnoux, 1-Aug-2020)

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

Proof

Step Hyp Ref Expression
1 iscgra.p 
 |-  P = ( Base ` G )
2 iscgra.i 
 |-  I = ( Itv ` G )
3 iscgra.k 
 |-  K = ( hlG ` G )
4 iscgra.g 
 |-  ( ph -> G e. TarskiG )
5 iscgra.a 
 |-  ( ph -> A e. P )
6 iscgra.b 
 |-  ( ph -> B e. P )
7 iscgra.c 
 |-  ( ph -> C e. P )
8 iscgra.d 
 |-  ( ph -> D e. P )
9 iscgra.e 
 |-  ( ph -> E e. P )
10 iscgra.f 
 |-  ( ph -> F e. P )
11 iscgrad.x 
 |-  ( ph -> X e. P )
12 iscgrad.y 
 |-  ( ph -> Y e. P )
13 iscgrad.1 
 |-  ( ph -> <" A B C "> ( cgrG ` G ) <" X E Y "> )
14 iscgrad.2 
 |-  ( ph -> X ( K ` E ) D )
15 iscgrad.3 
 |-  ( ph -> Y ( K ` E ) F )
16 id 
 |-  ( x = X -> x = X )
17 eqidd 
 |-  ( x = X -> E = E )
18 eqidd 
 |-  ( x = X -> y = y )
19 16 17 18 s3eqd 
 |-  ( x = X -> <" x E y "> = <" X E y "> )
20 19 breq2d 
 |-  ( x = X -> ( <" A B C "> ( cgrG ` G ) <" x E y "> <-> <" A B C "> ( cgrG ` G ) <" X E y "> ) )
21 breq1 
 |-  ( x = X -> ( x ( K ` E ) D <-> X ( K ` E ) D ) )
22 20 21 3anbi12d 
 |-  ( x = X -> ( ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) <-> ( <" A B C "> ( cgrG ` G ) <" X E y "> /\ X ( K ` E ) D /\ y ( K ` E ) F ) ) )
23 eqidd 
 |-  ( y = Y -> X = X )
24 eqidd 
 |-  ( y = Y -> E = E )
25 id 
 |-  ( y = Y -> y = Y )
26 23 24 25 s3eqd 
 |-  ( y = Y -> <" X E y "> = <" X E Y "> )
27 26 breq2d 
 |-  ( y = Y -> ( <" A B C "> ( cgrG ` G ) <" X E y "> <-> <" A B C "> ( cgrG ` G ) <" X E Y "> ) )
28 breq1 
 |-  ( y = Y -> ( y ( K ` E ) F <-> Y ( K ` E ) F ) )
29 27 28 3anbi13d 
 |-  ( y = Y -> ( ( <" A B C "> ( cgrG ` G ) <" X E y "> /\ X ( K ` E ) D /\ y ( K ` E ) F ) <-> ( <" A B C "> ( cgrG ` G ) <" X E Y "> /\ X ( K ` E ) D /\ Y ( K ` E ) F ) ) )
30 22 29 rspc2ev 
 |-  ( ( X e. P /\ Y e. P /\ ( <" A B C "> ( cgrG ` G ) <" X E Y "> /\ X ( K ` E ) D /\ Y ( K ` E ) F ) ) -> E. x e. P E. y e. P ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) )
31 11 12 13 14 15 30 syl113anc 
 |-  ( ph -> E. x e. P E. y e. P ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) )
32 1 2 3 4 5 6 7 8 9 10 iscgra 
 |-  ( ph -> ( <" A B C "> ( cgrA ` G ) <" D E F "> <-> E. x e. P E. y e. P ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) )
33 31 32 mpbird 
 |-  ( ph -> <" A B C "> ( cgrA ` G ) <" D E F "> )