Theorem tgsas1

Description: First congruence theorem: SAS (Side-Angle-Side): If two pairs of sides of two triangles are equal in length, and the included angles are equal in measurement, then third sides are equal in length. Theorem 11.49 of Schwabhauser p. 107. (Contributed by Thierry Arnoux, 1-Aug-2020)

	Ref	Expression
Hypotheses	tgsas.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	tgsas.m	⊢ − = ( dist ‘ 𝐺 )
	tgsas.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	tgsas.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	tgsas.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
	tgsas.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
	tgsas.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
	tgsas.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
	tgsas.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
	tgsas.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
	tgsas.1	⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = ( 𝐷 − 𝐸 ) )
	tgsas.2	⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
	tgsas.3	⊢ ( 𝜑 → ( 𝐵 − 𝐶 ) = ( 𝐸 − 𝐹 ) )
Assertion	tgsas1	⊢ ( 𝜑 → ( 𝐶 − 𝐴 ) = ( 𝐹 − 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		tgsas.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		tgsas.m	⊢ − = ( dist ‘ 𝐺 )
3		tgsas.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		tgsas.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5		tgsas.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
6		tgsas.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
7		tgsas.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
8		tgsas.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
9		tgsas.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
10		tgsas.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
11		tgsas.1	⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = ( 𝐷 − 𝐸 ) )
12		tgsas.2	⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
13		tgsas.3	⊢ ( 𝜑 → ( 𝐵 − 𝐶 ) = ( 𝐸 − 𝐹 ) )
14		eqid	⊢ ( hlG ‘ 𝐺 ) = ( hlG ‘ 𝐺 )
15	1 3 14 4 5 6 7 8 9 10 12	cgrane1	⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
16	1 3 14 5 5 6 4 15	hlid	⊢ ( 𝜑 → 𝐴 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐴 )
17	1 3 14 4 5 6 7 8 9 10 12	cgrane2	⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
18	17	necomd	⊢ ( 𝜑 → 𝐶 ≠ 𝐵 )
19	1 3 14 7 5 6 4 18	hlid	⊢ ( 𝜑 → 𝐶 ( ( hlG ‘ 𝐺 ) ‘ 𝐵 ) 𝐶 )
20	1 2 3 4 5 6 8 9 11	tgcgrcomlr	⊢ ( 𝜑 → ( 𝐵 − 𝐴 ) = ( 𝐸 − 𝐷 ) )
21	1 3 14 4 5 6 7 8 9 10 12 5 2 7 16 19 20 13	cgracgr	⊢ ( 𝜑 → ( 𝐴 − 𝐶 ) = ( 𝐷 − 𝐹 ) )
22	1 2 3 4 5 7 8 10 21	tgcgrcomlr	⊢ ( 𝜑 → ( 𝐶 − 𝐴 ) = ( 𝐹 − 𝐷 ) )