Metamath Proof Explorer

Theorem tgextalt2

Description: tgexta 's SECOND conjunct, strict, at a supplied second extension point E . This is NOT a permutation of the first conjunct: E is a new point, C between A and E , and tgextale / tgextancgra are applied a second time at the reconfigured triangle (the roles of A and B exchanged, exterior angle <" B C E "> ). tgextaoa then identifies <" B C E "> with <" A C D "> as vertical angles, and the two halves are transported across that congruence -- leacgra for leA , and cgratr under mtand for the negation, which leacgra cannot move. E is existentially constructed by tgexta , not here. (Contributed by JAG, 12-Aug-2026)

Ref Expression
Hypotheses tgextalt2.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
tgextalt2.m ⊢ − = ( dist ‘ 𝐺 )
tgextalt2.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
tgextalt2.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
tgextalt2.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
tgextalt2.s ⊢ ≤ = ( ≤∠ ‘ 𝐺 )
tgextalt2.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
tgextalt2.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
tgextalt2.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
tgextalt2.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
tgextalt2.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
tgextalt2.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
tgextalt2.ext ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) )
tgextalt2.ext2 ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 𝐼 𝐸 ) )
tgextalt2.ncol ⊢ ( 𝜑 → ¬ ( 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) )
tgextalt2.ne ⊢ ( 𝜑 → 𝐶 ≠ 𝐷 )
tgextalt2.ne2 ⊢ ( 𝜑 → 𝐶 ≠ 𝐸 )
Assertion tgextalt2 ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ≤ ⟨“ 𝐴 𝐶 𝐷 ”⟩ ∧ ¬ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ ) )

Proof

