Theorem leawittrg

Description: Target-side leA witness transport: move a witness inside <" D E F "> across a congruent target angle <" X Y Z "> , carrying the angle <" H U J "> copied at that witness with it. (Contributed by JAG, 12-Aug-2026)

	Ref	Expression
Hypotheses	leawittrg.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	leawittrg.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	leawittrg.k	⊢ 𝐾 = ( hlG ‘ 𝐺 )
	leawittrg.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	leawittrg.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
	leawittrg.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
	leawittrg.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
	leawittrg.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
	leawittrg.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
	leawittrg.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
	leawittrg.h	⊢ ( 𝜑 → 𝐻 ∈ 𝑃 )
	leawittrg.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑃 )
	leawittrg.j	⊢ ( 𝜑 → 𝐽 ∈ 𝑃 )
	leawittrg.w	⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
	leawittrg.in	⊢ ( 𝜑 → 𝑊 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
	leawittrg.cga	⊢ ( 𝜑 → ⟨“ 𝐻 𝑈 𝐽 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑊 ”⟩ )
	leawittrg.cgb	⊢ ( 𝜑 → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ )
Assertion	leawittrg	⊢ ( 𝜑 → ∃ 𝑣 ∈ 𝑃 ( 𝑣 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ⟨“ 𝐻 𝑈 𝐽 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ) )

Proof

Step	Hyp	Ref	Expression
1		leawittrg.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		leawittrg.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
3		leawittrg.k	⊢ 𝐾 = ( hlG ‘ 𝐺 )
4		leawittrg.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5		leawittrg.d	⊢ ( 𝜑 → 𝐷 ∈ 𝑃 )
6		leawittrg.e	⊢ ( 𝜑 → 𝐸 ∈ 𝑃 )
7		leawittrg.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑃 )
8		leawittrg.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑃 )
9		leawittrg.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑃 )
10		leawittrg.z	⊢ ( 𝜑 → 𝑍 ∈ 𝑃 )
11		leawittrg.h	⊢ ( 𝜑 → 𝐻 ∈ 𝑃 )
12		leawittrg.u	⊢ ( 𝜑 → 𝑈 ∈ 𝑃 )
13		leawittrg.j	⊢ ( 𝜑 → 𝐽 ∈ 𝑃 )
14		leawittrg.w	⊢ ( 𝜑 → 𝑊 ∈ 𝑃 )
15		leawittrg.in	⊢ ( 𝜑 → 𝑊 ( inA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝐹 ”⟩ )
16		leawittrg.cga	⊢ ( 𝜑 → ⟨“ 𝐻 𝑈 𝐽 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑊 ”⟩ )
17		leawittrg.cgb	⊢ ( 𝜑 → ⟨“ 𝐷 𝐸 𝐹 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ )
18		simpr	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑃 ) ∧ ( 𝑣 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ) ) → ( 𝑣 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ) )
19	18	simpld	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑃 ) ∧ ( 𝑣 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ) ) → 𝑣 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ )
20	4	adantr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑃 ) → 𝐺 ∈ TarskiG )
21	20	adantr	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑃 ) ∧ ( 𝑣 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ) ) → 𝐺 ∈ TarskiG )
22	11	adantr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑃 ) → 𝐻 ∈ 𝑃 )
23	22	adantr	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑃 ) ∧ ( 𝑣 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ) ) → 𝐻 ∈ 𝑃 )
24	12	adantr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑃 ) → 𝑈 ∈ 𝑃 )
25	24	adantr	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑃 ) ∧ ( 𝑣 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ) ) → 𝑈 ∈ 𝑃 )
26	13	adantr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑃 ) → 𝐽 ∈ 𝑃 )
27	26	adantr	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑃 ) ∧ ( 𝑣 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ) ) → 𝐽 ∈ 𝑃 )
28	5	adantr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑃 ) → 𝐷 ∈ 𝑃 )
29	28	adantr	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑃 ) ∧ ( 𝑣 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ) ) → 𝐷 ∈ 𝑃 )
30	6	adantr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑃 ) → 𝐸 ∈ 𝑃 )
31	30	adantr	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑃 ) ∧ ( 𝑣 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ) ) → 𝐸 ∈ 𝑃 )
32	14	adantr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑃 ) → 𝑊 ∈ 𝑃 )
33	32	adantr	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑃 ) ∧ ( 𝑣 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ) ) → 𝑊 ∈ 𝑃 )
34	16	adantr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑃 ) → ⟨“ 𝐻 𝑈 𝐽 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑊 ”⟩ )
35	34	adantr	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑃 ) ∧ ( 𝑣 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ) ) → ⟨“ 𝐻 𝑈 𝐽 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝐷 𝐸 𝑊 ”⟩ )
36	8	adantr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑃 ) → 𝑋 ∈ 𝑃 )
37	36	adantr	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑃 ) ∧ ( 𝑣 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ) ) → 𝑋 ∈ 𝑃 )
38	9	adantr	⊢ ( ( 𝜑 ∧ 𝑣 ∈ 𝑃 ) → 𝑌 ∈ 𝑃 )
39	38	adantr	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑃 ) ∧ ( 𝑣 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ) ) → 𝑌 ∈ 𝑃 )
40		simpl	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑃 ) ∧ ( 𝑣 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ) ) → ( 𝜑 ∧ 𝑣 ∈ 𝑃 ) )
41	40	simprd	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑃 ) ∧ ( 𝑣 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ) ) → 𝑣 ∈ 𝑃 )
42	18	simprd	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑃 ) ∧ ( 𝑣 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ) ) → ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ )
43	1 2 21 3 23 25 27 29 31 33 35 37 39 41 42	cgratr	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑃 ) ∧ ( 𝑣 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ) ) → ⟨“ 𝐻 𝑈 𝐽 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ )
44	19 43	jca	⊢ ( ( ( 𝜑 ∧ 𝑣 ∈ 𝑃 ) ∧ ( 𝑣 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ) ) → ( 𝑣 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ⟨“ 𝐻 𝑈 𝐽 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ) )
45	1 2 3 4 5 6 7 8 9 10 14 15 17	cgrainag	⊢ ( 𝜑 → ∃ 𝑣 ∈ 𝑃 ( 𝑣 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ⟨“ 𝐷 𝐸 𝑊 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ) )
46	44 45	reximddv3	⊢ ( 𝜑 → ∃ 𝑣 ∈ 𝑃 ( 𝑣 ( inA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑍 ”⟩ ∧ ⟨“ 𝐻 𝑈 𝐽 ”⟩ ( cgrA ‘ 𝐺 ) ⟨“ 𝑋 𝑌 𝑣 ”⟩ ) )