Metamath Proof Explorer

Theorem iscgrag

Description: Ray normalization: an angle congruence yields two points on the target rays carrying a full triangle congruence, together with the two arm lengths. This is the forward direction of iscgra (Schwabhauser 11.3) repackaged -- nothing is constructed; the distances are read off the cgrG with cgr3simp1 and cgr3simp2 . No non-degeneracy hypothesis is needed or wanted: cgrA carries vertex distinctness intrinsically ( cgrane1 through cgrane4 ), and an extra hypothesis would obstruct the degenerate branches. (Contributed by JAG, 12-Aug-2026)

Ref Expression
Hypotheses iscgrag.p 
|- P = ( Base ` G )
iscgrag.i 
|- I = ( Itv ` G )
iscgrag.k 
|- K = ( hlG ` G )
iscgrag.m 
|- .- = ( dist ` G )
iscgrag.g 
|- ( ph -> G e. TarskiG )
iscgrag.a 
|- ( ph -> A e. P )
iscgrag.b 
|- ( ph -> B e. P )
iscgrag.c 
|- ( ph -> C e. P )
iscgrag.d 
|- ( ph -> D e. P )
iscgrag.e 
|- ( ph -> E e. P )
iscgrag.f 
|- ( ph -> F e. P )
iscgrag.1 
|- ( ph -> <" A B C "> ( cgrA ` G ) <" D E F "> )
Assertion iscgrag 
|- ( 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 ) /\ ( ( E .- x ) = ( B .- A ) /\ ( E .- y ) = ( B .- C ) ) ) )

Proof

Step Hyp Ref Expression
1 iscgrag.p 
 |-  P = ( Base ` G )
2 iscgrag.i 
 |-  I = ( Itv ` G )
3 iscgrag.k 
 |-  K = ( hlG ` G )
4 iscgrag.m 
 |-  .- = ( dist ` G )
5 iscgrag.g 
 |-  ( ph -> G e. TarskiG )
6 iscgrag.a 
 |-  ( ph -> A e. P )
7 iscgrag.b 
 |-  ( ph -> B e. P )
8 iscgrag.c 
 |-  ( ph -> C e. P )
9 iscgrag.d 
 |-  ( ph -> D e. P )
10 iscgrag.e 
 |-  ( ph -> E e. P )
11 iscgrag.f 
 |-  ( ph -> F e. P )
12 iscgrag.1 
 |-  ( ph -> <" A B C "> ( cgrA ` G ) <" D E F "> )
13 simpr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" 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 ) )
14 simpll 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> ( ph /\ x e. P ) )
15 14 simpld 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> ph )
16 15 5 syl 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> G e. TarskiG )
17 15 6 syl 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> A e. P )
18 15 7 syl 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> B e. P )
19 14 simprd 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> x e. P )
20 15 10 syl 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> E e. P )
21 eqid 
 |-  ( cgrG ` G ) = ( cgrG ` G )
22 15 8 syl 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> C e. P )
23 simplr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> y e. P )
24 13 simp1d 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> <" A B C "> ( cgrG ` G ) <" x E y "> )
25 1 4 2 21 16 17 18 22 19 20 23 24 cgr3simp1 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> ( A .- B ) = ( x .- E ) )
26 1 4 2 16 17 18 19 20 25 tgcgrcomlr 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> ( B .- A ) = ( E .- x ) )
27 26 eqcomd 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> ( E .- x ) = ( B .- A ) )
28 1 4 2 21 16 17 18 22 19 20 23 24 cgr3simp2 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> ( B .- C ) = ( E .- y ) )
29 28 eqcomd 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> ( E .- y ) = ( B .- C ) )
30 27 29 jca 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> ( ( E .- x ) = ( B .- A ) /\ ( E .- y ) = ( B .- C ) ) )
31 13 30 jca 
 |-  ( ( ( ( ph /\ x e. P ) /\ y e. P ) /\ ( <" 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 ) /\ ( ( E .- x ) = ( B .- A ) /\ ( E .- y ) = ( B .- C ) ) ) )
32 31 ex 
 |-  ( ( ( ph /\ x e. P ) /\ y e. P ) -> ( ( <" 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 ) /\ ( ( E .- x ) = ( B .- A ) /\ ( E .- y ) = ( B .- C ) ) ) ) )
33 32 reximdva 
 |-  ( ( ph /\ x e. P ) -> ( E. y e. P ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) -> E. y e. P ( ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) /\ ( ( E .- x ) = ( B .- A ) /\ ( E .- y ) = ( B .- C ) ) ) ) )
34 33 imp 
 |-  ( ( ( ph /\ x e. P ) /\ E. y e. P ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) ) -> E. y e. P ( ( <" A B C "> ( cgrG ` G ) <" x E y "> /\ x ( K ` E ) D /\ y ( K ` E ) F ) /\ ( ( E .- x ) = ( B .- A ) /\ ( E .- y ) = ( B .- C ) ) ) )
35 1 2 3 5 6 7 8 9 10 11 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 ) ) )
36 12 35 mpbid 
 |-  ( 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 ) )
37 34 36 reximddv3 
 |-  ( 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 ) /\ ( ( E .- x ) = ( B .- A ) /\ ( E .- y ) = ( B .- C ) ) ) )