tgextancgra

Description: The exterior angle is NOT congruent to the remote interior angle -- the strictness tgextale cannot give, and what tgaas 's contradiction branch needs. The exterior angle is <" A C D "> , at the extension of B C beyond C . The tail of GeoCoq's l11__41__aux , run through acopyeu rather than conga__cop__or__out__ts : a congruent exterior angle would, by angle-construction uniqueness, put the midpoint-reflected point of tgmircgra on the ray C D -- the two rays make congruent angles with the shared base ray C A and, by tgextahp and hpgid , lie on the same open half-plane of line A C -- which tgextamirnhl forbids. Both of acopyeu 's non-collinearity hypotheses are discharged, not assumed: source side by rotating the triangle's own ncol , target side by tgextancd . (Contributed by JAG, 12-Aug-2026)

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

Proof

Step	Hyp	Ref	Expression
1		tgextalem1inag.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		tgextalem1inag.m	⊢ − = ( dist ‘ 𝐺 )
3		tgextalem1inag.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		tgextalem1inag.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
5		tgextalem1inag.k	⊢ 𝐾 = ( hlG ‘ 𝐺 )
6		tgextalem1inag.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
7		tgextalem1inag.a	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
8		tgextalem1inag.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
9		tgextalem1inag.c	⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
10		tgextalem1inag.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
11		tgextalem1inag.ext	⊢ ( 𝜑 → 𝐶 ∈ ( 𝐵 𝐼 𝐷 ) )
12		tgextalem1inag.ncol	⊢ ( 𝜑 → ¬ ( 𝐴 ∈ ( 𝐵 𝐿 𝐶 ) ∨ 𝐵 = 𝐶 ) )
13		tgextalem1inag.ne	⊢ ( 𝜑 → 𝐶 ≠ 𝐷 )
14	1 2 3 4 5 6 7 8 9 10 11 12 13	tgextamirnhl	⊢ ( 𝜑 → ¬ 𝐷 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) )
15	6	adantr	⊢ ( ( 𝜑 ∧ ⟨“ 𝐶 𝐴 𝐵 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ ) → 𝐺 ∈ TarskiG )
16	9	adantr	⊢ ( ( 𝜑 ∧ ⟨“ 𝐶 𝐴 𝐵 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ ) → 𝐶 ∈ 𝑃 )
17	7	adantr	⊢ ( ( 𝜑 ∧ ⟨“ 𝐶 𝐴 𝐵 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ ) → 𝐴 ∈ 𝑃 )
18	8	adantr	⊢ ( ( 𝜑 ∧ ⟨“ 𝐶 𝐴 𝐵 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ ) → 𝐵 ∈ 𝑃 )
19	10	adantr	⊢ ( ( 𝜑 ∧ ⟨“ 𝐶 𝐴 𝐵 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ ) → 𝐷 ∈ 𝑃 )
20	1 4 3 6 8 9 7 12	ncolrot1	⊢ ( 𝜑 → ¬ ( 𝐵 ∈ ( 𝐶 𝐿 𝐴 ) ∨ 𝐶 = 𝐴 ) )
21	1 4 3 6 9 7 8 20	ncolrot1	⊢ ( 𝜑 → ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
22	21	adantr	⊢ ( ( 𝜑 ∧ ⟨“ 𝐶 𝐴 𝐵 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ ) → ¬ ( 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
23	1 2 3 4 6 7 8 9 10 11 12 13	tgextancd	⊢ ( 𝜑 → ¬ ( 𝐴 ∈ ( 𝐶 𝐿 𝐷 ) ∨ 𝐶 = 𝐷 ) )
24	23	adantr	⊢ ( ( 𝜑 ∧ ⟨“ 𝐶 𝐴 𝐵 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ ) → ¬ ( 𝐴 ∈ ( 𝐶 𝐿 𝐷 ) ∨ 𝐶 = 𝐷 ) )
25		eqid	⊢ ( pInvG ‘ 𝐺 ) = ( pInvG ‘ 𝐺 )
26	1 4 3 6 8 9 7 12	ncoltgdim2	⊢ ( 𝜑 → 𝐺 Dim_TarskiG≥ 2 )
27	1 2 3 6 26 7 9	midcl	⊢ ( 𝜑 → ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ∈ 𝑃 )
28		eqid	⊢ ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) = ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) )
29	1 2 3 4 25 6 27 28 8	mircl	⊢ ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ∈ 𝑃 )
30	29	adantr	⊢ ( ( 𝜑 ∧ ⟨“ 𝐶 𝐴 𝐵 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ ) → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ∈ 𝑃 )
31		simpr	⊢ ( ( 𝜑 ∧ ⟨“ 𝐶 𝐴 𝐵 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ ) → ⟨“ 𝐶 𝐴 𝐵 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ )
32	1 2 3 4 6 7 8 9 12	tgmircgra	⊢ ( 𝜑 → ⟨“ 𝐶 𝐴 𝐵 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ”⟩ )
33	32	adantr	⊢ ( ( 𝜑 ∧ ⟨“ 𝐶 𝐴 𝐵 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ ) → ⟨“ 𝐶 𝐴 𝐵 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ”⟩ )
34	1 3 4 6 7 8 9 12	ncolne2	⊢ ( 𝜑 → 𝐴 ≠ 𝐶 )
35	1 3 4 6 7 9 34	tgelrnln	⊢ ( 𝜑 → ( 𝐴 𝐿 𝐶 ) ∈ ran 𝐿 )
36		simpl	⊢ ( ( 𝑢 = 𝑎 ∧ 𝑣 = 𝑏 ) → 𝑢 = 𝑎 )
37	36	eleq1d	⊢ ( ( 𝑢 = 𝑎 ∧ 𝑣 = 𝑏 ) → ( 𝑢 ∈ ( 𝑃 ∖ ( 𝐴 𝐿 𝐶 ) ) ↔ 𝑎 ∈ ( 𝑃 ∖ ( 𝐴 𝐿 𝐶 ) ) ) )
38		simpr	⊢ ( ( 𝑢 = 𝑎 ∧ 𝑣 = 𝑏 ) → 𝑣 = 𝑏 )
39	38	eleq1d	⊢ ( ( 𝑢 = 𝑎 ∧ 𝑣 = 𝑏 ) → ( 𝑣 ∈ ( 𝑃 ∖ ( 𝐴 𝐿 𝐶 ) ) ↔ 𝑏 ∈ ( 𝑃 ∖ ( 𝐴 𝐿 𝐶 ) ) ) )
40	37 39	anbi12d	⊢ ( ( 𝑢 = 𝑎 ∧ 𝑣 = 𝑏 ) → ( ( 𝑢 ∈ ( 𝑃 ∖ ( 𝐴 𝐿 𝐶 ) ) ∧ 𝑣 ∈ ( 𝑃 ∖ ( 𝐴 𝐿 𝐶 ) ) ) ↔ ( 𝑎 ∈ ( 𝑃 ∖ ( 𝐴 𝐿 𝐶 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝐴 𝐿 𝐶 ) ) ) ) )
41		simpr	⊢ ( ( ( 𝑢 = 𝑎 ∧ 𝑣 = 𝑏 ) ∧ 𝑤 = 𝑡 ) → 𝑤 = 𝑡 )
42		simpll	⊢ ( ( ( 𝑢 = 𝑎 ∧ 𝑣 = 𝑏 ) ∧ 𝑤 = 𝑡 ) → 𝑢 = 𝑎 )
43		simplr	⊢ ( ( ( 𝑢 = 𝑎 ∧ 𝑣 = 𝑏 ) ∧ 𝑤 = 𝑡 ) → 𝑣 = 𝑏 )
44	42 43	oveq12d	⊢ ( ( ( 𝑢 = 𝑎 ∧ 𝑣 = 𝑏 ) ∧ 𝑤 = 𝑡 ) → ( 𝑢 𝐼 𝑣 ) = ( 𝑎 𝐼 𝑏 ) )
45	41 44	eleq12d	⊢ ( ( ( 𝑢 = 𝑎 ∧ 𝑣 = 𝑏 ) ∧ 𝑤 = 𝑡 ) → ( 𝑤 ∈ ( 𝑢 𝐼 𝑣 ) ↔ 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) )
46	45	cbvrexdva	⊢ ( ( 𝑢 = 𝑎 ∧ 𝑣 = 𝑏 ) → ( ∃ 𝑤 ∈ ( 𝐴 𝐿 𝐶 ) 𝑤 ∈ ( 𝑢 𝐼 𝑣 ) ↔ ∃ 𝑡 ∈ ( 𝐴 𝐿 𝐶 ) 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) )
47	40 46	anbi12d	⊢ ( ( 𝑢 = 𝑎 ∧ 𝑣 = 𝑏 ) → ( ( ( 𝑢 ∈ ( 𝑃 ∖ ( 𝐴 𝐿 𝐶 ) ) ∧ 𝑣 ∈ ( 𝑃 ∖ ( 𝐴 𝐿 𝐶 ) ) ) ∧ ∃ 𝑤 ∈ ( 𝐴 𝐿 𝐶 ) 𝑤 ∈ ( 𝑢 𝐼 𝑣 ) ) ↔ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝐴 𝐿 𝐶 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝐴 𝐿 𝐶 ) ) ) ∧ ∃ 𝑡 ∈ ( 𝐴 𝐿 𝐶 ) 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) ) )
48	47	cbvopabv	⊢ { ⟨ 𝑢 , 𝑣 ⟩ ∣ ( ( 𝑢 ∈ ( 𝑃 ∖ ( 𝐴 𝐿 𝐶 ) ) ∧ 𝑣 ∈ ( 𝑃 ∖ ( 𝐴 𝐿 𝐶 ) ) ) ∧ ∃ 𝑤 ∈ ( 𝐴 𝐿 𝐶 ) 𝑤 ∈ ( 𝑢 𝐼 𝑣 ) ) } = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃 ∖ ( 𝐴 𝐿 𝐶 ) ) ∧ 𝑏 ∈ ( 𝑃 ∖ ( 𝐴 𝐿 𝐶 ) ) ) ∧ ∃ 𝑡 ∈ ( 𝐴 𝐿 𝐶 ) 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
49		ioran	⊢ ( ¬ ( 𝐴 ∈ ( 𝐶 𝐿 𝐷 ) ∨ 𝐶 = 𝐷 ) ↔ ( ¬ 𝐴 ∈ ( 𝐶 𝐿 𝐷 ) ∧ ¬ 𝐶 = 𝐷 ) )
50	23 49	sylib	⊢ ( 𝜑 → ( ¬ 𝐴 ∈ ( 𝐶 𝐿 𝐷 ) ∧ ¬ 𝐶 = 𝐷 ) )
51	50	simpld	⊢ ( 𝜑 → ¬ 𝐴 ∈ ( 𝐶 𝐿 𝐷 ) )
52	34	necomd	⊢ ( 𝜑 → 𝐶 ≠ 𝐴 )
53	1 3 4 6 9 7 52	tglinerflx2	⊢ ( 𝜑 → 𝐴 ∈ ( 𝐶 𝐿 𝐴 ) )
54	53	adantr	⊢ ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐴 𝐿 𝐶 ) ) → 𝐴 ∈ ( 𝐶 𝐿 𝐴 ) )
55	6	adantr	⊢ ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐴 𝐿 𝐶 ) ) → 𝐺 ∈ TarskiG )
56	9	adantr	⊢ ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐴 𝐿 𝐶 ) ) → 𝐶 ∈ 𝑃 )
57	7	adantr	⊢ ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐴 𝐿 𝐶 ) ) → 𝐴 ∈ 𝑃 )
58	52	adantr	⊢ ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐴 𝐿 𝐶 ) ) → 𝐶 ≠ 𝐴 )
59	10	adantr	⊢ ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐴 𝐿 𝐶 ) ) → 𝐷 ∈ 𝑃 )
60	13	necomd	⊢ ( 𝜑 → 𝐷 ≠ 𝐶 )
61	60	adantr	⊢ ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐴 𝐿 𝐶 ) ) → 𝐷 ≠ 𝐶 )
62		simpr	⊢ ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐴 𝐿 𝐶 ) ) → 𝐷 ∈ ( 𝐴 𝐿 𝐶 ) )
63	34	adantr	⊢ ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐴 𝐿 𝐶 ) ) → 𝐴 ≠ 𝐶 )
64	1 3 4 55 57 56 63	tglinecom	⊢ ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐴 𝐿 𝐶 ) ) → ( 𝐴 𝐿 𝐶 ) = ( 𝐶 𝐿 𝐴 ) )
65	62 64	eleqtrd	⊢ ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐴 𝐿 𝐶 ) ) → 𝐷 ∈ ( 𝐶 𝐿 𝐴 ) )
66	1 3 4 55 56 57 58 59 61 65	tglineelsb2	⊢ ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐴 𝐿 𝐶 ) ) → ( 𝐶 𝐿 𝐴 ) = ( 𝐶 𝐿 𝐷 ) )
67	54 66	eleqtrd	⊢ ( ( 𝜑 ∧ 𝐷 ∈ ( 𝐴 𝐿 𝐶 ) ) → 𝐴 ∈ ( 𝐶 𝐿 𝐷 ) )
68	51 67	mtand	⊢ ( 𝜑 → ¬ 𝐷 ∈ ( 𝐴 𝐿 𝐶 ) )
69	1 3 4 6 35 10 48 68	hpgid	⊢ ( 𝜑 → 𝐷 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐴 𝐿 𝐶 ) ) 𝐷 )
70	69	adantr	⊢ ( ( 𝜑 ∧ ⟨“ 𝐶 𝐴 𝐵 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ ) → 𝐷 ( ( hpG ‘ 𝐺 ) ‘ ( 𝐴 𝐿 𝐶 ) ) 𝐷 )
71	1 2 3 4 5 6 7 8 9 10 11 12 13	tgextahp	⊢ ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ( ( hpG ‘ 𝐺 ) ‘ ( 𝐴 𝐿 𝐶 ) ) 𝐷 )
72	71	adantr	⊢ ( ( 𝜑 ∧ ⟨“ 𝐶 𝐴 𝐵 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ ) → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ( ( hpG ‘ 𝐺 ) ‘ ( 𝐴 𝐿 𝐶 ) ) 𝐷 )
73	1 3 2 15 16 17 18 17 16 19 4 22 24 19 30 5 31 33 70 72	acopyeu	⊢ ( ( 𝜑 ∧ ⟨“ 𝐶 𝐴 𝐵 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ ) → 𝐷 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) )
74	14 73	mtand	⊢ ( 𝜑 → ¬ ⟨“ 𝐶 𝐴 𝐵 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ )

Metamath Proof Explorer

Theorem tgextancgra

Proof