Step Hyp Ref Expression
1 tgextalt2.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 tgextalt2.m ⊢ − = ( dist ‘ 𝐺 )
3 tgextalt2.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 tgextalt2.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
5 tgextalt2.k ⊢ 𝐾 = ( hlG ‘ 𝐺 )
6 tgextalt2.s ⊢ ≤ = ( ≤∠ ‘ 𝐺 )
7 tgextalt2.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
8 tgextalt2.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
9 tgextalt2.b ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
10 tgextalt2.c ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
11 tgextalt2.d ⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
12 tgextalt2.e ⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
13 tgextalt2.ext ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) )
14 tgextalt2.ext2 ⊢ ( 𝜑 → 𝐶 ∈ ( 𝐴 𝐼 𝐸 ) )
15 tgextalt2.ncol ⊢ ( 𝜑 → ¬ ( 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) )
16 tgextalt2.ne ⊢ ( 𝜑 → 𝐶 ≠ 𝐷 )
17 tgextalt2.ne2 ⊢ ( 𝜑 → 𝐶 ≠ 𝐸 )
18 1 4 3 7 9 10 8 15 ncolrot2 ⊢ ( 𝜑 → ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
19 1 4 3 7 8 9 10 18 ncolcom ⊢ ( 𝜑 → ¬ ( 𝐶 ∈ ( 𝐵 𝐿 𝐴 ) ∨ 𝐵 = 𝐴 ) )
20 1 4 3 7 9 8 10 19 ncolrot1 ⊢ ( 𝜑 → ¬ ( 𝐵 ∈ ( 𝐴 𝐿 𝐶 ) ∨ 𝐴 = 𝐶 ) )
21 1 2 3 4 5 7 9 8 10 12 14 20 17 tgextale ⊢ ( 𝜑 → ⟨“ 𝐶 𝐵 𝐴 ”⟩ ( ≤∠ ‘ 𝐺 ) ⟨“ 𝐵 𝐶 𝐸 ”⟩ )
22 6 breqi ⊢ ( ⟨“ 𝐶 𝐵 𝐴 ”⟩ ≤ ⟨“ 𝐵 𝐶 𝐸 ”⟩ ↔ ⟨“ 𝐶 𝐵 𝐴 ”⟩ ( ≤∠ ‘ 𝐺 ) ⟨“ 𝐵 𝐶 𝐸 ”⟩ )
23 21 22 sylibr ⊢ ( 𝜑 → ⟨“ 𝐶 𝐵 𝐴 ”⟩ ≤ ⟨“ 𝐵 𝐶 𝐸 ”⟩ )
24 1 4 3 7 9 10 8 15 ncolrot1 ⊢ ( 𝜑 → ¬ ( 𝐵 ∈ ( 𝐶 𝐿 𝐴 ) ∨ 𝐶 = 𝐴 ) )
25 1 3 4 7 9 10 8 24 ncolne1 ⊢ ( 𝜑 → 𝐵 ≠ 𝐶 )
26 25 necomd ⊢ ( 𝜑 → 𝐶 ≠ 𝐵 )
27 1 3 4 7 8 9 10 15 ncolne1 ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
28 27 necomd ⊢ ( 𝜑 → 𝐵 ≠ 𝐴 )
29 1 3 7 5 10 9 8 26 28 cgraswap ⊢ ( 𝜑 → ⟨“ 𝐶 𝐵 𝐴 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ )
30 1 3 4 7 8 9 10 15 ncolne2 ⊢ ( 𝜑 → 𝐴 ≠ 𝐶 )
31 30 necomd ⊢ ( 𝜑 → 𝐶 ≠ 𝐴 )
32 16 necomd ⊢ ( 𝜑 → 𝐷 ≠ 𝐶 )
33 1 2 3 5 7 8 9 10 11 12 13 14 26 31 32 17 tgextaoa ⊢ ( 𝜑 → ⟨“ 𝐵 𝐶 𝐸 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ )
34 1 3 5 6 7 10 9 8 9 10 12 8 9 10 8 10 11 23 29 33 leacgra ⊢ ( 𝜑 → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ≤ ⟨“ 𝐴 𝐶 𝐷 ”⟩ )
35 1 2 3 4 5 7 9 8 10 12 14 20 17 tgextancgra ⊢ ( 𝜑 → ¬ ⟨“ 𝐶 𝐵 𝐴 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐵 𝐶 𝐸 ”⟩ )
36 7 adantr ⊢ ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ ) → 𝐺 ∈ TarskiG )
37 10 adantr ⊢ ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ ) → 𝐶 ∈ 𝑃 )
38 9 adantr ⊢ ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ ) → 𝐵 ∈ 𝑃 )
39 8 adantr ⊢ ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ ) → 𝐴 ∈ 𝑃 )
40 11 adantr ⊢ ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ ) → 𝐷 ∈ 𝑃 )
41 29 adantr ⊢ ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ ) → ⟨“ 𝐶 𝐵 𝐴 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐵 𝐶 ”⟩ )
42 simpr ⊢ ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ ) → ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ )
43 1 3 36 5 37 38 39 39 38 37 41 39 37 40 42 cgratr ⊢ ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ ) → ⟨“ 𝐶 𝐵 𝐴 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ )
44 12 adantr ⊢ ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ ) → 𝐸 ∈ 𝑃 )
45 1 3 7 5 9 10 12 8 10 11 33 cgracom ⊢ ( 𝜑 → ⟨“ 𝐴 𝐶 𝐷 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐵 𝐶 𝐸 ”⟩ )
46 45 adantr ⊢ ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ ) → ⟨“ 𝐴 𝐶 𝐷 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐵 𝐶 𝐸 ”⟩ )
47 1 3 36 5 37 38 39 39 37 40 43 38 37 44 46 cgratr ⊢ ( ( 𝜑 ∧ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ ) → ⟨“ 𝐶 𝐵 𝐴 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐵 𝐶 𝐸 ”⟩ )
48 35 47 mtand ⊢ ( 𝜑 → ¬ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ )
49 34 48 jca ⊢ ( 𝜑 → ( ⟨“ 𝐴 𝐵 𝐶 ”⟩ ≤ ⟨“ 𝐴 𝐶 𝐷 ”⟩ ∧ ¬ ⟨“ 𝐴 𝐵 𝐶 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ ) )