Theorem isoas

Description: Congruence theorem for isocele triangles: if two angles of a triangle are congruent, then the corresponding sides also are. (Contributed by Thierry Arnoux, 5-Oct-2020)

	Ref	Expression
Hypotheses	isoas.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	isoas.m	⊢ − = ( dist ‘ 𝐺 )
	isoas.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	isoas.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	isoas.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	isoas.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
	isoas.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
	isoas.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
	isoas.1	⊢ ( 𝜑 → ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
	isoas.2	⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐵 ”⟩ )
Assertion	isoas	⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = ( 𝐴 − 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		isoas.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		isoas.m	⊢ − = ( dist ‘ 𝐺 )
3		isoas.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		isoas.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
5		isoas.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6		isoas.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
7		isoas.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
8		isoas.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
9		isoas.1	⊢ ( 𝜑 → ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
10		isoas.2	⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐵 ”⟩ )
11		eqid	⊢ ( cgrG ‘ 𝐺 ) = ( cgrG ‘ 𝐺 )
12	1 4 3 5 6 7 8 9	ncolrot1	⊢ ( 𝜑 → ¬ ( 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) )
13	1 2 3 5 7 8	axtgcgrrflx	⊢ ( 𝜑 → ( 𝐵 − 𝐶 ) = ( 𝐶 − 𝐵 ) )
14		eqid	⊢ ( hlG ‘ 𝐺 ) = ( hlG ‘ 𝐺 )
15	1 3 5 14 6 7 8 6 8 7 10	cgracom	⊢ ( 𝜑 → ⟨“ 𝐴 𝐶 𝐵 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ )
16	1 3 2 5 6 8 7 6 7 8 15	cgraswaplr	⊢ ( 𝜑 → ⟨“ 𝐵 𝐶 𝐴 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐶 𝐵 𝐴 ”⟩ )
17	1 2 3 5 7 8 6 8 7 6 4 12 13 16 10	tgasa	⊢ ( 𝜑 → ⟨“ 𝐵 𝐶 𝐴 ”⟩ ( cgrG ‘ 𝐺 ) ⟨“ 𝐶 𝐵 𝐴 ”⟩ )
18	1 2 3 11 5 7 8 6 8 7 6 17	cgr3simp3	⊢ ( 𝜑 → ( 𝐴 − 𝐵 ) = ( 𝐴 − 𝐶 ) )