Metamath Proof Explorer

Theorem iscgra1

Description: A special version of iscgra where one distance is known to be equal. In this case, angle congruence can be written with only one quantifier. (Contributed by Thierry Arnoux, 9-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 )
iscgra1.m 
|- .- = ( dist ` G )
iscgra1.1 
|- ( ph -> A =/= B )
iscgra1.2 
|- ( ph -> ( A .- B ) = ( D .- E ) )
Assertion iscgra1 
|- ( ph -> ( <" A B C "> ( cgrA ` G ) <" D E F "> <-> E. x e. P ( <" A B C "> ( cgrG ` G ) <" D E x "> /\ x ( K ` 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 iscgra1.m 
 |-  .- = ( dist ` G )
12 iscgra1.1 
 |-  ( ph -> A =/= B )
13 iscgra1.2 
 |-  ( ph -> ( A .- B ) = ( D .- E ) )
14 1 2 3 4 5 6 7 8 9 10 iscgra 
 |-  ( ph -> ( <" A B C "> ( cgrA ` G ) <" D E F "> <-> E. y e. P E. x e. P ( <" A B C "> ( cgrG ` G ) <" y E x "> /\ y ( K ` E ) D /\ x ( K ` E ) F ) ) )
15 9 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. P ) /\ x e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" y E x "> /\ y ( K ` E ) D /\ x ( K ` E ) F ) ) -> E e. P )
16 6 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. P ) /\ x e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" y E x "> /\ y ( K ` E ) D /\ x ( K ` E ) F ) ) -> B e. P )
17 5 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. P ) /\ x e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" y E x "> /\ y ( K ` E ) D /\ x ( K ` E ) F ) ) -> A e. P )
18 4 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. P ) /\ x e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" y E x "> /\ y ( K ` E ) D /\ x ( K ` E ) F ) ) -> G e. TarskiG )
19 8 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. P ) /\ x e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" y E x "> /\ y ( K ` E ) D /\ x ( K ` E ) F ) ) -> D e. P )
20 simpllr 
 |-  ( ( ( ( ph /\ y e. P ) /\ x e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" y E x "> /\ y ( K ` E ) D /\ x ( K ` E ) F ) ) -> y e. P )
21 simpr2 
 |-  ( ( ( ( ph /\ y e. P ) /\ x e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" y E x "> /\ y ( K ` E ) D /\ x ( K ` E ) F ) ) -> y ( K ` E ) D )
22 1 2 3 20 19 15 18 21 hlne2 
 |-  ( ( ( ( ph /\ y e. P ) /\ x e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" y E x "> /\ y ( K ` E ) D /\ x ( K ` E ) F ) ) -> D =/= E )
23 12 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. P ) /\ x e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" y E x "> /\ y ( K ` E ) D /\ x ( K ` E ) F ) ) -> A =/= B )
24 23 necomd 
 |-  ( ( ( ( ph /\ y e. P ) /\ x e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" y E x "> /\ y ( K ` E ) D /\ x ( K ` E ) F ) ) -> B =/= A )
25 1 2 3 19 15 15 18 22 hlid 
 |-  ( ( ( ( ph /\ y e. P ) /\ x e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" y E x "> /\ y ( K ` E ) D /\ x ( K ` E ) F ) ) -> D ( K ` E ) D )
26 eqid 
 |-  ( cgrG ` G ) = ( cgrG ` G )
27 7 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. P ) /\ x e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" y E x "> /\ y ( K ` E ) D /\ x ( K ` E ) F ) ) -> C e. P )
28 simplr 
 |-  ( ( ( ( ph /\ y e. P ) /\ x e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" y E x "> /\ y ( K ` E ) D /\ x ( K ` E ) F ) ) -> x e. P )
29 simpr1 
 |-  ( ( ( ( ph /\ y e. P ) /\ x e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" y E x "> /\ y ( K ` E ) D /\ x ( K ` E ) F ) ) -> <" A B C "> ( cgrG ` G ) <" y E x "> )
30 1 11 2 26 18 17 16 27 20 15 28 29 cgr3simp1 
 |-  ( ( ( ( ph /\ y e. P ) /\ x e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" y E x "> /\ y ( K ` E ) D /\ x ( K ` E ) F ) ) -> ( A .- B ) = ( y .- E ) )
31 30 eqcomd 
 |-  ( ( ( ( ph /\ y e. P ) /\ x e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" y E x "> /\ y ( K ` E ) D /\ x ( K ` E ) F ) ) -> ( y .- E ) = ( A .- B ) )
