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	$⊢ P = {Base}_{G}$
	leawittrg.i	$⊢ I = Itv (G)$
	leawittrg.k	$⊢ K = {hl}_{𝒢} (G)$
	leawittrg.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	leawittrg.d	$⊢ φ \to D \in P$
	leawittrg.e	$⊢ φ \to E \in P$
	leawittrg.f	$⊢ φ \to F \in P$
	leawittrg.x	$⊢ φ \to X \in P$
	leawittrg.y	$⊢ φ \to Y \in P$
	leawittrg.z	$⊢ φ \to Z \in P$
	leawittrg.h	$⊢ φ \to H \in P$
	leawittrg.u	$⊢ φ \to U \in P$
	leawittrg.j	$⊢ φ \to J \in P$
	leawittrg.w	$⊢ φ \to W \in P$
	leawittrg.in	$⊢ φ \to W \in_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
	leawittrg.cga	$⊢ φ \to ⟨“ H U J ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E W ”⟩$
	leawittrg.cgb	$⊢ φ \to ⟨“ D E F ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩$
Assertion	leawittrg	$⊢ φ \to \exists v \in P (v \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ H U J ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩)$

Proof

Step	Hyp	Ref	Expression
1		leawittrg.p	$⊢ P = {Base}_{G}$
2		leawittrg.i	$⊢ I = Itv (G)$
3		leawittrg.k	$⊢ K = {hl}_{𝒢} (G)$
4		leawittrg.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		leawittrg.d	$⊢ φ \to D \in P$
6		leawittrg.e	$⊢ φ \to E \in P$
7		leawittrg.f	$⊢ φ \to F \in P$
8		leawittrg.x	$⊢ φ \to X \in P$
9		leawittrg.y	$⊢ φ \to Y \in P$
10		leawittrg.z	$⊢ φ \to Z \in P$
11		leawittrg.h	$⊢ φ \to H \in P$
12		leawittrg.u	$⊢ φ \to U \in P$
13		leawittrg.j	$⊢ φ \to J \in P$
14		leawittrg.w	$⊢ φ \to W \in P$
15		leawittrg.in	$⊢ φ \to W \in_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
16		leawittrg.cga	$⊢ φ \to ⟨“ H U J ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E W ”⟩$
17		leawittrg.cgb	$⊢ φ \to ⟨“ D E F ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩$
18		simpr	$⊢ ((φ \land v \in P) \land (v \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩)) \to (v \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩)$
19	18	simpld	$⊢ ((φ \land v \in P) \land (v \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩)) \to v \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩$
20	4	adantr	$⊢ (φ \land v \in P) \to G \in 𝒢_{Tarski}$
21	20	adantr	$⊢ ((φ \land v \in P) \land (v \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩)) \to G \in 𝒢_{Tarski}$
22	11	adantr	$⊢ (φ \land v \in P) \to H \in P$
23	22	adantr	$⊢ ((φ \land v \in P) \land (v \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩)) \to H \in P$
24	12	adantr	$⊢ (φ \land v \in P) \to U \in P$
25	24	adantr	$⊢ ((φ \land v \in P) \land (v \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩)) \to U \in P$
26	13	adantr	$⊢ (φ \land v \in P) \to J \in P$
27	26	adantr	$⊢ ((φ \land v \in P) \land (v \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩)) \to J \in P$
28	5	adantr	$⊢ (φ \land v \in P) \to D \in P$
29	28	adantr	$⊢ ((φ \land v \in P) \land (v \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩)) \to D \in P$
30	6	adantr	$⊢ (φ \land v \in P) \to E \in P$
31	30	adantr	$⊢ ((φ \land v \in P) \land (v \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩)) \to E \in P$
32	14	adantr	$⊢ (φ \land v \in P) \to W \in P$
33	32	adantr	$⊢ ((φ \land v \in P) \land (v \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩)) \to W \in P$
34	16	adantr	$⊢ (φ \land v \in P) \to ⟨“ H U J ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E W ”⟩$
35	34	adantr	$⊢ ((φ \land v \in P) \land (v \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩)) \to ⟨“ H U J ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ D E W ”⟩$
36	8	adantr	$⊢ (φ \land v \in P) \to X \in P$
37	36	adantr	$⊢ ((φ \land v \in P) \land (v \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩)) \to X \in P$
38	9	adantr	$⊢ (φ \land v \in P) \to Y \in P$
39	38	adantr	$⊢ ((φ \land v \in P) \land (v \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩)) \to Y \in P$
40		simpl	$⊢ ((φ \land v \in P) \land (v \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩)) \to (φ \land v \in P)$
41	40	simprd	$⊢ ((φ \land v \in P) \land (v \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩)) \to v \in P$
42	18	simprd	$⊢ ((φ \land v \in P) \land (v \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩)) \to ⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩$
43	1 2 21 3 23 25 27 29 31 33 35 37 39 41 42	cgratr	$⊢ ((φ \land v \in P) \land (v \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩)) \to ⟨“ H U J ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩$
44	19 43	jca	$⊢ ((φ \land v \in P) \land (v \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩)) \to (v \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ H U J ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩)$
45	1 2 3 4 5 6 7 8 9 10 14 15 17	cgrainag	$⊢ φ \to \exists v \in P (v \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩)$
46	44 45	reximddv3	$⊢ φ \to \exists v \in P (v \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ H U J ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩)$

Metamath Proof Explorer

Theorem leawittrg

Proof