ragsupplcgra

Description: An angle <" X Y Z "> is a right angle exactly when it is congruent to its supplementary angle <" X Y W "> . Theorem 11.18 of Schwabhauser p. 98. (Contributed by Thierry Arnoux, 13-Jul-2026)

	Ref	Expression
Hypotheses	ragsupplcgra.p	$⊢ P = {Base}_{G}$
	ragsupplcgra.i	$⊢ I = Itv (G)$
	ragsupplcgra.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	ragsupplcgra.7	$⊢ φ \to X \in (P ∖ \{Y\})$
	ragsupplcgra.x	$⊢ φ \to Y \in P$
	ragsupplcgra.z	$⊢ φ \to Z \in (P ∖ \{Y\})$
	ragsupplcgra.w	$⊢ φ \to W \in (P ∖ \{Y\})$
	ragsupplcgra.y	$⊢ φ \to Y \in (Z I W)$
Assertion	ragsupplcgra	$⊢ φ \to (⟨“ X Y Z ”⟩ \in ∟_{𝒢} (G) \leftrightarrow ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y W ”⟩)$

Proof

Step	Hyp	Ref	Expression
1		ragsupplcgra.p	$⊢ P = {Base}_{G}$
2		ragsupplcgra.i	$⊢ I = Itv (G)$
3		ragsupplcgra.g	$⊢ φ \to G \in 𝒢_{Tarski}$
4		ragsupplcgra.7	$⊢ φ \to X \in (P ∖ \{Y\})$
5		ragsupplcgra.x	$⊢ φ \to Y \in P$
6		ragsupplcgra.z	$⊢ φ \to Z \in (P ∖ \{Y\})$
7		ragsupplcgra.w	$⊢ φ \to W \in (P ∖ \{Y\})$
8		ragsupplcgra.y	$⊢ φ \to Y \in (Z I W)$
9	3	adantr	$⊢ (φ \land ⟨“ X Y Z ”⟩ \in ∟_{𝒢} (G)) \to G \in 𝒢_{Tarski}$
10	4	eldifad	$⊢ φ \to X \in P$
11	10	adantr	$⊢ (φ \land ⟨“ X Y Z ”⟩ \in ∟_{𝒢} (G)) \to X \in P$
12	5	adantr	$⊢ (φ \land ⟨“ X Y Z ”⟩ \in ∟_{𝒢} (G)) \to Y \in P$
13	6	eldifad	$⊢ φ \to Z \in P$
14	13	adantr	$⊢ (φ \land ⟨“ X Y Z ”⟩ \in ∟_{𝒢} (G)) \to Z \in P$
15	7	eldifad	$⊢ φ \to W \in P$
16	15	adantr	$⊢ (φ \land ⟨“ X Y Z ”⟩ \in ∟_{𝒢} (G)) \to W \in P$
17		simpr	$⊢ (φ \land ⟨“ X Y Z ”⟩ \in ∟_{𝒢} (G)) \to ⟨“ X Y Z ”⟩ \in ∟_{𝒢} (G)$
18		eqid	$⊢ dist (G) = dist (G)$
19		eqid	$⊢ {Line}_{𝒢} (G) = {Line}_{𝒢} (G)$
20		eqid	$⊢ {pInv}_{𝒢} (G) = {pInv}_{𝒢} (G)$
21	1 18 2 19 20 9 11 12 14 17	ragcom	$⊢ (φ \land ⟨“ X Y Z ”⟩ \in ∟_{𝒢} (G)) \to ⟨“ Z Y X ”⟩ \in ∟_{𝒢} (G)$
22	6	eldifsnbd	$⊢ φ \to Z \neq Y$
23	22	adantr	$⊢ (φ \land ⟨“ X Y Z ”⟩ \in ∟_{𝒢} (G)) \to Z \neq Y$
24	8	adantr	$⊢ (φ \land ⟨“ X Y Z ”⟩ \in ∟_{𝒢} (G)) \to Y \in (Z I W)$
25	1 19 2 9 12 16 14 24	btwncolg2	$⊢ (φ \land ⟨“ X Y Z ”⟩ \in ∟_{𝒢} (G)) \to (Z \in (Y {Line}_{𝒢} (G) W) \lor Y = W)$
26	1 18 2 19 20 9 14 12 11 16 21 23 25	ragcol	$⊢ (φ \land ⟨“ X Y Z ”⟩ \in ∟_{𝒢} (G)) \to ⟨“ W Y X ”⟩ \in ∟_{𝒢} (G)$
27	1 18 2 19 20 9 16 12 11 26	ragcom	$⊢ (φ \land ⟨“ X Y Z ”⟩ \in ∟_{𝒢} (G)) \to ⟨“ X Y W ”⟩ \in ∟_{𝒢} (G)$
28	4	eldifsnbd	$⊢ φ \to X \neq Y$
29	28	adantr	$⊢ (φ \land ⟨“ X Y Z ”⟩ \in ∟_{𝒢} (G)) \to X \neq Y$
30	7	eldifsnbd	$⊢ φ \to W \neq Y$
31	30	necomd	$⊢ φ \to Y \neq W$
32	31	adantr	$⊢ (φ \land ⟨“ X Y Z ”⟩ \in ∟_{𝒢} (G)) \to Y \neq W$
33	22	necomd	$⊢ φ \to Y \neq Z$
34	33	adantr	$⊢ (φ \land ⟨“ X Y Z ”⟩ \in ∟_{𝒢} (G)) \to Y \neq Z$
35	1 9 11 12 14 11 12 16 17 27 29 32 29 34	ragcgra	$⊢ (φ \land ⟨“ X Y Z ”⟩ \in ∟_{𝒢} (G)) \to ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y W ”⟩$
36	3	ad6antr	$⊢ ((((((φ \land ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y W ”⟩) \land x \in P) \land z \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ x Y z ”⟩) \land x {hl}_{𝒢} (G) (Y) X) \land z {hl}_{𝒢} (G) (Y) W) \to G \in 𝒢_{Tarski}$
37	13	ad6antr	$⊢ ((((((φ \land ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y W ”⟩) \land x \in P) \land z \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ x Y z ”⟩) \land x {hl}_{𝒢} (G) (Y) X) \land z {hl}_{𝒢} (G) (Y) W) \to Z \in P$
38	10	ad6antr	$⊢ ((((((φ \land ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y W ”⟩) \land x \in P) \land z \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ x Y z ”⟩) \land x {hl}_{𝒢} (G) (Y) X) \land z {hl}_{𝒢} (G) (Y) W) \to X \in P$
39		simp-4r	$⊢ ((((((φ \land ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y W ”⟩) \land x \in P) \land z \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ x Y z ”⟩) \land x {hl}_{𝒢} (G) (Y) X) \land z {hl}_{𝒢} (G) (Y) W) \to z \in P$
40		simp-5r	$⊢ ((((((φ \land ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y W ”⟩) \land x \in P) \land z \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ x Y z ”⟩) \land x {hl}_{𝒢} (G) (Y) X) \land z {hl}_{𝒢} (G) (Y) W) \to x \in P$
41		eqid	$⊢ \sim_{𝒢} (G) = \sim_{𝒢} (G)$
42	5	ad6antr	$⊢ ((((((φ \land ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y W ”⟩) \land x \in P) \land z \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ x Y z ”⟩) \land x {hl}_{𝒢} (G) (Y) X) \land z {hl}_{𝒢} (G) (Y) W) \to Y \in P$
43		simpllr	$⊢ ((((((φ \land ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y W ”⟩) \land x \in P) \land z \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ x Y z ”⟩) \land x {hl}_{𝒢} (G) (Y) X) \land z {hl}_{𝒢} (G) (Y) W) \to ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ x Y z ”⟩$
44	1 18 2 41 36 38 42 37 40 42 39 43	cgr3simp3	$⊢ ((((((φ \land ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y W ”⟩) \land x \in P) \land z \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ x Y z ”⟩) \land x {hl}_{𝒢} (G) (Y) X) \land z {hl}_{𝒢} (G) (Y) W) \to Z dist (G) X = z dist (G) x$
45	1 18 2 36 37 38 39 40 44	tgcgrcomlr	$⊢ ((((((φ \land ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y W ”⟩) \land x \in P) \land z \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ x Y z ”⟩) \land x {hl}_{𝒢} (G) (Y) X) \land z {hl}_{𝒢} (G) (Y) W) \to X dist (G) Z = x dist (G) z$
46		eqid	$⊢ {hl}_{𝒢} (G) = {hl}_{𝒢} (G)$
47	28	ad6antr	$⊢ ((((((φ \land ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y W ”⟩) \land x \in P) \land z \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ x Y z ”⟩) \land x {hl}_{𝒢} (G) (Y) X) \land z {hl}_{𝒢} (G) (Y) W) \to X \neq Y$
48	47	necomd	$⊢ ((((((φ \land ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y W ”⟩) \land x \in P) \land z \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ x Y z ”⟩) \land x {hl}_{𝒢} (G) (Y) X) \land z {hl}_{𝒢} (G) (Y) W) \to Y \neq X$
49	1 2 46 38 38 42 36 47	hlid	$⊢ ((((((φ \land ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y W ”⟩) \land x \in P) \land z \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ x Y z ”⟩) \land x {hl}_{𝒢} (G) (Y) X) \land z {hl}_{𝒢} (G) (Y) W) \to X {hl}_{𝒢} (G) (Y) X$
50		simplr	$⊢ ((((((φ \land ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y W ”⟩) \land x \in P) \land z \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ x Y z ”⟩) \land x {hl}_{𝒢} (G) (Y) X) \land z {hl}_{𝒢} (G) (Y) W) \to x {hl}_{𝒢} (G) (Y) X$
51		eqidd	$⊢ ((((((φ \land ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y W ”⟩) \land x \in P) \land z \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ x Y z ”⟩) \land x {hl}_{𝒢} (G) (Y) X) \land z {hl}_{𝒢} (G) (Y) W) \to Y dist (G) X = Y dist (G) X$
52	1 18 2 41 36 38 42 37 40 42 39 43	cgr3simp1	$⊢ ((((((φ \land ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y W ”⟩) \land x \in P) \land z \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ x Y z ”⟩) \land x {hl}_{𝒢} (G) (Y) X) \land z {hl}_{𝒢} (G) (Y) W) \to X dist (G) Y = x dist (G) Y$
53	52	eqcomd	$⊢ ((((((φ \land ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y W ”⟩) \land x \in P) \land z \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ x Y z ”⟩) \land x {hl}_{𝒢} (G) (Y) X) \land z {hl}_{𝒢} (G) (Y) W) \to x dist (G) Y = X dist (G) Y$
54	1 18 2 36 40 42 38 42 53	tgcgrcomlr	$⊢ ((((((φ \land ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y W ”⟩) \land x \in P) \land z \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ x Y z ”⟩) \land x {hl}_{𝒢} (G) (Y) X) \land z {hl}_{𝒢} (G) (Y) W) \to Y dist (G) x = Y dist (G) X$
55	1 18 46 42 42 38 36 38 47 48 49 50 51 54	hlcgreq	$⊢ ((((((φ \land ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y W ”⟩) \land x \in P) \land z \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ x Y z ”⟩) \land x {hl}_{𝒢} (G) (Y) X) \land z {hl}_{𝒢} (G) (Y) W) \to X = x$
56		eqid	$⊢ {pInv}_{𝒢} (G) (Y) = {pInv}_{𝒢} (G) (Y)$
57	1 18 2 19 20 36 42 56 37	mircl	$⊢ ((((((φ \land ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y W ”⟩) \land x \in P) \land z \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ x Y z ”⟩) \land x {hl}_{𝒢} (G) (Y) X) \land z {hl}_{𝒢} (G) (Y) W) \to {pInv}_{𝒢} (G) (Y) (Z) \in P$
58	22	ad6antr	$⊢ ((((((φ \land ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y W ”⟩) \land x \in P) \land z \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ x Y z ”⟩) \land x {hl}_{𝒢} (G) (Y) X) \land z {hl}_{𝒢} (G) (Y) W) \to Z \neq Y$
59	1 18 2 19 20 36 42 56 37	mirbtwn	$⊢ ((((((φ \land ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y W ”⟩) \land x \in P) \land z \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ x Y z ”⟩) \land x {hl}_{𝒢} (G) (Y) X) \land z {hl}_{𝒢} (G) (Y) W) \to Y \in ({pInv}_{𝒢} (G) (Y) (Z) I Z)$
60	1 18 2 36 57 42 37 59	tgbtwncom	$⊢ ((((((φ \land ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y W ”⟩) \land x \in P) \land z \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ x Y z ”⟩) \land x {hl}_{𝒢} (G) (Y) X) \land z {hl}_{𝒢} (G) (Y) W) \to Y \in (Z I {pInv}_{𝒢} (G) (Y) (Z))$
61	15	ad6antr	$⊢ ((((((φ \land ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y W ”⟩) \land x \in P) \land z \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ x Y z ”⟩) \land x {hl}_{𝒢} (G) (Y) X) \land z {hl}_{𝒢} (G) (Y) W) \to W \in P$
62		simpr	$⊢ ((((((φ \land ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y W ”⟩) \land x \in P) \land z \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ x Y z ”⟩) \land x {hl}_{𝒢} (G) (Y) X) \land z {hl}_{𝒢} (G) (Y) W) \to z {hl}_{𝒢} (G) (Y) W$
63	1 2 46 39 61 42 36 62	hlcomd	$⊢ ((((((φ \land ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y W ”⟩) \land x \in P) \land z \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ x Y z ”⟩) \land x {hl}_{𝒢} (G) (Y) X) \land z {hl}_{𝒢} (G) (Y) W) \to W {hl}_{𝒢} (G) (Y) z$
64	1 18 2 3 13 5 15 8	tgbtwncom	$⊢ φ \to Y \in (W I Z)$
65	64	ad6antr	$⊢ ((((((φ \land ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y W ”⟩) \land x \in P) \land z \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ x Y z ”⟩) \land x {hl}_{𝒢} (G) (Y) X) \land z {hl}_{𝒢} (G) (Y) W) \to Y \in (W I Z)$
66	1 2 46 61 39 37 36 42 63 65	btwnhl	$⊢ ((((((φ \land ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y W ”⟩) \land x \in P) \land z \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ x Y z ”⟩) \land x {hl}_{𝒢} (G) (Y) X) \land z {hl}_{𝒢} (G) (Y) W) \to Y \in (z I Z)$
67	1 18 2 36 39 42 37 66	tgbtwncom	$⊢ ((((((φ \land ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y W ”⟩) \land x \in P) \land z \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ x Y z ”⟩) \land x {hl}_{𝒢} (G) (Y) X) \land z {hl}_{𝒢} (G) (Y) W) \to Y \in (Z I z)$
68	1 18 2 19 20 36 42 56 37	mircgr	$⊢ ((((((φ \land ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y W ”⟩) \land x \in P) \land z \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ x Y z ”⟩) \land x {hl}_{𝒢} (G) (Y) X) \land z {hl}_{𝒢} (G) (Y) W) \to Y dist (G) {pInv}_{𝒢} (G) (Y) (Z) = Y dist (G) Z$
69	1 18 2 41 36 38 42 37 40 42 39 43	cgr3simp2	$⊢ ((((((φ \land ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y W ”⟩) \land x \in P) \land z \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ x Y z ”⟩) \land x {hl}_{𝒢} (G) (Y) X) \land z {hl}_{𝒢} (G) (Y) W) \to Y dist (G) Z = Y dist (G) z$
70	69	eqcomd	$⊢ ((((((φ \land ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y W ”⟩) \land x \in P) \land z \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ x Y z ”⟩) \land x {hl}_{𝒢} (G) (Y) X) \land z {hl}_{𝒢} (G) (Y) W) \to Y dist (G) z = Y dist (G) Z$
71	1 18 2 36 42 42 37 37 57 39 58 60 67 68 70	tgsegconeq	$⊢ ((((((φ \land ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y W ”⟩) \land x \in P) \land z \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ x Y z ”⟩) \land x {hl}_{𝒢} (G) (Y) X) \land z {hl}_{𝒢} (G) (Y) W) \to {pInv}_{𝒢} (G) (Y) (Z) = z$
72	55 71	oveq12d	$⊢ ((((((φ \land ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y W ”⟩) \land x \in P) \land z \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ x Y z ”⟩) \land x {hl}_{𝒢} (G) (Y) X) \land z {hl}_{𝒢} (G) (Y) W) \to X dist (G) {pInv}_{𝒢} (G) (Y) (Z) = x dist (G) z$
73	45 72	eqtr4d	$⊢ ((((((φ \land ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y W ”⟩) \land x \in P) \land z \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ x Y z ”⟩) \land x {hl}_{𝒢} (G) (Y) X) \land z {hl}_{𝒢} (G) (Y) W) \to X dist (G) Z = X dist (G) {pInv}_{𝒢} (G) (Y) (Z)$
74	1 18 2 19 20 3 10 5 13	israg	$⊢ φ \to (⟨“ X Y Z ”⟩ \in ∟_{𝒢} (G) \leftrightarrow X dist (G) Z = X dist (G) {pInv}_{𝒢} (G) (Y) (Z))$
75	74	ad6antr	$⊢ ((((((φ \land ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y W ”⟩) \land x \in P) \land z \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ x Y z ”⟩) \land x {hl}_{𝒢} (G) (Y) X) \land z {hl}_{𝒢} (G) (Y) W) \to (⟨“ X Y Z ”⟩ \in ∟_{𝒢} (G) \leftrightarrow X dist (G) Z = X dist (G) {pInv}_{𝒢} (G) (Y) (Z))$
76	73 75	mpbird	$⊢ ((((((φ \land ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y W ”⟩) \land x \in P) \land z \in P) \land ⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ x Y z ”⟩) \land x {hl}_{𝒢} (G) (Y) X) \land z {hl}_{𝒢} (G) (Y) W) \to ⟨“ X Y Z ”⟩ \in ∟_{𝒢} (G)$
77	76	3anasss	$⊢ ((((φ \land ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y W ”⟩) \land x \in P) \land z \in P) \land (⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ x Y z ”⟩ \land x {hl}_{𝒢} (G) (Y) X \land z {hl}_{𝒢} (G) (Y) W)) \to ⟨“ X Y Z ”⟩ \in ∟_{𝒢} (G)$
78	1 2 46 3 10 5 13 10 5 15	iscgra	$⊢ φ \to (⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y W ”⟩ \leftrightarrow \exists x \in P \exists z \in P (⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ x Y z ”⟩ \land x {hl}_{𝒢} (G) (Y) X \land z {hl}_{𝒢} (G) (Y) W))$
79	78	biimpa	$⊢ (φ \land ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y W ”⟩) \to \exists x \in P \exists z \in P (⟨“ X Y Z ”⟩ \sim_{𝒢} (G) ⟨“ x Y z ”⟩ \land x {hl}_{𝒢} (G) (Y) X \land z {hl}_{𝒢} (G) (Y) W)$
80	77 79	r19.29vva	$⊢ (φ \land ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y W ”⟩) \to ⟨“ X Y Z ”⟩ \in ∟_{𝒢} (G)$
81	35 80	impbida	$⊢ φ \to (⟨“ X Y Z ”⟩ \in ∟_{𝒢} (G) \leftrightarrow ⟨“ X Y Z ”⟩ \sim_{𝒢}^{∠} (G) ⟨“ X Y W ”⟩)$

Metamath Proof Explorer

Theorem ragsupplcgra

Proof