inagswap

Description: Swap the order of the half lines delimiting the angle. Theorem 11.24 of Schwabhauser p. 101. (Contributed by Thierry Arnoux, 15-Aug-2020)

	Ref	Expression
Hypotheses	isinag.p	$⊢ P = {Base}_{G}$
	isinag.i	$⊢ I = Itv (G)$
	isinag.k	$⊢ K = {hl}_{𝒢} (G)$
	isinag.x	$⊢ φ \to X \in P$
	isinag.a	$⊢ φ \to A \in P$
	isinag.b	$⊢ φ \to B \in P$
	isinag.c	$⊢ φ \to C \in P$
	inagflat.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	inagswap.1	$⊢ φ \to X \in_{𝒢}^{∠} (G) ⟨“ A B C ”⟩$
Assertion	inagswap	$⊢ φ \to X \in_{𝒢}^{∠} (G) ⟨“ C B A ”⟩$

Proof

Step	Hyp	Ref	Expression
1		isinag.p	$⊢ P = {Base}_{G}$
2		isinag.i	$⊢ I = Itv (G)$
3		isinag.k	$⊢ K = {hl}_{𝒢} (G)$
4		isinag.x	$⊢ φ \to X \in P$
5		isinag.a	$⊢ φ \to A \in P$
6		isinag.b	$⊢ φ \to B \in P$
7		isinag.c	$⊢ φ \to C \in P$
8		inagflat.g	$⊢ φ \to G \in 𝒢_{Tarski}$
9		inagswap.1	$⊢ φ \to X \in_{𝒢}^{∠} (G) ⟨“ A B C ”⟩$
10	1 2 3 4 5 6 7 8	isinag	$⊢ φ \to (X \in_{𝒢}^{∠} (G) ⟨“ A B C ”⟩ \leftrightarrow ((A \neq B \land C \neq B \land X \neq B) \land \exists x \in P (x \in (A I C) \land (x = B \lor x K (B) X))))$
11	9 10	mpbid	$⊢ φ \to ((A \neq B \land C \neq B \land X \neq B) \land \exists x \in P (x \in (A I C) \land (x = B \lor x K (B) X)))$
12	11	simpld	$⊢ φ \to (A \neq B \land C \neq B \land X \neq B)$
13	12	simp2d	$⊢ φ \to C \neq B$
14	12	simp1d	$⊢ φ \to A \neq B$
15	12	simp3d	$⊢ φ \to X \neq B$
16	13 14 15	3jca	$⊢ φ \to (C \neq B \land A \neq B \land X \neq B)$
17	11	simprd	$⊢ φ \to \exists x \in P (x \in (A I C) \land (x = B \lor x K (B) X))$
18		eqid	$⊢ dist (G) = dist (G)$
19	8	3ad2ant1	$⊢ (φ \land x \in P \land x \in (A I C)) \to G \in 𝒢_{Tarski}$
20	5	3ad2ant1	$⊢ (φ \land x \in P \land x \in (A I C)) \to A \in P$
21		simp2	$⊢ (φ \land x \in P \land x \in (A I C)) \to x \in P$
22	7	3ad2ant1	$⊢ (φ \land x \in P \land x \in (A I C)) \to C \in P$
23		simp3	$⊢ (φ \land x \in P \land x \in (A I C)) \to x \in (A I C)$
24	1 18 2 19 20 21 22 23	tgbtwncom	$⊢ (φ \land x \in P \land x \in (A I C)) \to x \in (C I A)$
25	24	3expia	$⊢ (φ \land x \in P) \to (x \in (A I C) \to x \in (C I A))$
26	25	anim1d	$⊢ (φ \land x \in P) \to ((x \in (A I C) \land (x = B \lor x K (B) X)) \to (x \in (C I A) \land (x = B \lor x K (B) X)))$
27	26	reximdva	$⊢ φ \to (\exists x \in P (x \in (A I C) \land (x = B \lor x K (B) X)) \to \exists x \in P (x \in (C I A) \land (x = B \lor x K (B) X)))$
28	17 27	mpd	$⊢ φ \to \exists x \in P (x \in (C I A) \land (x = B \lor x K (B) X))$
29	1 2 3 4 7 6 5 8	isinag	$⊢ φ \to (X \in_{𝒢}^{∠} (G) ⟨“ C B A ”⟩ \leftrightarrow ((C \neq B \land A \neq B \land X \neq B) \land \exists x \in P (x \in (C I A) \land (x = B \lor x K (B) X))))$
30	16 28 29	mpbir2and	$⊢ φ \to X \in_{𝒢}^{∠} (G) ⟨“ C B A ”⟩$

Metamath Proof Explorer

Theorem inagswap

Proof