32 1 11 2 18 20 15 17 16 31 tgcgrcomlr 
 |-  ( ( ( ( ph /\ y e. P ) /\ x e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" y E x "> /\ y ( K ` E ) D /\ x ( K ` E ) F ) ) -> ( E .- y ) = ( B .- A ) )
33 13 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. P ) /\ x e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" y E x "> /\ y ( K ` E ) D /\ x ( K ` E ) F ) ) -> ( A .- B ) = ( D .- E ) )
34 33 eqcomd 
 |-  ( ( ( ( ph /\ y e. P ) /\ x e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" y E x "> /\ y ( K ` E ) D /\ x ( K ` E ) F ) ) -> ( D .- E ) = ( A .- B ) )
35 1 11 2 18 19 15 17 16 34 tgcgrcomlr 
 |-  ( ( ( ( ph /\ y e. P ) /\ x e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" y E x "> /\ y ( K ` E ) D /\ x ( K ` E ) F ) ) -> ( E .- D ) = ( B .- A ) )
36 1 2 3 15 16 17 18 19 11 22 24 20 19 21 25 32 35 hlcgreulem 
 |-  ( ( ( ( ph /\ y e. P ) /\ x e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" y E x "> /\ y ( K ` E ) D /\ x ( K ` E ) F ) ) -> y = D )
37 simpr3 
 |-  ( ( ( ( ph /\ y e. P ) /\ x e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" y E x "> /\ y ( K ` E ) D /\ x ( K ` E ) F ) ) -> x ( K ` E ) F )
38 36 29 37 jca32 
 |-  ( ( ( ( ph /\ y e. P ) /\ x e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" y E x "> /\ y ( K ` E ) D /\ x ( K ` E ) F ) ) -> ( y = D /\ ( <" A B C "> ( cgrG ` G ) <" y E x "> /\ x ( K ` E ) F ) ) )
39 simprrl 
 |-  ( ( ( ( ph /\ y e. P ) /\ x e. P ) /\ ( y = D /\ ( <" A B C "> ( cgrG ` G ) <" y E x "> /\ x ( K ` E ) F ) ) ) -> <" A B C "> ( cgrG ` G ) <" y E x "> )
40 simprl 
 |-  ( ( ( ( ph /\ y e. P ) /\ x e. P ) /\ ( y = D /\ ( <" A B C "> ( cgrG ` G ) <" y E x "> /\ x ( K ` E ) F ) ) ) -> y = D )
41 8 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. P ) /\ x e. P ) /\ ( y = D /\ ( <" A B C "> ( cgrG ` G ) <" y E x "> /\ x ( K ` E ) F ) ) ) -> D e. P )
42 9 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. P ) /\ x e. P ) /\ ( y = D /\ ( <" A B C "> ( cgrG ` G ) <" y E x "> /\ x ( K ` E ) F ) ) ) -> E e. P )
43 4 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. P ) /\ x e. P ) /\ ( y = D /\ ( <" A B C "> ( cgrG ` G ) <" y E x "> /\ x ( K ` E ) F ) ) ) -> G e. TarskiG )
44 1 11 2 4 5 6 8 9 13 12 tgcgrneq 
 |-  ( ph -> D =/= E )
45 44 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. P ) /\ x e. P ) /\ ( y = D /\ ( <" A B C "> ( cgrG ` G ) <" y E x "> /\ x ( K ` E ) F ) ) ) -> D =/= E )
46 1 2 3 41 41 42 43 45 hlid 
 |-  ( ( ( ( ph /\ y e. P ) /\ x e. P ) /\ ( y = D /\ ( <" A B C "> ( cgrG ` G ) <" y E x "> /\ x ( K ` E ) F ) ) ) -> D ( K ` E ) D )
47 40 46 eqbrtrd 
 |-  ( ( ( ( ph /\ y e. P ) /\ x e. P ) /\ ( y = D /\ ( <" A B C "> ( cgrG ` G ) <" y E x "> /\ x ( K ` E ) F ) ) ) -> y ( K ` E ) D )
