sacgr

Description: Supplementary angles of congruent angles are themselves congruent. Theorem 11.13 of Schwabhauser p. 98. (Contributed by Thierry Arnoux, 30-Sep-2020) (Proof shortened by Igor Ieskov, 16-Feb-2023)

	Ref	Expression
Hypotheses	dfcgra2.p	$⊢ P = {Base}_{G}$
	dfcgra2.i	$⊢ I = Itv (G)$
	dfcgra2.m	$⊢ \underset{˙}{-} = dist (G)$
	dfcgra2.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	dfcgra2.a	$⊢ φ \to A \in P$
	dfcgra2.b	$⊢ φ \to B \in P$
	dfcgra2.c	$⊢ φ \to C \in P$
	dfcgra2.d	$⊢ φ \to D \in P$
	dfcgra2.e	$⊢ φ \to E \in P$
	dfcgra2.f	$⊢ φ \to F \in P$
	sacgr.x	$⊢ φ \to X \in P$
	sacgr.y	$⊢ φ \to Y \in P$
	sacgr.1	$⊢ φ \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
	sacgr.2	$⊢ φ \to B \in (A I X)$
	sacgr.3	$⊢ φ \to E \in (D I Y)$
	sacgr.4	$⊢ φ \to B \neq X$
	sacgr.5	$⊢ φ \to E \neq Y$
Assertion	sacgr	$⊢ φ \to ⟨“ X B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ Y E F ”⟩$

Proof

