Theorem ssscongptld

Description: If two triangles have equal sides, one angle in one triangle has the same cosine as the corresponding angle in the other triangle. This is a partial form of the SSS congruence theorem.

This theorem is proven by using lawcos on both triangles to express one side in terms of the other two, and then equating these expressions and reducing this algebraically to get an equality of cosines of angles. (Contributed by David Moews, 28-Feb-2017)

	Ref	Expression
Hypotheses	ssscongptld.angdef	|- F = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) )
	ssscongptld.1	|- ( ph -> A e. CC )
	ssscongptld.2	|- ( ph -> B e. CC )
	ssscongptld.3	|- ( ph -> C e. CC )
	ssscongptld.4	|- ( ph -> D e. CC )
	ssscongptld.5	|- ( ph -> E e. CC )
	ssscongptld.6	|- ( ph -> G e. CC )
	ssscongptld.7	|- ( ph -> A =/= B )
	ssscongptld.8	|- ( ph -> B =/= C )
	ssscongptld.9	|- ( ph -> D =/= E )
	ssscongptld.10	|- ( ph -> E =/= G )
	ssscongptld.11	|- ( ph -> ( abs ` ( A - B ) ) = ( abs ` ( D - E ) ) )
	ssscongptld.12	|- ( ph -> ( abs ` ( B - C ) ) = ( abs ` ( E - G ) ) )
	ssscongptld.13	|- ( ph -> ( abs ` ( C - A ) ) = ( abs ` ( G - D ) ) )
