Theorem cgraid

Description: Angle congruence is reflexive. Theorem 11.6 of Schwabhauser p. 96. (Contributed by Thierry Arnoux, 31-Jul-2020)

	Ref	Expression
Hypotheses	cgraid.p	$$⊢P={\mathrm{Base}}_G$$
	cgraid.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
	cgraid.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	cgraid.k	$$⊢K={hl}_{𝒢}\left(G\right)$$
	cgraid.a	$$⊢\phi \to A\in P$$
	cgraid.b	$$⊢\phi \to B\in P$$
	cgraid.c	$$⊢\phi \to C\in P$$
	cgraid.1	$$⊢\phi \to A\ne B$$
	cgraid.2	$$⊢\phi \to B\ne C$$
Assertion	cgraid	$$⊢\phi \to ⟨“ABC”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“ABC”⟩$$

Proof

Step	Hyp	Ref	Expression
1		cgraid.p	$$⊢P={\mathrm{Base}}_G$$
2		cgraid.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
3		cgraid.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
4		cgraid.k	$$⊢K={hl}_{𝒢}\left(G\right)$$
5		cgraid.a	$$⊢\phi \to A\in P$$
6		cgraid.b	$$⊢\phi \to B\in P$$
7		cgraid.c	$$⊢\phi \to C\in P$$
8		cgraid.1	$$⊢\phi \to A\ne B$$
9		cgraid.2	$$⊢\phi \to B\ne C$$
10		eqid	$$⊢\mathrm{dist}\left(G\right)=\mathrm{dist}\left(G\right)$$
11		eqid	$$⊢{\sim }_{𝒢}\left(G\right)={\sim }_{𝒢}\left(G\right)$$
12	1 10 2 11 3 5 6 7	cgr3id	$$⊢\phi \to ⟨“ABC”⟩{\sim }_{𝒢}\left(G\right)⟨“ABC”⟩$$
13	1 2 4 5 5 6 3 8	hlid	$$⊢\phi \to AK\left(B\right)A$$
14	9	necomd	$$⊢\phi \to C\ne B$$
15	1 2 4 7 5 6 3 14	hlid	$$⊢\phi \to CK\left(B\right)C$$
16	1 2 4 3 5 6 7 5 6 7 5 7 12 13 15	iscgrad	$$⊢\phi \to ⟨“ABC”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“ABC”⟩$$