footexALT

Description: Alternative version of footex which minimization requires a notably long time. (Contributed by Thierry Arnoux, 19-Oct-2019) (New usage is discouraged.) (Proof modification is discouraged.)

	Ref	Expression
Hypotheses	isperp.p	$⊢ P = {Base}_{G}$
	isperp.d	$⊢ \underset{˙}{-} = dist (G)$
	isperp.i	$⊢ I = Itv (G)$
	isperp.l	$⊢ L = {Line}_{𝒢} (G)$
	isperp.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	isperp.a	$⊢ φ \to A \in ran L$
	foot.x	$⊢ φ \to C \in P$
	foot.y	$⊢ φ \to \neg C \in A$
Assertion	footexALT	$⊢ φ \to \exists x \in A (C L x) ⟂_{𝒢} (G) A$

Proof

Step	Hyp	Ref	Expression
1		isperp.p	$⊢ P = {Base}_{G}$
2		isperp.d	$⊢ \underset{˙}{-} = dist (G)$
3		isperp.i	$⊢ I = Itv (G)$
4		isperp.l	$⊢ L = {Line}_{𝒢} (G)$
5		isperp.g	$⊢ φ \to G \in 𝒢_{Tarski}$
6		isperp.a	$⊢ φ \to A \in ran L$
7		foot.x	$⊢ φ \to C \in P$
8		foot.y	$⊢ φ \to \neg C \in A$
9		eqid	$⊢ {pInv}_{𝒢} (G) = {pInv}_{𝒢} (G)$
10	5	ad3antrrr	$⊢ (((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \to G \in 𝒢_{Tarski}$
11	10	ad2antrr	$⊢ (((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \to G \in 𝒢_{Tarski}$
12	11	ad2antrr	$⊢ (((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \to G \in 𝒢_{Tarski}$
13	12	ad2antrr	$⊢ (((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \to G \in 𝒢_{Tarski}$
14	13	ad2antrr	$⊢ (((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \to G \in 𝒢_{Tarski}$
15	14	ad2antrr	$⊢ (((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to G \in 𝒢_{Tarski}$
16		eqid	$⊢ {pInv}_{𝒢} (G) (x) = {pInv}_{𝒢} (G) (x)$
17	7	ad3antrrr	$⊢ (((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \to C \in P$
18	17	ad2antrr	$⊢ (((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \to C \in P$
19	18	ad6antr	$⊢ (((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \to C \in P$
20	19	ad2antrr	$⊢ (((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to C \in P$
21		simplr	$⊢ (((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to d \in P$
22		simp-4r	$⊢ (((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \to y \in P$
23	22	ad2antrr	$⊢ (((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \to y \in P$
24	23	ad2antrr	$⊢ (((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \to y \in P$
25	24	ad2antrr	$⊢ (((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to y \in P$
26		simprr	$⊢ (((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to y \underset{˙}{-} d = y \underset{˙}{-} C$
27	26	eqcomd	$⊢ (((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to y \underset{˙}{-} C = y \underset{˙}{-} d$
28	1 2 3 4 9 15 16 20 21 25 27	midexlem	$⊢ (((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to \exists x \in P d = {pInv}_{𝒢} (G) (x) (C)$
29	15	adantr	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to G \in 𝒢_{Tarski}$
30	25	adantr	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to y \in P$
31		simp-6r	$⊢ (((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to z \in P$
32	31	adantr	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to z \in P$
33		simprl	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to x \in P$
34		simp-4r	$⊢ (((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \to p \in P$
35	34	ad4antr	$⊢ (((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to p \in P$
36	35	adantr	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to p \in P$
37		simp-5r	$⊢ (((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)$
38	37	simprd	$⊢ (((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to y \underset{˙}{-} z = y \underset{˙}{-} p$
39	38	eqcomd	$⊢ (((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to y \underset{˙}{-} p = y \underset{˙}{-} z$
40	39	adantr	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to y \underset{˙}{-} p = y \underset{˙}{-} z$
41		simp-7r	$⊢ (((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to C = {pInv}_{𝒢} (G) (p) (y)$
42	41	adantr	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to C = {pInv}_{𝒢} (G) (p) (y)$
43		simpllr	$⊢ (((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \to a \in P$
44	43	ad2antrr	$⊢ (((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \to a \in P$
45	44	ad2antrr	$⊢ (((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \to a \in P$
46	45	ad2antrr	$⊢ (((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \to a \in P$
47	46	ad4antr	$⊢ (((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to a \in P$
48		simplr	$⊢ (((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \to b \in P$
49	48	ad10antr	$⊢ (((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to b \in P$
50		simp-11r	$⊢ (((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to (A = a L b \land a \neq b)$
51	50	simprd	$⊢ (((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to a \neq b$
52	51	necomd	$⊢ (((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to b \neq a$
53		simp-9r	$⊢ (((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)$
54	53	simpld	$⊢ (((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to a \in (b I y)$
55	1 3 4 15 49 47 25 52 54	btwnlng3	$⊢ (((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to y \in (b L a)$
56	1 3 4 15 47 49 25 51 55	lncom	$⊢ (((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to y \in (a L b)$
57	50	simpld	$⊢ (((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to A = a L b$
58	56 57	eleqtrrd	$⊢ (((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to y \in A$
59	58	adantr	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to y \in A$
60	8	ad3antrrr	$⊢ (((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \to \neg C \in A$
61	60	ad10antr	$⊢ (((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to \neg C \in A$
62	61	adantr	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to \neg C \in A$
63		nelne2	$⊢ (y \in A \land \neg C \in A) \to y \neq C$
64	59 62 63	syl2anc	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to y \neq C$
65	64	necomd	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to C \neq y$
66	42 65	eqnetrrd	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to {pInv}_{𝒢} (G) (p) (y) \neq y$
67		eqid	$⊢ {pInv}_{𝒢} (G) (p) = {pInv}_{𝒢} (G) (p)$
68	1 2 3 4 9 29 36 67 30	mirinv	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to ({pInv}_{𝒢} (G) (p) (y) = y \leftrightarrow p = y)$
69	68	necon3bid	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to ({pInv}_{𝒢} (G) (p) (y) \neq y \leftrightarrow p \neq y)$
70	66 69	mpbid	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to p \neq y$
71	70	necomd	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to y \neq p$
72	1 2 3 29 30 36 30 32 40 71	tgcgrneq	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to y \neq z$
73	72	necomd	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to z \neq y$
74		eqid	$⊢ {pInv}_{𝒢} (G) (z) = {pInv}_{𝒢} (G) (z)$
75		simp-4r	$⊢ (((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to q \in P$
76	75	adantr	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to q \in P$
77		simp-4r	$⊢ (((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \to z \in P$
78		simplr	$⊢ (((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \to q \in P$
79	1 2 3 4 9 14 77 74 78	mircl	$⊢ (((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \to {pInv}_{𝒢} (G) (z) (q) \in P$
80	79	ad3antrrr	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to {pInv}_{𝒢} (G) (z) (q) \in P$
81	20	adantr	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to C \in P$
82		simpllr	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to d \in P$
83	1 2 3 4 9 29 36 67 30	mirbtwn	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to p \in ({pInv}_{𝒢} (G) (p) (y) I y)$
84	42	oveq1d	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to C I y = {pInv}_{𝒢} (G) (p) (y) I y$
85	83 84	eleqtrrd	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to p \in (C I y)$
86		simpllr	$⊢ (((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)$
87	86	simpld	$⊢ (((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to y \in (p I q)$
88	87	adantr	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to y \in (p I q)$
89	1 2 3 29 81 36 30 76 70 85 88	tgbtwnouttr2	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to y \in (C I q)$
90	1 2 3 29 81 30 76 89	tgbtwncom	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to y \in (q I C)$
91		simplrl	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to y \in ({pInv}_{𝒢} (G) (z) (q) I d)$
92		eqid	$⊢ \sim_{𝒢} (G) = \sim_{𝒢} (G)$
93	53	simprd	$⊢ (((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to a \underset{˙}{-} y = a \underset{˙}{-} C$
94	41	oveq2d	$⊢ (((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to a \underset{˙}{-} C = a \underset{˙}{-} {pInv}_{𝒢} (G) (p) (y)$
95	93 94	eqtrd	$⊢ (((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to a \underset{˙}{-} y = a \underset{˙}{-} {pInv}_{𝒢} (G) (p) (y)$
96	1 2 3 4 9 15 47 35 25	israg	$⊢ (((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to (⟨“ a p y ”⟩ \in ∟_{𝒢} (G) \leftrightarrow a \underset{˙}{-} y = a \underset{˙}{-} {pInv}_{𝒢} (G) (p) (y))$
97	95 96	mpbird	$⊢ (((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to ⟨“ a p y ”⟩ \in ∟_{𝒢} (G)$
98	86	simprd	$⊢ (((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to y \underset{˙}{-} q = y \underset{˙}{-} a$
99	1 2 3 15 47 25 47 20 93	tgcgrcomlr	$⊢ (((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to y \underset{˙}{-} a = C \underset{˙}{-} a$
100	98 99	eqtr2d	$⊢ (((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to C \underset{˙}{-} a = y \underset{˙}{-} q$
101	1 3 4 15 47 49 51	tglinerflx1	$⊢ (((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to a \in (a L b)$
102	101 57	eleqtrrd	$⊢ (((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to a \in A$
103		nelne2	$⊢ (a \in A \land \neg C \in A) \to a \neq C$
104	102 61 103	syl2anc	$⊢ (((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to a \neq C$
105	104	necomd	$⊢ (((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to C \neq a$
106	1 2 3 15 20 47 25 75 100 105	tgcgrneq	$⊢ (((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to y \neq q$
107	106	necomd	$⊢ (((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to q \neq y$
108	1 2 3 15 35 25 75 87	tgbtwncom	$⊢ (((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to y \in (q I p)$
109	37	simpld	$⊢ (((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to y \in (a I z)$
110	1 2 3 15 25 75 25 47 98	tgcgrcomlr	$⊢ (((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to q \underset{˙}{-} y = a \underset{˙}{-} y$
111	1 2 3 15 75 47	axtgcgrrflx	$⊢ (((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to q \underset{˙}{-} a = a \underset{˙}{-} q$
112	98	eqcomd	$⊢ (((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to y \underset{˙}{-} a = y \underset{˙}{-} q$
113	1 2 3 15 75 25 35 47 25 31 47 75 107 108 109 110 39 111 112	axtg5seg	$⊢ (((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to p \underset{˙}{-} a = z \underset{˙}{-} q$
114	1 2 3 15 35 47 31 75 113	tgcgrcomlr	$⊢ (((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to a \underset{˙}{-} p = q \underset{˙}{-} z$
115	1 2 3 15 25 35 25 31 39	tgcgrcomlr	$⊢ (((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to p \underset{˙}{-} y = z \underset{˙}{-} y$
116	1 2 92 15 47 35 25 75 31 25 114 115 112	trgcgr	$⊢ (((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to ⟨“ a p y ”⟩ \sim_{𝒢} (G) ⟨“ q z y ”⟩$
117	1 2 3 4 9 15 47 35 25 92 75 31 25 97 116	ragcgr	$⊢ (((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to ⟨“ q z y ”⟩ \in ∟_{𝒢} (G)$
118	1 2 3 4 9 15 75 31 25 117	ragcom	$⊢ (((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to ⟨“ y z q ”⟩ \in ∟_{𝒢} (G)$
119	1 2 3 4 9 15 25 31 75	israg	$⊢ (((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to (⟨“ y z q ”⟩ \in ∟_{𝒢} (G) \leftrightarrow y \underset{˙}{-} q = y \underset{˙}{-} {pInv}_{𝒢} (G) (z) (q))$
120	118 119	mpbid	$⊢ (((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to y \underset{˙}{-} q = y \underset{˙}{-} {pInv}_{𝒢} (G) (z) (q)$
121	120	adantr	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to y \underset{˙}{-} q = y \underset{˙}{-} {pInv}_{𝒢} (G) (z) (q)$
122	27	adantr	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to y \underset{˙}{-} C = y \underset{˙}{-} d$
123		eqidd	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to {pInv}_{𝒢} (G) (z) (q) = {pInv}_{𝒢} (G) (z) (q)$
124		simprr	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to d = {pInv}_{𝒢} (G) (x) (C)$
125	1 2 3 4 9 29 74 16 76 80 30 81 82 32 33 90 91 121 122 123 124	krippen	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to y \in (z I x)$
126	1 3 4 29 32 30 33 73 125	btwnlng3	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to x \in (z L y)$
127	1 3 4 29 30 32 33 72 126	lncom	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to x \in (y L z)$
128	6	ad5antr	$⊢ (((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \to A \in ran L$
129	128	ad9antr	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to A \in ran L$
130	47	adantr	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to a \in P$
131	93	adantr	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to a \underset{˙}{-} y = a \underset{˙}{-} C$
132	131	eqcomd	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to a \underset{˙}{-} C = a \underset{˙}{-} y$
133	104	adantr	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to a \neq C$
134	1 2 3 29 130 81 130 30 132 133	tgcgrneq	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to a \neq y$
135	109	adantr	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to y \in (a I z)$
136	1 3 4 29 130 30 32 134 135	btwnlng3	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to z \in (a L y)$
137	102	adantr	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to a \in A$
138	1 3 4 29 130 30 134 134 129 137 59	tglinethru	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to A = a L y$
139	136 138	eleqtrrd	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to z \in A$
140	1 3 4 29 30 32 72 72 129 59 139	tglinethru	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to A = y L z$
141	127 140	eleqtrrd	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to x \in A$
142		nelne2	$⊢ (x \in A \land \neg C \in A) \to x \neq C$
143	141 62 142	syl2anc	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to x \neq C$
144	143	necomd	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to C \neq x$
145	1 3 4 29 81 33 144	tgelrnln	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to C L x \in ran L$
146	1 3 4 29 81 33 144	tglinerflx2	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to x \in (C L x)$
147	146 141	elind	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to x \in ((C L x) \cap A)$
148	1 3 4 29 81 33 144	tglinerflx1	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to C \in (C L x)$
149	29	adantr	$⊢ (((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \land y = x) \to G \in 𝒢_{Tarski}$
150	130	adantr	$⊢ (((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \land y = x) \to a \in P$
151	30	adantr	$⊢ (((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \land y = x) \to y \in P$
152	36	adantr	$⊢ (((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \land y = x) \to p \in P$
153	81	adantr	$⊢ (((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \land y = x) \to C \in P$
154		eqidd	$⊢ (((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \land y = x) \to C = C$
155		simpr	$⊢ (((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \land y = x) \to y = x$
156		eqidd	$⊢ (((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \land y = x) \to a = a$
157	154 155 156	s3eqd	$⊢ (((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \land y = x) \to ⟨“ C y a ”⟩ = ⟨“ C x a ”⟩$
158	33	adantr	$⊢ (((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \land y = x) \to x \in P$
159	32	adantr	$⊢ (((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \land y = x) \to z \in P$
160	107	adantr	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to q \neq y$
161	1 2 3 29 30 76 30 80 121	tgcgrcomlr	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to q \underset{˙}{-} y = {pInv}_{𝒢} (G) (z) (q) \underset{˙}{-} y$
162	1 2 3 4 9 29 32 74 76	mircgr	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to z \underset{˙}{-} {pInv}_{𝒢} (G) (z) (q) = z \underset{˙}{-} q$
163	162	eqcomd	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to z \underset{˙}{-} q = z \underset{˙}{-} {pInv}_{𝒢} (G) (z) (q)$
164	1 2 3 29 32 76 32 80 163	tgcgrcomlr	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to q \underset{˙}{-} z = {pInv}_{𝒢} (G) (z) (q) \underset{˙}{-} z$
165		eqidd	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to y \underset{˙}{-} z = y \underset{˙}{-} z$
166	1 2 3 29 76 30 81 80 30 82 32 32 160 90 91 161 122 164 165	axtg5seg	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to C \underset{˙}{-} z = d \underset{˙}{-} z$
167	1 2 3 29 81 32 82 32 166	tgcgrcomlr	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to z \underset{˙}{-} C = z \underset{˙}{-} d$
168	124	oveq2d	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to z \underset{˙}{-} d = z \underset{˙}{-} {pInv}_{𝒢} (G) (x) (C)$
169	167 168	eqtrd	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to z \underset{˙}{-} C = z \underset{˙}{-} {pInv}_{𝒢} (G) (x) (C)$
170	1 2 3 4 9 29 32 33 81	israg	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to (⟨“ z x C ”⟩ \in ∟_{𝒢} (G) \leftrightarrow z \underset{˙}{-} C = z \underset{˙}{-} {pInv}_{𝒢} (G) (x) (C))$
171	169 170	mpbird	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to ⟨“ z x C ”⟩ \in ∟_{𝒢} (G)$
172	171	adantr	$⊢ (((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \land y = x) \to ⟨“ z x C ”⟩ \in ∟_{𝒢} (G)$
173	73	adantr	$⊢ (((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \land y = x) \to z \neq y$
174	173 155	neeqtrd	$⊢ (((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \land y = x) \to z \neq x$
175	132	adantr	$⊢ (((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \land y = x) \to a \underset{˙}{-} C = a \underset{˙}{-} y$
176	133	adantr	$⊢ (((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \land y = x) \to a \neq C$
177	1 2 3 149 150 153 150 151 175 176	tgcgrneq	$⊢ (((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \land y = x) \to a \neq y$
178	177	necomd	$⊢ (((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \land y = x) \to y \neq a$
179	136	adantr	$⊢ (((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \land y = x) \to z \in (a L y)$
180	1 3 4 149 151 150 159 178 179	lncom	$⊢ (((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \land y = x) \to z \in (y L a)$
181	155	oveq1d	$⊢ (((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \land y = x) \to y L a = x L a$
182	180 181	eleqtrd	$⊢ (((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \land y = x) \to z \in (x L a)$
183	182	orcd	$⊢ (((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \land y = x) \to (z \in (x L a) \lor x = a)$
184	1 2 3 4 9 149 159 158 153 150 172 174 183	ragcol	$⊢ (((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \land y = x) \to ⟨“ a x C ”⟩ \in ∟_{𝒢} (G)$
185	1 2 3 4 9 149 150 158 153 184	ragcom	$⊢ (((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \land y = x) \to ⟨“ C x a ”⟩ \in ∟_{𝒢} (G)$
186	157 185	eqeltrd	$⊢ (((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \land y = x) \to ⟨“ C y a ”⟩ \in ∟_{𝒢} (G)$
187	65	adantr	$⊢ (((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \land y = x) \to C \neq y$
188	1 2 3 29 81 36 30 85	tgbtwncom	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to p \in (y I C)$
189	1 4 3 29 30 36 81 188	btwncolg3	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to (C \in (y L p) \lor y = p)$
190	189	adantr	$⊢ (((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \land y = x) \to (C \in (y L p) \lor y = p)$
191	1 2 3 4 9 149 153 151 150 152 186 187 190	ragcol	$⊢ (((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \land y = x) \to ⟨“ p y a ”⟩ \in ∟_{𝒢} (G)$
192	1 2 3 4 9 149 152 151 150 191	ragcom	$⊢ (((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \land y = x) \to ⟨“ a y p ”⟩ \in ∟_{𝒢} (G)$
193	97	ad2antrr	$⊢ (((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \land y = x) \to ⟨“ a p y ”⟩ \in ∟_{𝒢} (G)$
194	1 2 3 4 9 149 150 151 152 192 193	ragflat	$⊢ (((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \land y = x) \to y = p$
195	71	adantr	$⊢ (((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \land y = x) \to y \neq p$
196	195	neneqd	$⊢ (((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \land y = x) \to \neg y = p$
197	194 196	pm2.65da	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to \neg y = x$
198	197	neqned	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to y \neq x$
199	124	oveq2d	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to y \underset{˙}{-} d = y \underset{˙}{-} {pInv}_{𝒢} (G) (x) (C)$
200	122 199	eqtrd	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to y \underset{˙}{-} C = y \underset{˙}{-} {pInv}_{𝒢} (G) (x) (C)$
201	1 2 3 4 9 29 30 33 81	israg	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to (⟨“ y x C ”⟩ \in ∟_{𝒢} (G) \leftrightarrow y \underset{˙}{-} C = y \underset{˙}{-} {pInv}_{𝒢} (G) (x) (C))$
202	200 201	mpbird	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to ⟨“ y x C ”⟩ \in ∟_{𝒢} (G)$
203	1 2 3 4 9 29 30 33 81 202	ragcom	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to ⟨“ C x y ”⟩ \in ∟_{𝒢} (G)$
204	1 2 3 4 29 145 129 147 148 59 144 198 203	ragperp	$⊢ ((((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to (C L x) ⟂_{𝒢} (G) A$
205	28 141 204	reximssdv	$⊢ (((((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to \exists x \in A (C L x) ⟂_{𝒢} (G) A$
206	1 2 3 14 79 24 24 19	axtgsegcon	$⊢ (((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \to \exists d \in P (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)$
207	205 206	r19.29a	$⊢ (((((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \to \exists x \in A (C L x) ⟂_{𝒢} (G) A$
208	1 2 3 13 34 23 23 46	axtgsegcon	$⊢ (((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \to \exists q \in P (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)$
209	207 208	r19.29a	$⊢ (((((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \to \exists x \in A (C L x) ⟂_{𝒢} (G) A$
210		simplr	$⊢ (((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \to p \in P$
211	1 2 3 12 45 22 22 210	axtgsegcon	$⊢ (((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \to \exists z \in P (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)$
212	209 211	r19.29a	$⊢ (((((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \to \exists x \in A (C L x) ⟂_{𝒢} (G) A$
213		simplr	$⊢ (((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \to y \in P$
214		simprr	$⊢ (((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \to a \underset{˙}{-} y = a \underset{˙}{-} C$
215	1 2 3 4 9 11 67 213 18 44 214	midexlem	$⊢ (((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \to \exists p \in P C = {pInv}_{𝒢} (G) (p) (y)$
216	212 215	r19.29a	$⊢ (((((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \land y \in P) \land (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)) \to \exists x \in A (C L x) ⟂_{𝒢} (G) A$
217	1 2 3 10 48 43 43 17	axtgsegcon	$⊢ (((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \to \exists y \in P (a \in (b I y) \land a \underset{˙}{-} y = a \underset{˙}{-} C)$
218	216 217	r19.29a	$⊢ (((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \to \exists x \in A (C L x) ⟂_{𝒢} (G) A$
219	1 3 4 5 6	tgisline	$⊢ φ \to \exists a \in P \exists b \in P (A = a L b \land a \neq b)$
220	218 219	r19.29vva	$⊢ φ \to \exists x \in A (C L x) ⟂_{𝒢} (G) A$

Metamath Proof Explorer

Theorem footexALT

Proof