footex

Description: From a point C outside of a line A , there exists a point x on A such that ( C L x ) is perpendicular to A . This point is unique, see foot . (Contributed by Thierry Arnoux, 19-Oct-2019) (Revised by Thierry Arnoux, 1-Jul-2023)

	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	footex	$⊢ φ \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	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 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)) \land p \in P) \land C = {pInv}_{𝒢} (G) (p) (y)) \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)) \land z \in P) \land (y \in (a I z) \land y \underset{˙}{-} z = y \underset{˙}{-} p)) \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)) \land q \in P) \land (y \in (p I q) \land y \underset{˙}{-} q = y \underset{˙}{-} a)) \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)) \land d \in P) \land (y \in ({pInv}_{𝒢} (G) (z) (q) I d) \land y \underset{˙}{-} d = y \underset{˙}{-} C)) \to G \in 𝒢_{Tarski}$
15		eqid	$⊢ {pInv}_{𝒢} (G) (x) = {pInv}_{𝒢} (G) (x)$
16	7	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 C \in P$
17	16	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$
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)) \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$
19		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$
20		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$
21	20	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$
22	21	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$
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)) \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$
24		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$
25	24	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$
26	1 2 3 4 9 14 15 18 19 23 25	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)$
27	12	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)) \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}$
28	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$
29	28	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$
30	18	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$
31	8	ad3antrrr	$⊢ (((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \to \neg C \in A$
32	31	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$
33	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))) \to \neg C \in A$
34		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)) \to a \in P$
35	34	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$
36	35	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)) \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$
37		simplr	$⊢ (((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \to b \in P$
38	37	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$
39	38	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 b \in P$
40		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$
41	40	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)) \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$
42		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$
43	21	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)) \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$
44		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)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to z \in P$
45		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$
46		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)$
47	46	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$
48	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 = a L b$
49	46	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$
50	49	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 b$
51		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)$
52	51	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)$
53	52	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 (b I y)$
54	51	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$
55	54	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$
56		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)$
57	56	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)$
58		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)$
59	58	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)$
60	59	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)$
61	58	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$
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 y \underset{˙}{-} z = y \underset{˙}{-} p$
63		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)) \land (x \in P \land d = {pInv}_{𝒢} (G) (x) (C))) \to q \in P$
64		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)$
65	64	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)$
66	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))) \to y \in (p I q)$
67	64	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$
68	67	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{˙}{-} a$
69		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)$
70	24	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{˙}{-} d = y \underset{˙}{-} C$
71		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)$
72	1 2 3 4 27 29 30 33 36 39 41 42 43 44 45 48 50 53 55 57 60 62 63 66 68 69 70 71	footexlem1	$⊢ ((((((((((((((φ \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$
73	1 2 3 4 27 29 30 33 36 39 41 42 43 44 45 48 50 53 55 57 60 62 63 66 68 69 70 71	footexlem2	$⊢ ((((((((((((((φ \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$
74	26 72 73	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$
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)) \to z \in P$
76		eqid	$⊢ {pInv}_{𝒢} (G) (z) = {pInv}_{𝒢} (G) (z)$
77		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$
78	1 2 3 4 9 13 75 76 77	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$
79	1 2 3 13 78 22 22 17	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)$
80	74 79	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$
81	1 2 3 12 40 21 21 35	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)$
82	80 81	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$
83		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$
84	1 2 3 11 34 20 20 83	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)$
85	82 84	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$
86		eqid	$⊢ {pInv}_{𝒢} (G) (p) = {pInv}_{𝒢} (G) (p)$
87		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$
88		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)) \to a \in P$
89		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$
90	1 2 3 4 9 10 86 87 16 88 89	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)$
91	85 90	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$
92	5	ad3antrrr	$⊢ (((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \to G \in 𝒢_{Tarski}$
93		simpllr	$⊢ (((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \to a \in P$
94	7	ad3antrrr	$⊢ (((φ \land a \in P) \land b \in P) \land (A = a L b \land a \neq b)) \to C \in P$
95	1 2 3 92 37 93 93 94	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)$
96	91 95	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$
97	1 3 4 5 6	tgisline	$⊢ φ \to \exists a \in P \exists b \in P (A = a L b \land a \neq b)$
98	96 97	r19.29vva	$⊢ φ \to \exists x \in A (C L x) ⟂_{𝒢} (G) A$

Metamath Proof Explorer

Theorem footex

Proof