leacgra1

Description: Source-side leA transport: replacing the smaller angle by a congruent angle preserves the angle order. The counterpart of leacgra2 , proved directly from the witness form of leA ( isleag , isleagd ). (Contributed by JAG, 12-Aug-2026)

	Ref	Expression
Hypotheses	leacgra1.p	$⊢ P = {Base}_{G}$
	leacgra1.i	$⊢ I = Itv (G)$
	leacgra1.k	$⊢ K = {hl}_{𝒢} (G)$
	leacgra1.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	leacgra1.a	$⊢ φ \to A \in P$
	leacgra1.b	$⊢ φ \to B \in P$
	leacgra1.c	$⊢ φ \to C \in P$
	leacgra1.d	$⊢ φ \to D \in P$
	leacgra1.e	$⊢ φ \to E \in P$
	leacgra1.f	$⊢ φ \to F \in P$
	leacgra1.h	$⊢ φ \to H \in P$
	leacgra1.u	$⊢ φ \to U \in P$
	leacgra1.j	$⊢ φ \to J \in P$
	leacgra1.1	$⊢ φ \to ⟨“ A B C ”⟩ \leq_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
	leacgra1.2	$⊢ φ \to ⟨“ A B C ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ H U J ”⟩$
Assertion	leacgra1	$⊢ φ \to ⟨“ H U J ”⟩ \leq_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$

Proof

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

Metamath Proof Explorer

Theorem leacgra1

Proof