Step	Hyp	Ref	Expression
1		dfcgra2.p	$⊢ P = {Base}_{G}$
2		dfcgra2.i	$⊢ I = Itv (G)$
3		dfcgra2.m	$⊢ \underset{˙}{-} = dist (G)$
4		dfcgra2.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		dfcgra2.a	$⊢ φ \to A \in P$
6		dfcgra2.b	$⊢ φ \to B \in P$
7		dfcgra2.c	$⊢ φ \to C \in P$
8		dfcgra2.d	$⊢ φ \to D \in P$
9		dfcgra2.e	$⊢ φ \to E \in P$
10		dfcgra2.f	$⊢ φ \to F \in P$
11		sacgr.x	$⊢ φ \to X \in P$
12		sacgr.y	$⊢ φ \to Y \in P$
13		sacgr.1	$⊢ φ \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
14		sacgr.2	$⊢ φ \to B \in (A I X)$
15		sacgr.3	$⊢ φ \to E \in (D I Y)$
16		sacgr.4	$⊢ φ \to B \neq X$
17		sacgr.5	$⊢ φ \to E \neq Y$
18		eqid	$⊢ {hl}_{𝒢} (G) = {hl}_{𝒢} (G)$
19	4	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ {pInv}_{𝒢} (G) (B) (X) B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F)) \to G \in 𝒢_{Tarski}$
20	11	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ {pInv}_{𝒢} (G) (B) (X) B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F)) \to X \in P$
21	6	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ {pInv}_{𝒢} (G) (B) (X) B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F)) \to B \in P$
22	7	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ {pInv}_{𝒢} (G) (B) (X) B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F)) \to C \in P$
23	12	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ {pInv}_{𝒢} (G) (B) (X) B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F)) \to Y \in P$
24	9	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ {pInv}_{𝒢} (G) (B) (X) B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F)) \to E \in P$
25	10	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ {pInv}_{𝒢} (G) (B) (X) B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F)) \to F \in P$
26		eqid	$⊢ {Line}_{𝒢} (G) = {Line}_{𝒢} (G)$
27		eqid	$⊢ {pInv}_{𝒢} (G) = {pInv}_{𝒢} (G)$
28		eqid	$⊢ {pInv}_{𝒢} (G) (E) = {pInv}_{𝒢} (G) (E)$
29		simpllr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ {pInv}_{𝒢} (G) (B) (X) B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F)) \to x \in P$
30	1 3 2 26 27 19 24 28 29	mircl	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ {pInv}_{𝒢} (G) (B) (X) B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F)) \to {pInv}_{𝒢} (G) (E) (x) \in P$
31		simplr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ {pInv}_{𝒢} (G) (B) (X) B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F)) \to y \in P$
32		eqid	$⊢ {pInv}_{𝒢} (G) (B) = {pInv}_{𝒢} (G) (B)$
33	1 3 2 26 27 4 6 32 11	mirmir	$⊢ φ \to {pInv}_{𝒢} (G) (B) ({pInv}_{𝒢} (G) (B) (X)) = X$
34		eqidd	$⊢ φ \to B = B$
35		eqidd	$⊢ φ \to C = C$
36	33 34 35	s3eqd	$⊢ φ \to ⟨“ {pInv}_{𝒢} (G) (B) ({pInv}_{𝒢} (G) (B) (X)) B C ”⟩ = ⟨“ X B C ”⟩$
37	36	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ {pInv}_{𝒢} (G) (B) (X) B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F)) \to ⟨“ {pInv}_{𝒢} (G) (B) ({pInv}_{𝒢} (G) (B) (X)) B C ”⟩ = ⟨“ X B C ”⟩$
38		eqid	$⊢ \sim_{𝒢} (G) = \sim_{𝒢} (G)$
39	1 3 2 26 27 4 6 32 11	mircl	$⊢ φ \to {pInv}_{𝒢} (G) (B) (X) \in P$
40	39	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ {pInv}_{𝒢} (G) (B) (X) B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F)) \to {pInv}_{𝒢} (G) (B) (X) \in P$
41	16	necomd	$⊢ φ \to X \neq B$
42	1 3 2 26 27 4 6 32 11 41	mirne	$⊢ φ \to {pInv}_{𝒢} (G) (B) (X) \neq B$
43	42	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ {pInv}_{𝒢} (G) (B) (X) B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F)) \to {pInv}_{𝒢} (G) (B) (X) \neq B$
44		simpr1	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ {pInv}_{𝒢} (G) (B) (X) B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F)) \to ⟨“ {pInv}_{𝒢} (G) (B) (X) B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩$
45	1 3 2 26 27 19 38 32 28 40 21 29 24 22 31 43 44	mirtrcgr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ {pInv}_{𝒢} (G) (B) (X) B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F)) \to ⟨“ {pInv}_{𝒢} (G) (B) ({pInv}_{𝒢} (G) (B) (X)) B C ”⟩ \sim_{𝒢} (G) ⟨“ {pInv}_{𝒢} (G) (E) (x) E y ”⟩$
46	37 45	eqbrtrrd	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ {pInv}_{𝒢} (G) (B) (X) B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F)) \to ⟨“ X B C ”⟩ \sim_{𝒢} (G) ⟨“ {pInv}_{𝒢} (G) (E) (x) E y ”⟩$
47	17	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ {pInv}_{𝒢} (G) (B) (X) B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F)) \to E \neq Y$
48	47	necomd	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ {pInv}_{𝒢} (G) (B) (X) B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F)) \to Y \neq E$
49	8	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ {pInv}_{𝒢} (G) (B) (X) B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F)) \to D \in P$
50		simpr2	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ {pInv}_{𝒢} (G) (B) (X) B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F)) \to x {hl}_{𝒢} (G) (E) D$
51	1 2 18 29 49 24 19 50	hlne1	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ {pInv}_{𝒢} (G) (B) (X) B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F)) \to x \neq E$
52	1 3 2 26 27 19 24 28 29 51	mirne	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ {pInv}_{𝒢} (G) (B) (X) B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F)) \to {pInv}_{𝒢} (G) (E) (x) \neq E$
53	1 2 18 29 49 24 19 50	hlcomd	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ {pInv}_{𝒢} (G) (B) (X) B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F)) \to D {hl}_{𝒢} (G) (E) x$
54	15	ad3antrrr	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ {pInv}_{𝒢} (G) (B) (X) B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F)) \to E \in (D I Y)$
55	1 2 18 49 29 23 19 24 53 54	btwnhl	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ {pInv}_{𝒢} (G) (B) (X) B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F)) \to E \in (x I Y)$
56	1 3 2 19 29 24 23 55	tgbtwncom	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ {pInv}_{𝒢} (G) (B) (X) B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F)) \to E \in (Y I x)$
57	1 3 2 26 27 19 24 28 29	mirmir	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ {pInv}_{𝒢} (G) (B) (X) B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F)) \to {pInv}_{𝒢} (G) (E) ({pInv}_{𝒢} (G) (E) (x)) = x$
58	57	oveq2d	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ {pInv}_{𝒢} (G) (B) (X) B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F)) \to Y I {pInv}_{𝒢} (G) (E) ({pInv}_{𝒢} (G) (E) (x)) = Y I x$
59	56 58	eleqtrrd	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ {pInv}_{𝒢} (G) (B) (X) B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F)) \to E \in (Y I {pInv}_{𝒢} (G) (E) ({pInv}_{𝒢} (G) (E) (x)))$
60	1 3 2 26 27 19 28 18 24 23 30 24 48 52 59	mirhl2	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ {pInv}_{𝒢} (G) (B) (X) B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F)) \to Y {hl}_{𝒢} (G) (E) {pInv}_{𝒢} (G) (E) (x)$
61	1 2 18 23 30 24 19 60	hlcomd	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ {pInv}_{𝒢} (G) (B) (X) B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F)) \to {pInv}_{𝒢} (G) (E) (x) {hl}_{𝒢} (G) (E) Y$
62		simpr3	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ {pInv}_{𝒢} (G) (B) (X) B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F)) \to y {hl}_{𝒢} (G) (E) F$
63	1 2 18 19 20 21 22 23 24 25 30 31 46 61 62	iscgrad	$⊢ (((φ \land x \in P) \land y \in P) \land (⟨“ {pInv}_{𝒢} (G) (B) (X) B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F)) \to ⟨“ X B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ Y E F ”⟩$
64	1 2 18 4 5 6 7 8 9 10 13	cgrane2	$⊢ φ \to B \neq C$
65	1 2 4 18 39 6 7 42 64	cgraid	$⊢ φ \to ⟨“ {pInv}_{𝒢} (G) (B) (X) B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ {pInv}_{𝒢} (G) (B) (X) B C ”⟩$
66	1 2 18 4 5 6 7 8 9 10 13	cgrane1	$⊢ φ \to A \neq B$
67	33	oveq2d	$⊢ φ \to A I {pInv}_{𝒢} (G) (B) ({pInv}_{𝒢} (G) (B) (X)) = A I X$
68	14 67	eleqtrrd	$⊢ φ \to B \in (A I {pInv}_{𝒢} (G) (B) ({pInv}_{𝒢} (G) (B) (X)))$
69	1 3 2 26 27 4 32 18 6 5 39 5 66 42 68	mirhl2	$⊢ φ \to A {hl}_{𝒢} (G) (B) {pInv}_{𝒢} (G) (B) (X)$
70	1 2 18 4 39 6 7 39 6 7 65 5 69	cgrahl1	$⊢ φ \to ⟨“ {pInv}_{𝒢} (G) (B) (X) B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ A B C ”⟩$
71	1 2 4 18 39 6 7 5 6 7 70 8 9 10 13	cgratr	$⊢ φ \to ⟨“ {pInv}_{𝒢} (G) (B) (X) B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
72	1 2 18 4 39 6 7 8 9 10	iscgra	$⊢ φ \to (⟨“ {pInv}_{𝒢} (G) (B) (X) B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩ \leftrightarrow \exists x \in P \exists y \in P (⟨“ {pInv}_{𝒢} (G) (B) (X) B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F))$
73	71 72	mpbid	$⊢ φ \to \exists x \in P \exists y \in P (⟨“ {pInv}_{𝒢} (G) (B) (X) B C ”⟩ \sim_{𝒢} (G) ⟨“ x E y ”⟩ \land x {hl}_{𝒢} (G) (E) D \land y {hl}_{𝒢} (G) (E) F)$
74	63 73	r19.29vva	$⊢ φ \to ⟨“ X B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ Y E F ”⟩$

Metamath Proof Explorer

Theorem sacgr

Proof