Metamath Proof Explorer

Theorem 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 ⊢ 𝑃 = ( Base ‘ 𝐺 )
leacgra2.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
leacgra2.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
leacgra2.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
leacgra2.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
leacgra2.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
leacgra2.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
leacgra2.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
leacgra2.y ⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
leacgra2.z ⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
leacgra2.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
leacgra2.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
leacgra2.f ⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
leacgra2.1 ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( ≤∠ ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ )
leacgra2.2 ⊢ ( 𝜑 → ⟨“ 𝑋 𝑌 𝑍 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
Assertion leacgra2 ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( ≤∠ ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )

Proof

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