Metamath Proof Explorer

Theorem 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 ⊢ 𝑃 = ( Base ‘ 𝐺 )
leacgra1.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
leacgra1.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
leacgra1.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
leacgra1.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
leacgra1.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
leacgra1.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
leacgra1.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
leacgra1.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
leacgra1.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
leacgra1.h ⊢ ( 𝜑 → 𝐻 ∈ 𝑃 )
leacgra1.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑃 )
leacgra1.j ⊢ ( 𝜑 → 𝐽 ∈ 𝑃 )
leacgra1.1 ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( ≤∠ ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
leacgra1.2 ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐻 𝑈 𝐽 ”⟩ )
Assertion leacgra1 ( 𝜑 → ⟨“ 𝐻 𝑈 𝐽 ”⟩ ( ≤∠ ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )

Proof

Step Hyp Ref Expression
1 leacgra1.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 leacgra1.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
3 leacgra1.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
4 leacgra1.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5 leacgra1.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
6 leacgra1.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
7 leacgra1.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
8 leacgra1.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
9 leacgra1.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
10 leacgra1.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
11 leacgra1.h ⊢ ( 𝜑 → 𝐻 ∈ 𝑃 )
12 leacgra1.u ⊢ ( 𝜑 → 𝑈 ∈ 𝑃 )
13 leacgra1.j ⊢ ( 𝜑 → 𝐽 ∈ 𝑃 )
14 leacgra1.1 ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( ≤∠ ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
15 leacgra1.2 ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐻 𝑈 𝐽 ”⟩ )
16 4 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) → 𝐺 ∈ TarskiG )
17 16 adantr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑤 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑤 ”⟩ ) ) → 𝐺 ∈ TarskiG )
18 11 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) → 𝐻 ∈ 𝑃 )
19 18 adantr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑤 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑤 ”⟩ ) ) → 𝐻 ∈ 𝑃 )
20 12 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) → 𝑈 ∈ 𝑃 )
21 20 adantr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑤 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑤 ”⟩ ) ) → 𝑈 ∈ 𝑃 )
22 13 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) → 𝐽 ∈ 𝑃 )
23 22 adantr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑤 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑤 ”⟩ ) ) → 𝐽 ∈ 𝑃 )
24 8 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) → 𝐷 ∈ 𝑃 )
25 24 adantr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑤 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑤 ”⟩ ) ) → 𝐷 ∈ 𝑃 )
26 9 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) → 𝐸 ∈ 𝑃 )
27 26 adantr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑤 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑤 ”⟩ ) ) → 𝐸 ∈ 𝑃 )
28 10 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) → 𝐹 ∈ 𝑃 )
29 28 adantr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑤 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑤 ”⟩ ) ) → 𝐹 ∈ 𝑃 )
30 eqid ⊢ ( ≤∠ ‘ 𝐺 ) = ( ≤∠ ‘ 𝐺 )
31 simpl ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑤 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑤 ”⟩ ) ) → ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) )
32 31 simprd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑤 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑤 ”⟩ ) ) → 𝑤 ∈ 𝑃 )
33 simpr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑤 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑤 ”⟩ ) ) → ( 𝑤 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑤 ”⟩ ) )
34 33 simpld ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑤 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑤 ”⟩ ) ) → 𝑤 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
35 5 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) → 𝐴 ∈ 𝑃 )
36 35 adantr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑤 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑤 ”⟩ ) ) → 𝐴 ∈ 𝑃 )
37 6 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) → 𝐵 ∈ 𝑃 )
38 37 adantr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑤 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑤 ”⟩ ) ) → 𝐵 ∈ 𝑃 )
39 7 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) → 𝐶 ∈ 𝑃 )
40 39 adantr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑤 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑤 ”⟩ ) ) → 𝐶 ∈ 𝑃 )
41 15 adantr ⊢ ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐻 𝑈 𝐽 ”⟩ )
42 41 adantr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑤 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑤 ”⟩ ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐻 𝑈 𝐽 ”⟩ )
43 1 2 17 3 36 38 40 19 21 23 42 cgracom ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑤 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑤 ”⟩ ) ) → ⟨“ 𝐻 𝑈 𝐽 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ )
44 33 simprd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑤 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑤 ”⟩ ) ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑤 ”⟩ )
45 1 2 17 3 19 21 23 36 38 40 43 25 27 32 44 cgratr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑤 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑤 ”⟩ ) ) → ⟨“ 𝐻 𝑈 𝐽 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑤 ”⟩ )
46 1 17 19 21 23 25 27 29 30 32 34 45 isleagd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ 𝑃 ) ∧ ( 𝑤 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑤 ”⟩ ) ) → ⟨“ 𝐻 𝑈 𝐽 ”⟩ ( ≤∠ ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
47 1 4 5 6 7 8 9 10 isleag ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( ≤∠ ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ↔ ∃ 𝑤 ∈ 𝑃 ( 𝑤 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑤 ”⟩ ) ) )
48 14 47 mpbid ⊢ ( 𝜑 → ∃ 𝑤 ∈ 𝑃 ( 𝑤 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑤 ”⟩ ) )
49 46 48 r19.29a ⊢ ( 𝜑 → ⟨“ 𝐻 𝑈 𝐽 ”⟩ ( ≤∠ ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )