leacgra2

Description: Target-side leA transport: replacing the larger angle by a congruent angle preserves the angle order. Proved from leawittrg and isleag , the witness form of leA . (Contributed by JAG, 12-Aug-2026)

	Ref	Expression
Hypotheses	leacgra2.p	$⊢ P = {Base}_{G}$
	leacgra2.i	$⊢ I = Itv (G)$
	leacgra2.k	$⊢ K = {hl}_{𝒢} (G)$
	leacgra2.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	leacgra2.a	$⊢ φ \to A \in P$
	leacgra2.b	$⊢ φ \to B \in P$
	leacgra2.c	$⊢ φ \to C \in P$
	leacgra2.x	$⊢ φ \to X \in P$
	leacgra2.y	$⊢ φ \to Y \in P$
	leacgra2.z	$⊢ φ \to Z \in P$
	leacgra2.d	$⊢ φ \to D \in P$
	leacgra2.e	$⊢ φ \to E \in P$
	leacgra2.f	$⊢ φ \to F \in P$
	leacgra2.1	$⊢ φ \to ⟨“ A B C ”⟩ \leq_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩$
	leacgra2.2	$⊢ φ \to ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
Assertion	leacgra2	$⊢ φ \to ⟨“ A B C ”⟩ \leq_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$

Proof

Step	Hyp	Ref	Expression
1		leacgra2.p	$⊢ P = {Base}_{G}$
2		leacgra2.i	$⊢ I = Itv (G)$
3		leacgra2.k	$⊢ K = {hl}_{𝒢} (G)$
4		leacgra2.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		leacgra2.a	$⊢ φ \to A \in P$
6		leacgra2.b	$⊢ φ \to B \in P$
7		leacgra2.c	$⊢ φ \to C \in P$
8		leacgra2.x	$⊢ φ \to X \in P$
9		leacgra2.y	$⊢ φ \to Y \in P$
10		leacgra2.z	$⊢ φ \to Z \in P$
11		leacgra2.d	$⊢ φ \to D \in P$
12		leacgra2.e	$⊢ φ \to E \in P$
13		leacgra2.f	$⊢ φ \to F \in P$
14		leacgra2.1	$⊢ φ \to ⟨“ A B C ”⟩ \leq_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩$
15		leacgra2.2	$⊢ φ \to ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
16	4	adantr	$⊢ (φ \land w \in P) \to G \in 𝒢_{Tarski}$
17	16	adantr	$⊢ ((φ \land w \in P) \land (w \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y w ”⟩)) \to G \in 𝒢_{Tarski}$
18	8	adantr	$⊢ (φ \land w \in P) \to X \in P$
19	18	adantr	$⊢ ((φ \land w \in P) \land (w \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y w ”⟩)) \to X \in P$
20	9	adantr	$⊢ (φ \land w \in P) \to Y \in P$
21	20	adantr	$⊢ ((φ \land w \in P) \land (w \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y w ”⟩)) \to Y \in P$
22	10	adantr	$⊢ (φ \land w \in P) \to Z \in P$
23	22	adantr	$⊢ ((φ \land w \in P) \land (w \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y w ”⟩)) \to Z \in P$
24	11	adantr	$⊢ (φ \land w \in P) \to D \in P$
25	24	adantr	$⊢ ((φ \land w \in P) \land (w \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y w ”⟩)) \to D \in P$
26	12	adantr	$⊢ (φ \land w \in P) \to E \in P$
27	26	adantr	$⊢ ((φ \land w \in P) \land (w \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y w ”⟩)) \to E \in P$
28	13	adantr	$⊢ (φ \land w \in P) \to F \in P$
29	28	adantr	$⊢ ((φ \land w \in P) \land (w \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y w ”⟩)) \to F \in P$
30	5	adantr	$⊢ (φ \land w \in P) \to A \in P$
31	30	adantr	$⊢ ((φ \land w \in P) \land (w \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y w ”⟩)) \to A \in P$
32	6	adantr	$⊢ (φ \land w \in P) \to B \in P$
33	32	adantr	$⊢ ((φ \land w \in P) \land (w \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y w ”⟩)) \to B \in P$
34	7	adantr	$⊢ (φ \land w \in P) \to C \in P$
35	34	adantr	$⊢ ((φ \land w \in P) \land (w \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y w ”⟩)) \to C \in P$
36		simpl	$⊢ ((φ \land w \in P) \land (w \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y w ”⟩)) \to (φ \land w \in P)$
37	36	simprd	$⊢ ((φ \land w \in P) \land (w \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y w ”⟩)) \to w \in P$
38		simpr	$⊢ ((φ \land w \in P) \land (w \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y w ”⟩)) \to (w \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y w ”⟩)$
39	38	simpld	$⊢ ((φ \land w \in P) \land (w \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y w ”⟩)) \to w \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩$
40	38	simprd	$⊢ ((φ \land w \in P) \land (w \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y w ”⟩)) \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y w ”⟩$
41	15	adantr	$⊢ (φ \land w \in P) \to ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
42	41	adantr	$⊢ ((φ \land w \in P) \land (w \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y w ”⟩)) \to ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
43	1 2 3 17 19 21 23 25 27 29 31 33 35 37 39 40 42	leawittrg	$⊢ ((φ \land w \in P) \land (w \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y w ”⟩)) \to \exists v \in P (v \in_{𝒢}^{∠} (G) ⟨“ D E F ”⟩ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E v ”⟩)$
44	1 4 5 6 7 8 9 10	isleag	$⊢ φ \to (⟨“ A B C ”⟩ \leq_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \leftrightarrow \exists w \in P (w \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y w ”⟩))$
45	14 44	mpbid	$⊢ φ \to \exists w \in P (w \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y w ”⟩)$
46	43 45	r19.29a	$⊢ φ \to \exists v \in P (v \in_{𝒢}^{∠} (G) ⟨“ D E F ”⟩ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E v ”⟩)$
47	1 4 5 6 7 11 12 13	isleag	$⊢ φ \to (⟨“ A B C ”⟩ \leq_{𝒢}^{∠} (G) ⟨“ D E F ”⟩ \leftrightarrow \exists v \in P (v \in_{𝒢}^{∠} (G) ⟨“ D E F ”⟩ \land ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E v ”⟩))$
48	46 47	mpbird	$⊢ φ \to ⟨“ A B C ”⟩ \leq_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$

Metamath Proof Explorer

Theorem leacgra2

Proof