Assertion	ssscongptld	|- ( ph -> ( cos ` ( ( A - B ) F ( C - B ) ) ) = ( cos ` ( ( D - E ) F ( G - E ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ssscongptld.angdef	|- F = ( x e. ( CC \ { 0 } ) , y e. ( CC \ { 0 } ) |-> ( Im ` ( log ` ( y / x ) ) ) )
2		ssscongptld.1	|- ( ph -> A e. CC )
3		ssscongptld.2	|- ( ph -> B e. CC )
4		ssscongptld.3	|- ( ph -> C e. CC )
5		ssscongptld.4	|- ( ph -> D e. CC )
6		ssscongptld.5	|- ( ph -> E e. CC )
7		ssscongptld.6	|- ( ph -> G e. CC )
8		ssscongptld.7	|- ( ph -> A =/= B )
9		ssscongptld.8	|- ( ph -> B =/= C )
10		ssscongptld.9	|- ( ph -> D =/= E )
11		ssscongptld.10	|- ( ph -> E =/= G )
12		ssscongptld.11	|- ( ph -> ( abs ` ( A - B ) ) = ( abs ` ( D - E ) ) )
13		ssscongptld.12	|- ( ph -> ( abs ` ( B - C ) ) = ( abs ` ( E - G ) ) )
14		ssscongptld.13	|- ( ph -> ( abs ` ( C - A ) ) = ( abs ` ( G - D ) ) )
15		negpitopissre	|- ( -u _pi (,] _pi ) C_ RR
16		ax-resscn	|- RR C_ CC
17	15 16	sstri	|- ( -u _pi (,] _pi ) C_ CC
18	2 3	subcld	|- ( ph -> ( A - B ) e. CC )
19	2 3 8	subne0d	|- ( ph -> ( A - B ) =/= 0 )
20	4 3	subcld	|- ( ph -> ( C - B ) e. CC )
21	9	necomd	|- ( ph -> C =/= B )
22	4 3 21	subne0d	|- ( ph -> ( C - B ) =/= 0 )
23	1 18 19 20 22	angcld	|- ( ph -> ( ( A - B ) F ( C - B ) ) e. ( -u _pi (,] _pi ) )
24	17 23	sselid	|- ( ph -> ( ( A - B ) F ( C - B ) ) e. CC )
25	24	coscld	|- ( ph -> ( cos ` ( ( A - B ) F ( C - B ) ) ) e. CC )
26	5 6	subcld	|- ( ph -> ( D - E ) e. CC )
27	5 6 10	subne0d	|- ( ph -> ( D - E ) =/= 0 )
28	7 6	subcld	|- ( ph -> ( G - E ) e. CC )
29	11	necomd	|- ( ph -> G =/= E )
30	7 6 29	subne0d	|- ( ph -> ( G - E ) =/= 0 )
31	1 26 27 28 30	angcld	|- ( ph -> ( ( D - E ) F ( G - E ) ) e. ( -u _pi (,] _pi ) )
32	17 31	sselid	|- ( ph -> ( ( D - E ) F ( G - E ) ) e. CC )
33	32	coscld	|- ( ph -> ( cos ` ( ( D - E ) F ( G - E ) ) ) e. CC )
34	26	abscld	|- ( ph -> ( abs ` ( D - E ) ) e. RR )
35	34	recnd	|- ( ph -> ( abs ` ( D - E ) ) e. CC )
36	28	abscld	|- ( ph -> ( abs ` ( G - E ) ) e. RR )
37	36	recnd	|- ( ph -> ( abs ` ( G - E ) ) e. CC )
38	35 37	mulcld	|- ( ph -> ( ( abs ` ( D - E ) ) x. ( abs ` ( G - E ) ) ) e. CC )
39	26 27	absne0d	|- ( ph -> ( abs ` ( D - E ) ) =/= 0 )
40	28 30	absne0d	|- ( ph -> ( abs ` ( G - E ) ) =/= 0 )
41	35 37 39 40	mulne0d	|- ( ph -> ( ( abs ` ( D - E ) ) x. ( abs ` ( G - E ) ) ) =/= 0 )
42	4 3	abssubd	|- ( ph -> ( abs ` ( C - B ) ) = ( abs ` ( B - C ) ) )
43	7 6	abssubd	|- ( ph -> ( abs ` ( G - E ) ) = ( abs ` ( E - G ) ) )
44	13 42 43	3eqtr4d	|- ( ph -> ( abs ` ( C - B ) ) = ( abs ` ( G - E ) ) )
45	12 44	oveq12d	|- ( ph -> ( ( abs ` ( A - B ) ) x. ( abs ` ( C - B ) ) ) = ( ( abs ` ( D - E ) ) x. ( abs ` ( G - E ) ) ) )
46	45	oveq1d	|- ( ph -> ( ( ( abs ` ( A - B ) ) x. ( abs ` ( C - B ) ) ) x. ( cos ` ( ( A - B ) F ( C - B ) ) ) ) = ( ( ( abs ` ( D - E ) ) x. ( abs ` ( G - E ) ) ) x. ( cos ` ( ( A - B ) F ( C - B ) ) ) ) )
47	12 35	eqeltrd	|- ( ph -> ( abs ` ( A - B ) ) e. CC )
48	44 37	eqeltrd	|- ( ph -> ( abs ` ( C - B ) ) e. CC )
49	47 48	mulcld	|- ( ph -> ( ( abs ` ( A - B ) ) x. ( abs ` ( C - B ) ) ) e. CC )
50	49 25	mulcld	|- ( ph -> ( ( ( abs ` ( A - B ) ) x. ( abs ` ( C - B ) ) ) x. ( cos ` ( ( A - B ) F ( C - B ) ) ) ) e. CC )
51	38 33	mulcld	|- ( ph -> ( ( ( abs ` ( D - E ) ) x. ( abs ` ( G - E ) ) ) x. ( cos ` ( ( D - E ) F ( G - E ) ) ) ) e. CC )
52		2cnd	|- ( ph -> 2 e. CC )
53		2ne0	|- 2 =/= 0
54	53	a1i	|- ( ph -> 2 =/= 0 )
55	35	sqcld	|- ( ph -> ( ( abs ` ( D - E ) ) ^ 2 ) e. CC )
56	37	sqcld	|- ( ph -> ( ( abs ` ( G - E ) ) ^ 2 ) e. CC )
57	55 56	addcld	|- ( ph -> ( ( ( abs ` ( D - E ) ) ^ 2 ) + ( ( abs ` ( G - E ) ) ^ 2 ) ) e. CC )
58	52 50	mulcld	|- ( ph -> ( 2 x. ( ( ( abs ` ( A - B ) ) x. ( abs ` ( C - B ) ) ) x. ( cos ` ( ( A - B ) F ( C - B ) ) ) ) ) e. CC )
59	52 51	mulcld	|- ( ph -> ( 2 x. ( ( ( abs ` ( D - E ) ) x. ( abs ` ( G - E ) ) ) x. ( cos ` ( ( D - E ) F ( G - E ) ) ) ) ) e. CC )
60	12	oveq1d	|- ( ph -> ( ( abs ` ( A - B ) ) ^ 2 ) = ( ( abs ` ( D - E ) ) ^ 2 ) )
61	44	oveq1d	|- ( ph -> ( ( abs ` ( C - B ) ) ^ 2 ) = ( ( abs ` ( G - E ) ) ^ 2 ) )
62	60 61	oveq12d	|- ( ph -> ( ( ( abs ` ( A - B ) ) ^ 2 ) + ( ( abs ` ( C - B ) ) ^ 2 ) ) = ( ( ( abs ` ( D - E ) ) ^ 2 ) + ( ( abs ` ( G - E ) ) ^ 2 ) ) )
63	62	oveq1d	|- ( ph -> ( ( ( ( abs ` ( A - B ) ) ^ 2 ) + ( ( abs ` ( C - B ) ) ^ 2 ) ) - ( 2 x. ( ( ( abs ` ( A - B ) ) x. ( abs ` ( C - B ) ) ) x. ( cos ` ( ( A - B ) F ( C - B ) ) ) ) ) ) = ( ( ( ( abs ` ( D - E ) ) ^ 2 ) + ( ( abs ` ( G - E ) ) ^ 2 ) ) - ( 2 x. ( ( ( abs ` ( A - B ) ) x. ( abs ` ( C - B ) ) ) x. ( cos ` ( ( A - B ) F ( C - B ) ) ) ) ) ) )
64	14	oveq1d	|- ( ph -> ( ( abs ` ( C - A ) ) ^ 2 ) = ( ( abs ` ( G - D ) ) ^ 2 ) )
65		eqid	|- ( abs ` ( A - B ) ) = ( abs ` ( A - B ) )
66		eqid	|- ( abs ` ( C - B ) ) = ( abs ` ( C - B ) )
67		eqid	|- ( abs ` ( C - A ) ) = ( abs ` ( C - A ) )
68		eqid	|- ( ( A - B ) F ( C - B ) ) = ( ( A - B ) F ( C - B ) )
69	1 65 66 67 68	lawcos	|- ( ( ( C e. CC /\ A e. CC /\ B e. CC ) /\ ( C =/= B /\ A =/= B ) ) -> ( ( abs ` ( C - A ) ) ^ 2 ) = ( ( ( ( abs ` ( A - B ) ) ^ 2 ) + ( ( abs ` ( C - B ) ) ^ 2 ) ) - ( 2 x. ( ( ( abs ` ( A - B ) ) x. ( abs ` ( C - B ) ) ) x. ( cos ` ( ( A - B ) F ( C - B ) ) ) ) ) ) )
70	4 2 3 21 8 69	syl32anc	|- ( ph -> ( ( abs ` ( C - A ) ) ^ 2 ) = ( ( ( ( abs ` ( A - B ) ) ^ 2 ) + ( ( abs ` ( C - B ) ) ^ 2 ) ) - ( 2 x. ( ( ( abs ` ( A - B ) ) x. ( abs ` ( C - B ) ) ) x. ( cos ` ( ( A - B ) F ( C - B ) ) ) ) ) ) )
71		eqid	|- ( abs ` ( D - E ) ) = ( abs ` ( D - E ) )
72		eqid	|- ( abs ` ( G - E ) ) = ( abs ` ( G - E ) )
73		eqid	|- ( abs ` ( G - D ) ) = ( abs ` ( G - D ) )
74		eqid	|- ( ( D - E ) F ( G - E ) ) = ( ( D - E ) F ( G - E ) )
75	1 71 72 73 74	lawcos	|- ( ( ( G e. CC /\ D e. CC /\ E e. CC ) /\ ( G =/= E /\ D =/= E ) ) -> ( ( abs ` ( G - D ) ) ^ 2 ) = ( ( ( ( abs ` ( D - E ) ) ^ 2 ) + ( ( abs ` ( G - E ) ) ^ 2 ) ) - ( 2 x. ( ( ( abs ` ( D - E ) ) x. ( abs ` ( G - E ) ) ) x. ( cos ` ( ( D - E ) F ( G - E ) ) ) ) ) ) )
76	7 5 6 29 10 75	syl32anc	|- ( ph -> ( ( abs ` ( G - D ) ) ^ 2 ) = ( ( ( ( abs ` ( D - E ) ) ^ 2 ) + ( ( abs ` ( G - E ) ) ^ 2 ) ) - ( 2 x. ( ( ( abs ` ( D - E ) ) x. ( abs ` ( G - E ) ) ) x. ( cos ` ( ( D - E ) F ( G - E ) ) ) ) ) ) )
77	64 70 76	3eqtr3d	|- ( ph -> ( ( ( ( abs ` ( A - B ) ) ^ 2 ) + ( ( abs ` ( C - B ) ) ^ 2 ) ) - ( 2 x. ( ( ( abs ` ( A - B ) ) x. ( abs ` ( C - B ) ) ) x. ( cos ` ( ( A - B ) F ( C - B ) ) ) ) ) ) = ( ( ( ( abs ` ( D - E ) ) ^ 2 ) + ( ( abs ` ( G - E ) ) ^ 2 ) ) - ( 2 x. ( ( ( abs ` ( D - E ) ) x. ( abs ` ( G - E ) ) ) x. ( cos ` ( ( D - E ) F ( G - E ) ) ) ) ) ) )
78	63 77	eqtr3d	|- ( ph -> ( ( ( ( abs ` ( D - E ) ) ^ 2 ) + ( ( abs ` ( G - E ) ) ^ 2 ) ) - ( 2 x. ( ( ( abs ` ( A - B ) ) x. ( abs ` ( C - B ) ) ) x. ( cos ` ( ( A - B ) F ( C - B ) ) ) ) ) ) = ( ( ( ( abs ` ( D - E ) ) ^ 2 ) + ( ( abs ` ( G - E ) ) ^ 2 ) ) - ( 2 x. ( ( ( abs ` ( D - E ) ) x. ( abs ` ( G - E ) ) ) x. ( cos ` ( ( D - E ) F ( G - E ) ) ) ) ) ) )
79	57 58 59 78	subcand	|- ( ph -> ( 2 x. ( ( ( abs ` ( A - B ) ) x. ( abs ` ( C - B ) ) ) x. ( cos ` ( ( A - B ) F ( C - B ) ) ) ) ) = ( 2 x. ( ( ( abs ` ( D - E ) ) x. ( abs ` ( G - E ) ) ) x. ( cos ` ( ( D - E ) F ( G - E ) ) ) ) ) )
80	50 51 52 54 79	mulcanad	|- ( ph -> ( ( ( abs ` ( A - B ) ) x. ( abs ` ( C - B ) ) ) x. ( cos ` ( ( A - B ) F ( C - B ) ) ) ) = ( ( ( abs ` ( D - E ) ) x. ( abs ` ( G - E ) ) ) x. ( cos ` ( ( D - E ) F ( G - E ) ) ) ) )
81	46 80	eqtr3d	|- ( ph -> ( ( ( abs ` ( D - E ) ) x. ( abs ` ( G - E ) ) ) x. ( cos ` ( ( A - B ) F ( C - B ) ) ) ) = ( ( ( abs ` ( D - E ) ) x. ( abs ` ( G - E ) ) ) x. ( cos ` ( ( D - E ) F ( G - E ) ) ) ) )
82	25 33 38 41 81	mulcanad	|- ( ph -> ( cos ` ( ( A - B ) F ( C - B ) ) ) = ( cos ` ( ( D - E ) F ( G - E ) ) ) )