48 simprrr 
 |-  ( ( ( ( ph /\ y e. P ) /\ x e. P ) /\ ( y = D /\ ( <" A B C "> ( cgrG ` G ) <" y E x "> /\ x ( K ` E ) F ) ) ) -> x ( K ` E ) F )
49 39 47 48 3jca 
 |-  ( ( ( ( ph /\ y e. P ) /\ x e. P ) /\ ( y = D /\ ( <" A B C "> ( cgrG ` G ) <" y E x "> /\ x ( K ` E ) F ) ) ) -> ( <" A B C "> ( cgrG ` G ) <" y E x "> /\ y ( K ` E ) D /\ x ( K ` E ) F ) )
50 38 49 impbida 
 |-  ( ( ( ph /\ y e. P ) /\ x e. P ) -> ( ( <" A B C "> ( cgrG ` G ) <" y E x "> /\ y ( K ` E ) D /\ x ( K ` E ) F ) <-> ( y = D /\ ( <" A B C "> ( cgrG ` G ) <" y E x "> /\ x ( K ` E ) F ) ) ) )
51 50 rexbidva 
 |-  ( ( ph /\ y e. P ) -> ( E. x e. P ( <" A B C "> ( cgrG ` G ) <" y E x "> /\ y ( K ` E ) D /\ x ( K ` E ) F ) <-> E. x e. P ( y = D /\ ( <" A B C "> ( cgrG ` G ) <" y E x "> /\ x ( K ` E ) F ) ) ) )
52 r19.42v 
 |-  ( E. x e. P ( y = D /\ ( <" A B C "> ( cgrG ` G ) <" y E x "> /\ x ( K ` E ) F ) ) <-> ( y = D /\ E. x e. P ( <" A B C "> ( cgrG ` G ) <" y E x "> /\ x ( K ` E ) F ) ) )
53 51 52 bitrdi 
 |-  ( ( ph /\ y e. P ) -> ( E. x e. P ( <" A B C "> ( cgrG ` G ) <" y E x "> /\ y ( K ` E ) D /\ x ( K ` E ) F ) <-> ( y = D /\ E. x e. P ( <" A B C "> ( cgrG ` G ) <" y E x "> /\ x ( K ` E ) F ) ) ) )
54 53 rexbidva 
 |-  ( ph -> ( E. y e. P E. x e. P ( <" A B C "> ( cgrG ` G ) <" y E x "> /\ y ( K ` E ) D /\ x ( K ` E ) F ) <-> E. y e. P ( y = D /\ E. x e. P ( <" A B C "> ( cgrG ` G ) <" y E x "> /\ x ( K ` E ) F ) ) ) )
55 id 
 |-  ( y = D -> y = D )
56 eqidd 
 |-  ( y = D -> E = E )
57 eqidd 
 |-  ( y = D -> x = x )
58 55 56 57 s3eqd 
 |-  ( y = D -> <" y E x "> = <" D E x "> )
59 58 breq2d 
 |-  ( y = D -> ( <" A B C "> ( cgrG ` G ) <" y E x "> <-> <" A B C "> ( cgrG ` G ) <" D E x "> ) )
60 59 anbi1d 
 |-  ( y = D -> ( ( <" A B C "> ( cgrG ` G ) <" y E x "> /\ x ( K ` E ) F ) <-> ( <" A B C "> ( cgrG ` G ) <" D E x "> /\ x ( K ` E ) F ) ) )
61 60 rexbidv 
 |-  ( y = D -> ( E. x e. P ( <" A B C "> ( cgrG ` G ) <" y E x "> /\ x ( K ` E ) F ) <-> E. x e. P ( <" A B C "> ( cgrG ` G ) <" D E x "> /\ x ( K ` E ) F ) ) )
62 61 ceqsrexv 
 |-  ( D e. P -> ( E. y e. P ( y = D /\ E. x e. P ( <" A B C "> ( cgrG ` G ) <" y E x "> /\ x ( K ` E ) F ) ) <-> E. x e. P ( <" A B C "> ( cgrG ` G ) <" D E x "> /\ x ( K ` E ) F ) ) )
63 8 62 syl 
 |-  ( ph -> ( E. y e. P ( y = D /\ E. x e. P ( <" A B C "> ( cgrG ` G ) <" y E x "> /\ x ( K ` E ) F ) ) <-> E. x e. P ( <" A B C "> ( cgrG ` G ) <" D E x "> /\ x ( K ` E ) F ) ) )
64 14 54 63 3bitrd 
 |-  ( ph -> ( <" A B C "> ( cgrA ` G ) <" D E F "> <-> E. x e. P ( <" A B C "> ( cgrG ` G ) <" D E x "> /\ x ( K ` E ) F ) ) )