tgextahp

Description: The reflected point and D lie on the same OPEN half-plane of line A C -- the fact acopyeu requires and inA does not give. tgextalem1inag puts the reflected point inside the exterior angle, which is non-strict: isinag 's witness clause is ( x = C \/ x ( KC ) P ) , so a point inside an angle may sit on a boundary ray. The x = C branch collapses to ( A e. ( C L D ) \/ C = D ) and is killed by tgextancd ; the main branch is tgextahpl , whose off-line input is tgextamirn . The $d s are the mandatory ones isinag carries for the witness variable. (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	tgextahp	⊢ ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ( ( hpG ‘ 𝐺 ) ‘ ( 𝐴 𝐿 𝐶 ) ) 𝐷 )

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	tgextalem1inag	⊢ ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ( inA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ )
15		eqid	⊢ ( pInvG ‘ 𝐺 ) = ( pInvG ‘ 𝐺 )
16	1 4 3 6 8 9 7 12	ncoltgdim2	⊢ ( 𝜑 → 𝐺 Dim_TarskiG≥ 2 )
17	1 2 3 6 16 7 9	midcl	⊢ ( 𝜑 → ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ∈ 𝑃 )
18		eqid	⊢ ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) = ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) )
19	1 2 3 4 15 6 17 18 8	mircl	⊢ ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ∈ 𝑃 )
20	1 3 5 19 7 9 10 6	isinag	⊢ ( 𝜑 → ( ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ( inA ‘ 𝐺 ) ⟨“ 𝐴 𝐶 𝐷 ”⟩ ↔ ( ( 𝐴 ≠ 𝐶 ∧ 𝐷 ≠ 𝐶 ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ≠ 𝐶 ) ∧ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( 𝐴 𝐼 𝐷 ) ∧ ( 𝑥 = 𝐶 ∨ 𝑥 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) ) )
21	14 20	mpbid	⊢ ( 𝜑 → ( ( 𝐴 ≠ 𝐶 ∧ 𝐷 ≠ 𝐶 ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ≠ 𝐶 ) ∧ ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( 𝐴 𝐼 𝐷 ) ∧ ( 𝑥 = 𝐶 ∨ 𝑥 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) )
22	21	simprd	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 ( 𝑥 ∈ ( 𝐴 𝐼 𝐷 ) ∧ ( 𝑥 = 𝐶 ∨ 𝑥 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) )
23	6	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐷 ) ∧ ( 𝑥 = 𝐶 ∨ 𝑥 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) ) → 𝐺 ∈ TarskiG )
24	23	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐷 ) ∧ ( 𝑥 = 𝐶 ∨ 𝑥 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) ) ∧ 𝑥 = 𝐶 ) → 𝐺 ∈ TarskiG )
25	9	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐷 ) ∧ ( 𝑥 = 𝐶 ∨ 𝑥 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) ) → 𝐶 ∈ 𝑃 )
26	25	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐷 ) ∧ ( 𝑥 = 𝐶 ∨ 𝑥 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) ) ∧ 𝑥 = 𝐶 ) → 𝐶 ∈ 𝑃 )
27	10	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐷 ) ∧ ( 𝑥 = 𝐶 ∨ 𝑥 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) ) → 𝐷 ∈ 𝑃 )
28	27	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐷 ) ∧ ( 𝑥 = 𝐶 ∨ 𝑥 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) ) ∧ 𝑥 = 𝐶 ) → 𝐷 ∈ 𝑃 )
29	7	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐷 ) ∧ ( 𝑥 = 𝐶 ∨ 𝑥 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) ) → 𝐴 ∈ 𝑃 )
30	29	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐷 ) ∧ ( 𝑥 = 𝐶 ∨ 𝑥 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) ) ∧ 𝑥 = 𝐶 ) → 𝐴 ∈ 𝑃 )
31		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐷 ) ∧ ( 𝑥 = 𝐶 ∨ 𝑥 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) ) ∧ 𝑥 = 𝐶 ) → 𝑥 = 𝐶 )
32		simprrl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐷 ) ∧ ( 𝑥 = 𝐶 ∨ 𝑥 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) ) → 𝑥 ∈ ( 𝐴 𝐼 𝐷 ) )
33	32	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐷 ) ∧ ( 𝑥 = 𝐶 ∨ 𝑥 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) ) ∧ 𝑥 = 𝐶 ) → 𝑥 ∈ ( 𝐴 𝐼 𝐷 ) )
34	31 33	eqeltrrd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐷 ) ∧ ( 𝑥 = 𝐶 ∨ 𝑥 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) ) ∧ 𝑥 = 𝐶 ) → 𝐶 ∈ ( 𝐴 𝐼 𝐷 ) )
35	1 4 3 24 26 28 30 34	btwncolg2	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐷 ) ∧ ( 𝑥 = 𝐶 ∨ 𝑥 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) ) ∧ 𝑥 = 𝐶 ) → ( 𝐴 ∈ ( 𝐶 𝐿 𝐷 ) ∨ 𝐶 = 𝐷 ) )
36	1 2 3 4 6 7 8 9 10 11 12 13	tgextancd	⊢ ( 𝜑 → ¬ ( 𝐴 ∈ ( 𝐶 𝐿 𝐷 ) ∨ 𝐶 = 𝐷 ) )
37	36	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐷 ) ∧ ( 𝑥 = 𝐶 ∨ 𝑥 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) ) → ¬ ( 𝐴 ∈ ( 𝐶 𝐿 𝐷 ) ∨ 𝐶 = 𝐷 ) )
38	37	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐷 ) ∧ ( 𝑥 = 𝐶 ∨ 𝑥 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) ) ∧ 𝑥 = 𝐶 ) → ¬ ( 𝐴 ∈ ( 𝐶 𝐿 𝐷 ) ∨ 𝐶 = 𝐷 ) )
39	35 38	pm2.21dd	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐷 ) ∧ ( 𝑥 = 𝐶 ∨ 𝑥 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) ) ∧ 𝑥 = 𝐶 ) → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ( ( hpG ‘ 𝐺 ) ‘ ( 𝐴 𝐿 𝐶 ) ) 𝐷 )
40	23	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐷 ) ∧ ( 𝑥 = 𝐶 ∨ 𝑥 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) → 𝐺 ∈ TarskiG )
41	29	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐷 ) ∧ ( 𝑥 = 𝐶 ∨ 𝑥 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) → 𝐴 ∈ 𝑃 )
42	25	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐷 ) ∧ ( 𝑥 = 𝐶 ∨ 𝑥 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) → 𝐶 ∈ 𝑃 )
43	27	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐷 ) ∧ ( 𝑥 = 𝐶 ∨ 𝑥 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) → 𝐷 ∈ 𝑃 )
44	19	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐷 ) ∧ ( 𝑥 = 𝐶 ∨ 𝑥 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ∈ 𝑃 )
45	44	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐷 ) ∧ ( 𝑥 = 𝐶 ∨ 𝑥 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ∈ 𝑃 )
46		simprl	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐷 ) ∧ ( 𝑥 = 𝐶 ∨ 𝑥 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) ) → 𝑥 ∈ 𝑃 )
47	46	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐷 ) ∧ ( 𝑥 = 𝐶 ∨ 𝑥 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) → 𝑥 ∈ 𝑃 )
48	37	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐷 ) ∧ ( 𝑥 = 𝐶 ∨ 𝑥 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) → ¬ ( 𝐴 ∈ ( 𝐶 𝐿 𝐷 ) ∨ 𝐶 = 𝐷 ) )
49	1 2 3 4 6 7 8 9 12	tgextamirn	⊢ ( 𝜑 → ¬ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ∈ ( 𝐴 𝐿 𝐶 ) )
50	49	adantr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐷 ) ∧ ( 𝑥 = 𝐶 ∨ 𝑥 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) ) → ¬ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ∈ ( 𝐴 𝐿 𝐶 ) )
51	50	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐷 ) ∧ ( 𝑥 = 𝐶 ∨ 𝑥 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) → ¬ ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ∈ ( 𝐴 𝐿 𝐶 ) )
52	32	adantr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐷 ) ∧ ( 𝑥 = 𝐶 ∨ 𝑥 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) → 𝑥 ∈ ( 𝐴 𝐼 𝐷 ) )
53		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐷 ) ∧ ( 𝑥 = 𝐶 ∨ 𝑥 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) → 𝑥 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) )
54	1 2 3 4 5 40 41 42 43 45 47 48 51 52 53	tgextahpl	⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐷 ) ∧ ( 𝑥 = 𝐶 ∨ 𝑥 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) ) ∧ 𝑥 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ( ( hpG ‘ 𝐺 ) ‘ ( 𝐴 𝐿 𝐶 ) ) 𝐷 )
55		simprrr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐷 ) ∧ ( 𝑥 = 𝐶 ∨ 𝑥 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) ) → ( 𝑥 = 𝐶 ∨ 𝑥 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) )
56	39 54 55	mpjaodan	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑃 ∧ ( 𝑥 ∈ ( 𝐴 𝐼 𝐷 ) ∧ ( 𝑥 = 𝐶 ∨ 𝑥 ( 𝐾 ‘ 𝐶 ) ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ) ) ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ( ( hpG ‘ 𝐺 ) ‘ ( 𝐴 𝐿 𝐶 ) ) 𝐷 )
57	22 56	rexlimddv	⊢ ( 𝜑 → ( ( ( pInvG ‘ 𝐺 ) ‘ ( 𝐴 ( midG ‘ 𝐺 ) 𝐶 ) ) ‘ 𝐵 ) ( ( hpG ‘ 𝐺 ) ‘ ( 𝐴 𝐿 𝐶 ) ) 𝐷 )

Metamath Proof Explorer

Theorem tgextahp

Proof