# Metamath Proof Explorer

## Theorem colperpexlem3

Description: Lemma for colperpex . Case 1 of theorem 8.21 of Schwabhauser p. 63. (Contributed by Thierry Arnoux, 20-Nov-2019)

Ref Expression
Hypotheses colperpex.p ${⊢}{P}={\mathrm{Base}}_{{G}}$
colperpex.d
colperpex.i ${⊢}{I}=\mathrm{Itv}\left({G}\right)$
colperpex.l ${⊢}{L}={Line}_{𝒢}\left({G}\right)$
colperpex.g ${⊢}{\phi }\to {G}\in {𝒢}_{\mathrm{Tarski}}$
colperpex.1 ${⊢}{\phi }\to {A}\in {P}$
colperpex.2 ${⊢}{\phi }\to {B}\in {P}$
colperpex.3 ${⊢}{\phi }\to {C}\in {P}$
colperpex.4 ${⊢}{\phi }\to {A}\ne {B}$
colperpexlem3.1 ${⊢}{\phi }\to ¬{C}\in \left({A}{L}{B}\right)$
Assertion colperpexlem3 ${⊢}{\phi }\to \exists {p}\in {P}\phantom{\rule{.4em}{0ex}}\left(\left({A}{L}{p}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\wedge \exists {t}\in {P}\phantom{\rule{.4em}{0ex}}\left(\left({t}\in \left({A}{L}{B}\right)\vee {A}={B}\right)\wedge {t}\in \left({C}{I}{p}\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 colperpex.p ${⊢}{P}={\mathrm{Base}}_{{G}}$
2 colperpex.d
3 colperpex.i ${⊢}{I}=\mathrm{Itv}\left({G}\right)$
4 colperpex.l ${⊢}{L}={Line}_{𝒢}\left({G}\right)$
5 colperpex.g ${⊢}{\phi }\to {G}\in {𝒢}_{\mathrm{Tarski}}$
6 colperpex.1 ${⊢}{\phi }\to {A}\in {P}$
7 colperpex.2 ${⊢}{\phi }\to {B}\in {P}$
8 colperpex.3 ${⊢}{\phi }\to {C}\in {P}$
9 colperpex.4 ${⊢}{\phi }\to {A}\ne {B}$
10 colperpexlem3.1 ${⊢}{\phi }\to ¬{C}\in \left({A}{L}{B}\right)$
11 eqid ${⊢}{pInv}_{𝒢}\left({G}\right)={pInv}_{𝒢}\left({G}\right)$
12 5 ad2antrr ${⊢}\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\to {G}\in {𝒢}_{\mathrm{Tarski}}$
13 eqid ${⊢}{pInv}_{𝒢}\left({G}\right)\left({p}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)$
14 1 3 4 5 6 7 9 tgelrnln ${⊢}{\phi }\to {A}{L}{B}\in \mathrm{ran}{L}$
15 14 ad2antrr ${⊢}\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\to {A}{L}{B}\in \mathrm{ran}{L}$
16 simplr ${⊢}\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\to {x}\in \left({A}{L}{B}\right)$
17 1 4 3 12 15 16 tglnpt ${⊢}\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\to {x}\in {P}$
18 eqid ${⊢}{pInv}_{𝒢}\left({G}\right)\left({x}\right)={pInv}_{𝒢}\left({G}\right)\left({x}\right)$
19 8 ad2antrr ${⊢}\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\to {C}\in {P}$
20 1 2 3 4 11 12 17 18 19 mircl ${⊢}\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\to {pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\in {P}$
21 6 ad2antrr ${⊢}\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\to {A}\in {P}$
22 eqid ${⊢}{pInv}_{𝒢}\left({G}\right)\left({A}\right)={pInv}_{𝒢}\left({G}\right)\left({A}\right)$
23 1 2 3 4 11 12 21 22 19 mircl ${⊢}\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\to {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)\in {P}$
24 1 2 3 4 11 12 21 22 19 mircgr
25 7 ad2antrr ${⊢}\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\to {B}\in {P}$
26 10 ad2antrr ${⊢}\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\to ¬{C}\in \left({A}{L}{B}\right)$
27 nelne2 ${⊢}\left({x}\in \left({A}{L}{B}\right)\wedge ¬{C}\in \left({A}{L}{B}\right)\right)\to {x}\ne {C}$
28 16 26 27 syl2anc ${⊢}\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\to {x}\ne {C}$
29 1 3 4 12 17 19 28 tgelrnln ${⊢}\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\to {x}{L}{C}\in \mathrm{ran}{L}$
30 1 3 4 12 17 19 28 tglinecom ${⊢}\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\to {x}{L}{C}={C}{L}{x}$
31 simpr ${⊢}\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\to \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)$
32 30 31 eqbrtrd ${⊢}\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\to \left({x}{L}{C}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)$
33 1 2 3 4 12 29 15 32 perpcom ${⊢}\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\to \left({A}{L}{B}\right){⟂}_{𝒢}\left({G}\right)\left({x}{L}{C}\right)$
34 1 2 3 4 12 21 25 16 19 33 perprag ${⊢}\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\to ⟨“{A}{x}{C}”⟩\in {∟}_{𝒢}\left({G}\right)$
35 1 2 3 4 11 12 21 17 19 israg
36 34 35 mpbid
37 24 36 eqtr2d
38 1 2 3 4 11 12 13 20 23 21 37 midexlem ${⊢}\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\to \exists {p}\in {P}\phantom{\rule{.4em}{0ex}}{pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)$
39 12 ad2antrr ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\to {G}\in {𝒢}_{\mathrm{Tarski}}$
40 23 ad2antrr ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\to {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)\in {P}$
41 21 ad2antrr ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\to {A}\in {P}$
42 19 ad2antrr ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\to {C}\in {P}$
43 20 ad2antrr ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\to {pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\in {P}$
44 17 ad2antrr ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\to {x}\in {P}$
45 simplr ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\to {p}\in {P}$
46 1 2 3 4 11 39 41 22 42 mirbtwn ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\to {A}\in \left({pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right){I}{C}\right)$
47 1 2 3 4 11 39 44 18 42 mirbtwn ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\to {x}\in \left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right){I}{C}\right)$
48 1 2 3 4 11 39 45 13 43 mirbtwn ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\to {p}\in \left({pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right){I}{pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)$
49 simpr ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\to {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)$
50 49 eqcomd ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\to {pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)={pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)$
51 50 oveq1d ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\to {pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right){I}{pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right){I}{pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)$
52 48 51 eleqtrd ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\to {p}\in \left({pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right){I}{pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)$
53 1 2 3 39 40 41 42 43 44 45 46 47 52 tgtrisegint ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\to \exists {t}\in {P}\phantom{\rule{.4em}{0ex}}\left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)$
54 39 ad3antrrr ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}={A}\right)\to {G}\in {𝒢}_{\mathrm{Tarski}}$
55 41 ad3antrrr ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}={A}\right)\to {A}\in {P}$
56 simpllr ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}={A}\right)\to {t}\in {P}$
57 simplrr ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}={A}\right)\to {t}\in \left({A}{I}{x}\right)$
58 simpr ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}={A}\right)\to {x}={A}$
59 58 oveq2d ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}={A}\right)\to {A}{I}{x}={A}{I}{A}$
60 57 59 eleqtrd ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}={A}\right)\to {t}\in \left({A}{I}{A}\right)$
61 1 2 3 54 55 56 60 axtgbtwnid ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}={A}\right)\to {A}={t}$
62 61 eqcomd ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}={A}\right)\to {t}={A}$
63 62 oveq1d ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}={A}\right)\to {t}{L}{p}={A}{L}{p}$
64 50 ad3antrrr ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}={A}\right)\to {pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)={pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)$
65 58 fveq2d ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}={A}\right)\to {pInv}_{𝒢}\left({G}\right)\left({x}\right)={pInv}_{𝒢}\left({G}\right)\left({A}\right)$
66 65 fveq1d ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}={A}\right)\to {pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)$
67 64 66 eqtr4d ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}={A}\right)\to {pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)={pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)$
68 45 ad3antrrr ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}={A}\right)\to {p}\in {P}$
69 43 ad3antrrr ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}={A}\right)\to {pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\in {P}$
70 1 2 3 4 11 54 68 13 69 mirinv ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}={A}\right)\to \left({pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)={pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)↔{p}={pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)$
71 67 70 mpbid ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}={A}\right)\to {p}={pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)$
72 44 ad3antrrr ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}={A}\right)\to {x}\in {P}$
73 58 oveq1d ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}={A}\right)\to {x}{I}{x}={A}{I}{x}$
74 57 73 eleqtrrd ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}={A}\right)\to {t}\in \left({x}{I}{x}\right)$
75 1 2 3 54 72 56 74 axtgbtwnid ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}={A}\right)\to {x}={t}$
76 75 eqcomd ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}={A}\right)\to {t}={x}$
77 71 76 oveq12d ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}={A}\right)\to {p}{L}{t}={pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right){L}{x}$
78 34 ad2antrr ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\to ⟨“{A}{x}{C}”⟩\in {∟}_{𝒢}\left({G}\right)$
79 1 2 3 4 11 39 45 13 43 50 mircom ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\to {pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)\right)={pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)$
80 28 ad2antrr ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\to {x}\ne {C}$
81 1 2 3 4 39 11 22 18 13 41 44 42 45 78 79 80 colperpexlem2 ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\to {A}\ne {p}$
82 81 ad3antrrr ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}={A}\right)\to {A}\ne {p}$
83 62 82 eqnetrd ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}={A}\right)\to {t}\ne {p}$
84 1 3 4 54 56 68 83 tglinecom ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}={A}\right)\to {t}{L}{p}={p}{L}{t}$
85 42 ad3antrrr ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}={A}\right)\to {C}\in {P}$
86 80 ad3antrrr ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}={A}\right)\to {x}\ne {C}$
87 54 adantr ${⊢}\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}={A}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)={x}\right)\to {G}\in {𝒢}_{\mathrm{Tarski}}$
88 72 adantr ${⊢}\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}={A}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)={x}\right)\to {x}\in {P}$
89 85 adantr ${⊢}\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}={A}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)={x}\right)\to {C}\in {P}$
90 1 2 3 4 11 87 88 18 mircinv ${⊢}\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}={A}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)={x}\right)\to {pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({x}\right)={x}$
91 simpr ${⊢}\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}={A}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)={x}\right)\to {pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)={x}$
92 90 91 eqtr4d ${⊢}\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}={A}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)={x}\right)\to {pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({x}\right)={pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)$
93 1 2 3 4 11 87 88 18 88 89 92 mireq ${⊢}\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}={A}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)={x}\right)\to {x}={C}$
94 86 adantr ${⊢}\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}={A}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)={x}\right)\to {x}\ne {C}$
95 94 neneqd ${⊢}\left(\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}={A}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)={x}\right)\to ¬{x}={C}$
96 93 95 pm2.65da ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}={A}\right)\to ¬{pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)={x}$
97 96 neqned ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}={A}\right)\to {pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\ne {x}$
98 47 ad3antrrr ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}={A}\right)\to {x}\in \left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right){I}{C}\right)$
99 1 3 4 54 72 85 69 86 98 btwnlng2 ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}={A}\right)\to {pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\in \left({x}{L}{C}\right)$
100 1 3 4 54 72 85 86 69 97 99 tglineelsb2 ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}={A}\right)\to {x}{L}{C}={x}{L}{pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)$
101 28 necomd ${⊢}\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\to {C}\ne {x}$
102 101 ad5antr ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}={A}\right)\to {C}\ne {x}$
103 1 3 4 54 85 72 102 tglinecom ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}={A}\right)\to {C}{L}{x}={x}{L}{C}$
104 1 3 4 54 69 72 97 tglinecom ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}={A}\right)\to {pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right){L}{x}={x}{L}{pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)$
105 100 103 104 3eqtr4d ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}={A}\right)\to {C}{L}{x}={pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right){L}{x}$
106 77 84 105 3eqtr4d ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}={A}\right)\to {t}{L}{p}={C}{L}{x}$
107 63 106 eqtr3d ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}={A}\right)\to {A}{L}{p}={C}{L}{x}$
108 31 ad5antr ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}={A}\right)\to \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)$
109 107 108 eqbrtrd ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}={A}\right)\to \left({A}{L}{p}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)$
110 39 ad3antrrr ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}\ne {A}\right)\to {G}\in {𝒢}_{\mathrm{Tarski}}$
111 41 ad3antrrr ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}\ne {A}\right)\to {A}\in {P}$
112 45 ad3antrrr ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}\ne {A}\right)\to {p}\in {P}$
113 81 ad3antrrr ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}\ne {A}\right)\to {A}\ne {p}$
114 1 3 4 110 111 112 113 tgelrnln ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}\ne {A}\right)\to {A}{L}{p}\in \mathrm{ran}{L}$
115 15 ad5antr ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}\ne {A}\right)\to {A}{L}{B}\in \mathrm{ran}{L}$
116 1 3 4 110 111 112 113 tglinerflx1 ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}\ne {A}\right)\to {A}\in \left({A}{L}{p}\right)$
117 9 ad2antrr ${⊢}\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\to {A}\ne {B}$
118 1 3 4 12 21 25 117 tglinerflx1 ${⊢}\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\to {A}\in \left({A}{L}{B}\right)$
119 118 ad5antr ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}\ne {A}\right)\to {A}\in \left({A}{L}{B}\right)$
120 116 119 elind ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}\ne {A}\right)\to {A}\in \left(\left({A}{L}{p}\right)\cap \left({A}{L}{B}\right)\right)$
121 1 3 4 110 111 112 113 tglinerflx2 ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}\ne {A}\right)\to {p}\in \left({A}{L}{p}\right)$
122 16 ad5antr ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}\ne {A}\right)\to {x}\in \left({A}{L}{B}\right)$
123 113 necomd ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}\ne {A}\right)\to {p}\ne {A}$
124 simpr ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}\ne {A}\right)\to {x}\ne {A}$
125 44 ad3antrrr ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}\ne {A}\right)\to {x}\in {P}$
126 1 2 3 4 39 11 22 18 13 41 44 42 45 78 79 colperpexlem1 ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\to ⟨“{x}{A}{p}”⟩\in {∟}_{𝒢}\left({G}\right)$
127 126 ad3antrrr ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}\ne {A}\right)\to ⟨“{x}{A}{p}”⟩\in {∟}_{𝒢}\left({G}\right)$
128 1 2 3 4 11 110 125 111 112 127 ragcom ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}\ne {A}\right)\to ⟨“{p}{A}{x}”⟩\in {∟}_{𝒢}\left({G}\right)$
129 1 2 3 4 110 114 115 120 121 122 123 124 128 ragperp ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}\ne {A}\right)\to \left({A}{L}{p}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)$
130 109 129 pm2.61dane ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\to \left({A}{L}{p}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)$
131 118 ad5antr ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}={A}\right)\to {A}\in \left({A}{L}{B}\right)$
132 62 131 eqeltrd ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}={A}\right)\to {t}\in \left({A}{L}{B}\right)$
133 132 orcd ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}={A}\right)\to \left({t}\in \left({A}{L}{B}\right)\vee {A}={B}\right)$
134 25 ad5antr ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}\ne {A}\right)\to {B}\in {P}$
135 117 ad5antr ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}\ne {A}\right)\to {A}\ne {B}$
136 simpllr ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}\ne {A}\right)\to {t}\in {P}$
137 124 necomd ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}\ne {A}\right)\to {A}\ne {x}$
138 simplrr ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}\ne {A}\right)\to {t}\in \left({A}{I}{x}\right)$
139 1 3 4 110 111 125 136 137 138 btwnlng1 ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}\ne {A}\right)\to {t}\in \left({A}{L}{x}\right)$
140 1 3 4 110 111 134 135 125 124 122 136 139 tglineeltr ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}\ne {A}\right)\to {t}\in \left({A}{L}{B}\right)$
141 140 orcd ${⊢}\left(\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\wedge {x}\ne {A}\right)\to \left({t}\in \left({A}{L}{B}\right)\vee {A}={B}\right)$
142 133 141 pm2.61dane ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\to \left({t}\in \left({A}{L}{B}\right)\vee {A}={B}\right)$
143 39 ad2antrr ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\to {G}\in {𝒢}_{\mathrm{Tarski}}$
144 45 ad2antrr ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\to {p}\in {P}$
145 simplr ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\to {t}\in {P}$
146 42 ad2antrr ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\to {C}\in {P}$
147 simprl ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\to {t}\in \left({p}{I}{C}\right)$
148 1 2 3 143 144 145 146 147 tgbtwncom ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\to {t}\in \left({C}{I}{p}\right)$
149 130 142 148 jca32 ${⊢}\left(\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\wedge \left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\right)\to \left(\left({A}{L}{p}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\wedge \left(\left({t}\in \left({A}{L}{B}\right)\vee {A}={B}\right)\wedge {t}\in \left({C}{I}{p}\right)\right)\right)$
150 149 ex ${⊢}\left(\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\wedge {t}\in {P}\right)\to \left(\left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\to \left(\left({A}{L}{p}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\wedge \left(\left({t}\in \left({A}{L}{B}\right)\vee {A}={B}\right)\wedge {t}\in \left({C}{I}{p}\right)\right)\right)\right)$
151 150 reximdva ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\to \left(\exists {t}\in {P}\phantom{\rule{.4em}{0ex}}\left({t}\in \left({p}{I}{C}\right)\wedge {t}\in \left({A}{I}{x}\right)\right)\to \exists {t}\in {P}\phantom{\rule{.4em}{0ex}}\left(\left({A}{L}{p}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\wedge \left(\left({t}\in \left({A}{L}{B}\right)\vee {A}={B}\right)\wedge {t}\in \left({C}{I}{p}\right)\right)\right)\right)$
152 53 151 mpd ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\to \exists {t}\in {P}\phantom{\rule{.4em}{0ex}}\left(\left({A}{L}{p}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\wedge \left(\left({t}\in \left({A}{L}{B}\right)\vee {A}={B}\right)\wedge {t}\in \left({C}{I}{p}\right)\right)\right)$
153 r19.42v ${⊢}\exists {t}\in {P}\phantom{\rule{.4em}{0ex}}\left(\left({A}{L}{p}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\wedge \left(\left({t}\in \left({A}{L}{B}\right)\vee {A}={B}\right)\wedge {t}\in \left({C}{I}{p}\right)\right)\right)↔\left(\left({A}{L}{p}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\wedge \exists {t}\in {P}\phantom{\rule{.4em}{0ex}}\left(\left({t}\in \left({A}{L}{B}\right)\vee {A}={B}\right)\wedge {t}\in \left({C}{I}{p}\right)\right)\right)$
154 152 153 sylib ${⊢}\left(\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\wedge {pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\right)\to \left(\left({A}{L}{p}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\wedge \exists {t}\in {P}\phantom{\rule{.4em}{0ex}}\left(\left({t}\in \left({A}{L}{B}\right)\vee {A}={B}\right)\wedge {t}\in \left({C}{I}{p}\right)\right)\right)$
155 154 ex ${⊢}\left(\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\wedge {p}\in {P}\right)\to \left({pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\to \left(\left({A}{L}{p}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\wedge \exists {t}\in {P}\phantom{\rule{.4em}{0ex}}\left(\left({t}\in \left({A}{L}{B}\right)\vee {A}={B}\right)\wedge {t}\in \left({C}{I}{p}\right)\right)\right)\right)$
156 155 reximdva ${⊢}\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\to \left(\exists {p}\in {P}\phantom{\rule{.4em}{0ex}}{pInv}_{𝒢}\left({G}\right)\left({A}\right)\left({C}\right)={pInv}_{𝒢}\left({G}\right)\left({p}\right)\left({pInv}_{𝒢}\left({G}\right)\left({x}\right)\left({C}\right)\right)\to \exists {p}\in {P}\phantom{\rule{.4em}{0ex}}\left(\left({A}{L}{p}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\wedge \exists {t}\in {P}\phantom{\rule{.4em}{0ex}}\left(\left({t}\in \left({A}{L}{B}\right)\vee {A}={B}\right)\wedge {t}\in \left({C}{I}{p}\right)\right)\right)\right)$
157 38 156 mpd ${⊢}\left(\left({\phi }\wedge {x}\in \left({A}{L}{B}\right)\right)\wedge \left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\right)\to \exists {p}\in {P}\phantom{\rule{.4em}{0ex}}\left(\left({A}{L}{p}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\wedge \exists {t}\in {P}\phantom{\rule{.4em}{0ex}}\left(\left({t}\in \left({A}{L}{B}\right)\vee {A}={B}\right)\wedge {t}\in \left({C}{I}{p}\right)\right)\right)$
158 1 2 3 4 5 14 8 10 footex ${⊢}{\phi }\to \exists {x}\in \left({A}{L}{B}\right)\phantom{\rule{.4em}{0ex}}\left({C}{L}{x}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)$
159 157 158 r19.29a ${⊢}{\phi }\to \exists {p}\in {P}\phantom{\rule{.4em}{0ex}}\left(\left({A}{L}{p}\right){⟂}_{𝒢}\left({G}\right)\left({A}{L}{B}\right)\wedge \exists {t}\in {P}\phantom{\rule{.4em}{0ex}}\left(\left({t}\in \left({A}{L}{B}\right)\vee {A}={B}\right)\wedge {t}\in \left({C}{I}{p}\right)\right)\right)$