Theorem tgsas2

Description: First congruence theorem: SAS. 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	⊢ ( 𝜑 → ( 𝐵 − 𝐶 ) = ( 𝐸 − 𝐹 ) )
	tgsas2.4	⊢ ( 𝜑 → 𝐴 ≠ 𝐶 )
Assertion	tgsas2	⊢ ( 𝜑 → ⟨“ 𝐶 𝐴 𝐵 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐹 𝐷 𝐸 ”⟩ )

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		tgsas2.4	⊢ ( 𝜑 → 𝐴 ≠ 𝐶 )
15		eqid	⊢ ( hlG ‘ 𝐺 ) = ( hlG ‘ 𝐺 )
16		eqid	⊢ ( cgrG ‘ 𝐺 ) = ( cgrG ‘ 𝐺 )
17	1 2 3 4 5 6 7 8 9 10 11 12 13	tgsas	⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
18	1 2 3 16 4 5 6 7 8 9 10 17	cgr3rotr	⊢ ( 𝜑 → ⟨“ 𝐶 𝐴 𝐵 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐹 𝐷 𝐸 ”⟩ )
19	1 2 3 4 5 6 7 8 9 10 11 12 13	tgsas1	⊢ ( 𝜑 → ( 𝐶 − 𝐴 ) = ( 𝐹 − 𝐷 ) )
20	14	necomd	⊢ ( 𝜑 → 𝐶 ≠ 𝐴 )
21	1 2 3 4 7 5 10 8 19 20	tgcgrneq	⊢ ( 𝜑 → 𝐹 ≠ 𝐷 )
22	1 3 15 10 5 8 4 21	hlid	⊢ ( 𝜑 → 𝐹 ( ( hlG ‘ 𝐺 ) ‘ 𝐷 ) 𝐹 )
23	1 3 15 4 5 6 7 8 9 10 12	cgrane3	⊢ ( 𝜑 → 𝐸 ≠ 𝐷 )
24	1 3 15 9 5 8 4 23	hlid	⊢ ( 𝜑 → 𝐸 ( ( hlG ‘ 𝐺 ) ‘ 𝐷 ) 𝐸 )
25	1 3 15 4 7 5 6 10 8 9 10 9 18 22 24	iscgrad	⊢ ( 𝜑 → ⟨“ 𝐶 𝐴 𝐵 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐹 𝐷 𝐸 ”⟩ )