cgrainag

Description: Target-side in-angle transport: if W lies inside angle <" D E F "> and that angle is congruent to <" X Y Z "> , then some point inside <" X Y Z "> makes <" X Y v "> congruent to the sub-angle <" D E W "> . The geometric core of leawittrg . (Contributed by JAG, 12-Aug-2026)

	Ref	Expression
Hypotheses	cgrainag.p	$⊢ P = {Base}_{G}$
	cgrainag.i	$⊢ I = Itv (G)$
	cgrainag.k	$⊢ K = {hl}_{𝒢} (G)$
	cgrainag.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	cgrainag.d	$⊢ φ \to D \in P$
	cgrainag.e	$⊢ φ \to E \in P$
	cgrainag.f	$⊢ φ \to F \in P$
	cgrainag.x	$⊢ φ \to X \in P$
	cgrainag.y	$⊢ φ \to Y \in P$
	cgrainag.z	$⊢ φ \to Z \in P$
	cgrainag.w	$⊢ φ \to W \in P$
	cgrainag.in	$⊢ φ \to W \in_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
	cgrainag.cgb	$⊢ φ \to ⟨“ D E F ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩$
Assertion	cgrainag	$⊢ φ \to \exists v \in P (v \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩)$

Proof

Step	Hyp	Ref	Expression
1		cgrainag.p	$⊢ P = {Base}_{G}$
2		cgrainag.i	$⊢ I = Itv (G)$
3		cgrainag.k	$⊢ K = {hl}_{𝒢} (G)$
4		cgrainag.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		cgrainag.d	$⊢ φ \to D \in P$
6		cgrainag.e	$⊢ φ \to E \in P$
7		cgrainag.f	$⊢ φ \to F \in P$
8		cgrainag.x	$⊢ φ \to X \in P$
9		cgrainag.y	$⊢ φ \to Y \in P$
10		cgrainag.z	$⊢ φ \to Z \in P$
11		cgrainag.w	$⊢ φ \to W \in P$
12		cgrainag.in	$⊢ φ \to W \in_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
13		cgrainag.cgb	$⊢ φ \to ⟨“ D E F ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩$
14	4	adantr	$⊢ (φ \land (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \to G \in 𝒢_{Tarski}$
15	14	adantr	$⊢ ((φ \land (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \land D K (E) W) \to G \in 𝒢_{Tarski}$
16	5	adantr	$⊢ (φ \land (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \to D \in P$
17	16	adantr	$⊢ ((φ \land (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \land D K (E) W) \to D \in P$
18	6	adantr	$⊢ (φ \land (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \to E \in P$
19	18	adantr	$⊢ ((φ \land (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \land D K (E) W) \to E \in P$
20	7	adantr	$⊢ (φ \land (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \to F \in P$
21	20	adantr	$⊢ ((φ \land (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \land D K (E) W) \to F \in P$
22	11	adantr	$⊢ (φ \land (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \to W \in P$
23	22	adantr	$⊢ ((φ \land (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \land D K (E) W) \to W \in P$
24	8	adantr	$⊢ (φ \land (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \to X \in P$
25	24	adantr	$⊢ ((φ \land (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \land D K (E) W) \to X \in P$
26	9	adantr	$⊢ (φ \land (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \to Y \in P$
27	26	adantr	$⊢ ((φ \land (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \land D K (E) W) \to Y \in P$
28	10	adantr	$⊢ (φ \land (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \to Z \in P$
29	28	adantr	$⊢ ((φ \land (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \land D K (E) W) \to Z \in P$
30	13	adantr	$⊢ (φ \land (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \to ⟨“ D E F ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩$
31	30	adantr	$⊢ ((φ \land (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \land D K (E) W) \to ⟨“ D E F ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩$
32		simpr	$⊢ ((φ \land (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \land D K (E) W) \to D K (E) W$
33	1 2 3 15 17 19 21 23 25 27 29 31 32	inagcgrasubhl	$⊢ ((φ \land (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \land D K (E) W) \to \exists v \in P (v \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩)$
34	14	adantr	$⊢ ((φ \land (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \land E \in (D I W)) \to G \in 𝒢_{Tarski}$
35	16	adantr	$⊢ ((φ \land (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \land E \in (D I W)) \to D \in P$
36	18	adantr	$⊢ ((φ \land (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \land E \in (D I W)) \to E \in P$
37	20	adantr	$⊢ ((φ \land (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \land E \in (D I W)) \to F \in P$
38	22	adantr	$⊢ ((φ \land (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \land E \in (D I W)) \to W \in P$
39	24	adantr	$⊢ ((φ \land (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \land E \in (D I W)) \to X \in P$
40	26	adantr	$⊢ ((φ \land (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \land E \in (D I W)) \to Y \in P$
41	28	adantr	$⊢ ((φ \land (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \land E \in (D I W)) \to Z \in P$
42	12	adantr	$⊢ (φ \land (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \to W \in_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
43	42	adantr	$⊢ ((φ \land (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \land E \in (D I W)) \to W \in_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
44	30	adantr	$⊢ ((φ \land (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \land E \in (D I W)) \to ⟨“ D E F ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩$
45		simpr	$⊢ ((φ \land (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \land E \in (D I W)) \to E \in (D I W)$
46	1 2 3 34 35 36 37 38 39 40 41 43 44 45	inagcgrasubbtwn	$⊢ ((φ \land (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \land E \in (D I W)) \to \exists v \in P (v \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩)$
47		simpl	$⊢ ((φ \land (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \land W K (E) D) \to (φ \land (W \in (D {Line}_{𝒢} (G) E) \lor D = E))$
48	47 22	syl	$⊢ ((φ \land (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \land W K (E) D) \to W \in P$
49	47 16	syl	$⊢ ((φ \land (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \land W K (E) D) \to D \in P$
50	47 18	syl	$⊢ ((φ \land (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \land W K (E) D) \to E \in P$
51	47 14	syl	$⊢ ((φ \land (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \land W K (E) D) \to G \in 𝒢_{Tarski}$
52		simpr	$⊢ ((φ \land (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \land W K (E) D) \to W K (E) D$
53	1 2 3 48 49 50 51 52	hlcomd	$⊢ ((φ \land (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \land W K (E) D) \to D K (E) W$
54	53	orcd	$⊢ ((φ \land (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \land W K (E) D) \to (D K (E) W \lor E \in (D I W))$
55	45	olcd	$⊢ ((φ \land (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \land E \in (D I W)) \to (D K (E) W \lor E \in (D I W))$
56		eqid	$⊢ {Line}_{𝒢} (G) = {Line}_{𝒢} (G)$
57		simpr	$⊢ (φ \land (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \to (W \in (D {Line}_{𝒢} (G) E) \lor D = E)$
58	1 2 3 11 5 6 7 4 12	inagne1	$⊢ φ \to D \neq E$
59	58	neneqd	$⊢ φ \to \neg D = E$
60	59	adantr	$⊢ (φ \land (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \to \neg D = E$
61		orel2	$⊢ \neg D = E \to ((W \in (D {Line}_{𝒢} (G) E) \lor D = E) \to W \in (D {Line}_{𝒢} (G) E))$
62	60 61	syl	$⊢ (φ \land (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \to ((W \in (D {Line}_{𝒢} (G) E) \lor D = E) \to W \in (D {Line}_{𝒢} (G) E))$
63	57 62	mpd	$⊢ (φ \land (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \to W \in (D {Line}_{𝒢} (G) E)$
64	1 2 3 16 18 22 14 16 56 63	lnhl	$⊢ (φ \land (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \to (W K (E) D \lor E \in (D I W))$
65	54 55 64	mpjaodan	$⊢ (φ \land (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \to (D K (E) W \lor E \in (D I W))$
66	33 46 65	mpjaodan	$⊢ (φ \land (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \to \exists v \in P (v \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩)$
67	4	adantr	$⊢ (φ \land \neg (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \to G \in 𝒢_{Tarski}$
68	5	adantr	$⊢ (φ \land \neg (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \to D \in P$
69	6	adantr	$⊢ (φ \land \neg (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \to E \in P$
70	7	adantr	$⊢ (φ \land \neg (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \to F \in P$
71	11	adantr	$⊢ (φ \land \neg (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \to W \in P$
72	8	adantr	$⊢ (φ \land \neg (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \to X \in P$
73	9	adantr	$⊢ (φ \land \neg (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \to Y \in P$
74	10	adantr	$⊢ (φ \land \neg (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \to Z \in P$
75	13	adantr	$⊢ (φ \land \neg (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \to ⟨“ D E F ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩$
76	12	adantr	$⊢ (φ \land \neg (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \to W \in_{𝒢}^{∠} (G) ⟨“ D E F ”⟩$
77		simpr	$⊢ (φ \land \neg (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \to \neg (W \in (D {Line}_{𝒢} (G) E) \lor D = E)$
78	1 2 3 67 68 69 70 71 72 73 74 75 56 76 77	inagcgratrgn	$⊢ (φ \land \neg (W \in (D {Line}_{𝒢} (G) E) \lor D = E)) \to \exists v \in P (v \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩)$
79		exmid	$⊢ ((W \in (D {Line}_{𝒢} (G) E) \lor D = E) \lor \neg (W \in (D {Line}_{𝒢} (G) E) \lor D = E))$
80	79	a1i	$⊢ φ \to ((W \in (D {Line}_{𝒢} (G) E) \lor D = E) \lor \neg (W \in (D {Line}_{𝒢} (G) E) \lor D = E))$
81	66 78 80	mpjaodan	$⊢ φ \to \exists v \in P (v \in_{𝒢}^{∠} (G) ⟨“ X Y Z ”⟩ \land ⟨“ D E W ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y v ”⟩)$

Metamath Proof Explorer

Theorem cgrainag

Proof