Theorem midex

Description: Existence of the midpoint, part Theorem 8.22 of Schwabhauser p. 64. Note that this proof requires a construction in 2 dimensions or more, i.e. it does not prove the existence of a midpoint in dimension 1, for a geometry restricted to a line. (Contributed by Thierry Arnoux, 25-Nov-2019)

	Ref	Expression
Hypotheses	colperpex.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
	colperpex.d	⊢ − = ( dist ‘ 𝐺 )
	colperpex.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	colperpex.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
	colperpex.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	mideu.s	⊢ 𝑆 = ( pInvG ‘ 𝐺 )
	mideu.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
	mideu.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
	mideu.3	⊢ ( 𝜑 → 𝐺 DimTarskiG≥ 2 )
Assertion	midex	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 𝐵 = ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		colperpex.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		colperpex.d	⊢ − = ( dist ‘ 𝐺 )
3		colperpex.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		colperpex.l	⊢ 𝐿 = ( LineG ‘ 𝐺 )
5		colperpex.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6		mideu.s	⊢ 𝑆 = ( pInvG ‘ 𝐺 )
7		mideu.1	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
8		mideu.2	⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
9		mideu.3	⊢ ( 𝜑 → 𝐺 DimTarskiG≥ 2 )
10	5	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝐺 ∈ TarskiG )
11	7	adantr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝐴 ∈ 𝑃 )
12		eqid	⊢ ( 𝑆 ‘ 𝐴 ) = ( 𝑆 ‘ 𝐴 )
13	1 2 3 4 6 10 11 12	mircinv	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → ( ( 𝑆 ‘ 𝐴 ) ‘ 𝐴 ) = 𝐴 )
14		simpr	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝐴 = 𝐵 )
15	13 14	eqtr2d	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → 𝐵 = ( ( 𝑆 ‘ 𝐴 ) ‘ 𝐴 ) )
16		fveq2	⊢ ( 𝑥 = 𝐴 → ( 𝑆 ‘ 𝑥 ) = ( 𝑆 ‘ 𝐴 ) )
17	16	fveq1d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐴 ) = ( ( 𝑆 ‘ 𝐴 ) ‘ 𝐴 ) )
18	17	rspceeqv	⊢ ( ( 𝐴 ∈ 𝑃 ∧ 𝐵 = ( ( 𝑆 ‘ 𝐴 ) ‘ 𝐴 ) ) → ∃ 𝑥 ∈ 𝑃 𝐵 = ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐴 ) )
19	7 15 18	syl2an2r	⊢ ( ( 𝜑 ∧ 𝐴 = 𝐵 ) → ∃ 𝑥 ∈ 𝑃 𝐵 = ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐴 ) )
20	5	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) → 𝐺 ∈ TarskiG )
21	20	ad4antr	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐴 − 𝑝 ) ( ≤G ‘ 𝐺 ) ( 𝐵 − 𝑞 ) ) → 𝐺 ∈ TarskiG )
22	7	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) → 𝐴 ∈ 𝑃 )
23	22	ad4antr	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐴 − 𝑝 ) ( ≤G ‘ 𝐺 ) ( 𝐵 − 𝑞 ) ) → 𝐴 ∈ 𝑃 )
24	8	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) → 𝐵 ∈ 𝑃 )
25	24	ad4antr	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐴 − 𝑝 ) ( ≤G ‘ 𝐺 ) ( 𝐵 − 𝑞 ) ) → 𝐵 ∈ 𝑃 )
26		simpllr	⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) → 𝐴 ≠ 𝐵 )
27	26	ad4antr	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐴 − 𝑝 ) ( ≤G ‘ 𝐺 ) ( 𝐵 − 𝑞 ) ) → 𝐴 ≠ 𝐵 )
28		simplr	⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) → 𝑞 ∈ 𝑃 )
29	28	ad4antr	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐴 − 𝑝 ) ( ≤G ‘ 𝐺 ) ( 𝐵 − 𝑞 ) ) → 𝑞 ∈ 𝑃 )
30		simp-4r	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐴 − 𝑝 ) ( ≤G ‘ 𝐺 ) ( 𝐵 − 𝑞 ) ) → 𝑝 ∈ 𝑃 )
31		simpllr	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐴 − 𝑝 ) ( ≤G ‘ 𝐺 ) ( 𝐵 − 𝑞 ) ) → 𝑡 ∈ 𝑃 )
32		simp-5r	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐴 − 𝑝 ) ( ≤G ‘ 𝐺 ) ( 𝐵 − 𝑞 ) ) → ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) )
33	4 21 32	perpln1	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐴 − 𝑝 ) ( ≤G ‘ 𝐺 ) ( 𝐵 − 𝑞 ) ) → ( 𝐵 𝐿 𝑞 ) ∈ ran 𝐿 )
34	1 3 4 21 23 25 27	tgelrnln	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐴 − 𝑝 ) ( ≤G ‘ 𝐺 ) ( 𝐵 − 𝑞 ) ) → ( 𝐴 𝐿 𝐵 ) ∈ ran 𝐿 )
35	1 2 3 4 21 33 34 32	perpcom	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐴 − 𝑝 ) ( ≤G ‘ 𝐺 ) ( 𝐵 − 𝑞 ) ) → ( 𝐴 𝐿 𝐵 ) ( ⟂G ‘ 𝐺 ) ( 𝐵 𝐿 𝑞 ) )
36	1 3 4 21 25 29 33	tglnne	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐴 − 𝑝 ) ( ≤G ‘ 𝐺 ) ( 𝐵 − 𝑞 ) ) → 𝐵 ≠ 𝑞 )
37	1 3 4 21 25 29 36	tglinecom	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐴 − 𝑝 ) ( ≤G ‘ 𝐺 ) ( 𝐵 − 𝑞 ) ) → ( 𝐵 𝐿 𝑞 ) = ( 𝑞 𝐿 𝐵 ) )
38	35 37	breqtrd	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐴 − 𝑝 ) ( ≤G ‘ 𝐺 ) ( 𝐵 − 𝑞 ) ) → ( 𝐴 𝐿 𝐵 ) ( ⟂G ‘ 𝐺 ) ( 𝑞 𝐿 𝐵 ) )
39		simplr	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐴 − 𝑝 ) ( ≤G ‘ 𝐺 ) ( 𝐵 − 𝑞 ) ) → ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) )
40	39	simpld	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐴 − 𝑝 ) ( ≤G ‘ 𝐺 ) ( 𝐵 − 𝑞 ) ) → ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) )
41	4 21 40	perpln1	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐴 − 𝑝 ) ( ≤G ‘ 𝐺 ) ( 𝐵 − 𝑞 ) ) → ( 𝐴 𝐿 𝑝 ) ∈ ran 𝐿 )
42	1 2 3 4 21 41 34 40	perpcom	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐴 − 𝑝 ) ( ≤G ‘ 𝐺 ) ( 𝐵 − 𝑞 ) ) → ( 𝐴 𝐿 𝐵 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑝 ) )
43	27	neneqd	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐴 − 𝑝 ) ( ≤G ‘ 𝐺 ) ( 𝐵 − 𝑞 ) ) → ¬ 𝐴 = 𝐵 )
44	39	simprd	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐴 − 𝑝 ) ( ≤G ‘ 𝐺 ) ( 𝐵 − 𝑞 ) ) → ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) )
45	44	simpld	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐴 − 𝑝 ) ( ≤G ‘ 𝐺 ) ( 𝐵 − 𝑞 ) ) → ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
46	45	orcomd	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐴 − 𝑝 ) ( ≤G ‘ 𝐺 ) ( 𝐵 − 𝑞 ) ) → ( 𝐴 = 𝐵 ∨ 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ) )
47	46	ord	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐴 − 𝑝 ) ( ≤G ‘ 𝐺 ) ( 𝐵 − 𝑞 ) ) → ( ¬ 𝐴 = 𝐵 → 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ) )
48	43 47	mpd	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐴 − 𝑝 ) ( ≤G ‘ 𝐺 ) ( 𝐵 − 𝑞 ) ) → 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) )
49	44	simprd	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐴 − 𝑝 ) ( ≤G ‘ 𝐺 ) ( 𝐵 − 𝑞 ) ) → 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) )
50		simpr	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐴 − 𝑝 ) ( ≤G ‘ 𝐺 ) ( 𝐵 − 𝑞 ) ) → ( 𝐴 − 𝑝 ) ( ≤G ‘ 𝐺 ) ( 𝐵 − 𝑞 ) )
51	1 2 3 4 21 6 23 25 27 29 30 31 38 42 48 49 50	mideulem	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐴 − 𝑝 ) ( ≤G ‘ 𝐺 ) ( 𝐵 − 𝑞 ) ) → ∃ 𝑥 ∈ 𝑃 𝐵 = ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐴 ) )
52	20	ad4antr	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐵 − 𝑞 ) ( ≤G ‘ 𝐺 ) ( 𝐴 − 𝑝 ) ) → 𝐺 ∈ TarskiG )
53	52	adantr	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐵 − 𝑞 ) ( ≤G ‘ 𝐺 ) ( 𝐴 − 𝑝 ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝐴 = ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐵 ) ) ) → 𝐺 ∈ TarskiG )
54		simprl	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐵 − 𝑞 ) ( ≤G ‘ 𝐺 ) ( 𝐴 − 𝑝 ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝐴 = ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐵 ) ) ) → 𝑥 ∈ 𝑃 )
55		eqid	⊢ ( 𝑆 ‘ 𝑥 ) = ( 𝑆 ‘ 𝑥 )
56	24	ad4antr	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐵 − 𝑞 ) ( ≤G ‘ 𝐺 ) ( 𝐴 − 𝑝 ) ) → 𝐵 ∈ 𝑃 )
57	56	adantr	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐵 − 𝑞 ) ( ≤G ‘ 𝐺 ) ( 𝐴 − 𝑝 ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝐴 = ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐵 ) ) ) → 𝐵 ∈ 𝑃 )
58		simprr	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐵 − 𝑞 ) ( ≤G ‘ 𝐺 ) ( 𝐴 − 𝑝 ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝐴 = ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐵 ) ) ) → 𝐴 = ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐵 ) )
59	58	eqcomd	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐵 − 𝑞 ) ( ≤G ‘ 𝐺 ) ( 𝐴 − 𝑝 ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝐴 = ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐵 ) ) ) → ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐵 ) = 𝐴 )
60	1 2 3 4 6 53 54 55 57 59	mircom	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐵 − 𝑞 ) ( ≤G ‘ 𝐺 ) ( 𝐴 − 𝑝 ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝐴 = ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐵 ) ) ) → ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐴 ) = 𝐵 )
61	60	eqcomd	⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐵 − 𝑞 ) ( ≤G ‘ 𝐺 ) ( 𝐴 − 𝑝 ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝐴 = ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐵 ) ) ) → 𝐵 = ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐴 ) )
62	22	ad4antr	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐵 − 𝑞 ) ( ≤G ‘ 𝐺 ) ( 𝐴 − 𝑝 ) ) → 𝐴 ∈ 𝑃 )
63	26	ad4antr	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐵 − 𝑞 ) ( ≤G ‘ 𝐺 ) ( 𝐴 − 𝑝 ) ) → 𝐴 ≠ 𝐵 )
64	63	necomd	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐵 − 𝑞 ) ( ≤G ‘ 𝐺 ) ( 𝐴 − 𝑝 ) ) → 𝐵 ≠ 𝐴 )
65		simp-4r	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐵 − 𝑞 ) ( ≤G ‘ 𝐺 ) ( 𝐴 − 𝑝 ) ) → 𝑝 ∈ 𝑃 )
66	28	ad4antr	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐵 − 𝑞 ) ( ≤G ‘ 𝐺 ) ( 𝐴 − 𝑝 ) ) → 𝑞 ∈ 𝑃 )
67		simpllr	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐵 − 𝑞 ) ( ≤G ‘ 𝐺 ) ( 𝐴 − 𝑝 ) ) → 𝑡 ∈ 𝑃 )
68		simplr	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐵 − 𝑞 ) ( ≤G ‘ 𝐺 ) ( 𝐴 − 𝑝 ) ) → ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) )
69	68	simpld	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐵 − 𝑞 ) ( ≤G ‘ 𝐺 ) ( 𝐴 − 𝑝 ) ) → ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) )
70	4 52 69	perpln1	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐵 − 𝑞 ) ( ≤G ‘ 𝐺 ) ( 𝐴 − 𝑝 ) ) → ( 𝐴 𝐿 𝑝 ) ∈ ran 𝐿 )
71	1 3 4 52 62 65 70	tglnne	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐵 − 𝑞 ) ( ≤G ‘ 𝐺 ) ( 𝐴 − 𝑝 ) ) → 𝐴 ≠ 𝑝 )
72	1 3 4 52 62 65 71	tglinecom	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐵 − 𝑞 ) ( ≤G ‘ 𝐺 ) ( 𝐴 − 𝑝 ) ) → ( 𝐴 𝐿 𝑝 ) = ( 𝑝 𝐿 𝐴 ) )
73	72 70	eqeltrrd	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐵 − 𝑞 ) ( ≤G ‘ 𝐺 ) ( 𝐴 − 𝑝 ) ) → ( 𝑝 𝐿 𝐴 ) ∈ ran 𝐿 )
74	1 3 4 52 56 62 64	tgelrnln	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐵 − 𝑞 ) ( ≤G ‘ 𝐺 ) ( 𝐴 − 𝑝 ) ) → ( 𝐵 𝐿 𝐴 ) ∈ ran 𝐿 )
75	1 3 4 52 62 56 63	tglinecom	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐵 − 𝑞 ) ( ≤G ‘ 𝐺 ) ( 𝐴 − 𝑝 ) ) → ( 𝐴 𝐿 𝐵 ) = ( 𝐵 𝐿 𝐴 ) )
76	69 72 75	3brtr3d	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐵 − 𝑞 ) ( ≤G ‘ 𝐺 ) ( 𝐴 − 𝑝 ) ) → ( 𝑝 𝐿 𝐴 ) ( ⟂G ‘ 𝐺 ) ( 𝐵 𝐿 𝐴 ) )
77	1 2 3 4 52 73 74 76	perpcom	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐵 − 𝑞 ) ( ≤G ‘ 𝐺 ) ( 𝐴 − 𝑝 ) ) → ( 𝐵 𝐿 𝐴 ) ( ⟂G ‘ 𝐺 ) ( 𝑝 𝐿 𝐴 ) )
78		simp-5r	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐵 − 𝑞 ) ( ≤G ‘ 𝐺 ) ( 𝐴 − 𝑝 ) ) → ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) )
79	4 52 78	perpln1	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐵 − 𝑞 ) ( ≤G ‘ 𝐺 ) ( 𝐴 − 𝑝 ) ) → ( 𝐵 𝐿 𝑞 ) ∈ ran 𝐿 )
80	78 75	breqtrd	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐵 − 𝑞 ) ( ≤G ‘ 𝐺 ) ( 𝐴 − 𝑝 ) ) → ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐵 𝐿 𝐴 ) )
81	1 2 3 4 52 79 74 80	perpcom	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐵 − 𝑞 ) ( ≤G ‘ 𝐺 ) ( 𝐴 − 𝑝 ) ) → ( 𝐵 𝐿 𝐴 ) ( ⟂G ‘ 𝐺 ) ( 𝐵 𝐿 𝑞 ) )
82	63	neneqd	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐵 − 𝑞 ) ( ≤G ‘ 𝐺 ) ( 𝐴 − 𝑝 ) ) → ¬ 𝐴 = 𝐵 )
83	68	simprd	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐵 − 𝑞 ) ( ≤G ‘ 𝐺 ) ( 𝐴 − 𝑝 ) ) → ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) )
84	83	simpld	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐵 − 𝑞 ) ( ≤G ‘ 𝐺 ) ( 𝐴 − 𝑝 ) ) → ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
85	84	orcomd	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐵 − 𝑞 ) ( ≤G ‘ 𝐺 ) ( 𝐴 − 𝑝 ) ) → ( 𝐴 = 𝐵 ∨ 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ) )
86	85	ord	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐵 − 𝑞 ) ( ≤G ‘ 𝐺 ) ( 𝐴 − 𝑝 ) ) → ( ¬ 𝐴 = 𝐵 → 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ) )
87	82 86	mpd	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐵 − 𝑞 ) ( ≤G ‘ 𝐺 ) ( 𝐴 − 𝑝 ) ) → 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) )
88	87 75	eleqtrd	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐵 − 𝑞 ) ( ≤G ‘ 𝐺 ) ( 𝐴 − 𝑝 ) ) → 𝑡 ∈ ( 𝐵 𝐿 𝐴 ) )
89	83	simprd	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐵 − 𝑞 ) ( ≤G ‘ 𝐺 ) ( 𝐴 − 𝑝 ) ) → 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) )
90	1 2 3 52 66 67 65 89	tgbtwncom	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐵 − 𝑞 ) ( ≤G ‘ 𝐺 ) ( 𝐴 − 𝑝 ) ) → 𝑡 ∈ ( 𝑝 𝐼 𝑞 ) )
91		simpr	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐵 − 𝑞 ) ( ≤G ‘ 𝐺 ) ( 𝐴 − 𝑝 ) ) → ( 𝐵 − 𝑞 ) ( ≤G ‘ 𝐺 ) ( 𝐴 − 𝑝 ) )
92	1 2 3 4 52 6 56 62 64 65 66 67 77 81 88 90 91	mideulem	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐵 − 𝑞 ) ( ≤G ‘ 𝐺 ) ( 𝐴 − 𝑝 ) ) → ∃ 𝑥 ∈ 𝑃 𝐴 = ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐵 ) )
93	61 92	reximddv	⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) ∧ ( 𝐵 − 𝑞 ) ( ≤G ‘ 𝐺 ) ( 𝐴 − 𝑝 ) ) → ∃ 𝑥 ∈ 𝑃 𝐵 = ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐴 ) )
94		eqid	⊢ ( ≤G ‘ 𝐺 ) = ( ≤G ‘ 𝐺 )
95	20	ad3antrrr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) → 𝐺 ∈ TarskiG )
96	22	ad3antrrr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) → 𝐴 ∈ 𝑃 )
97		simpllr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) → 𝑝 ∈ 𝑃 )
98	24	ad3antrrr	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) → 𝐵 ∈ 𝑃 )
99		simp-5r	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) → 𝑞 ∈ 𝑃 )
100	1 2 3 94 95 96 97 98 99	legtrid	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) → ( ( 𝐴 − 𝑝 ) ( ≤G ‘ 𝐺 ) ( 𝐵 − 𝑞 ) ∨ ( 𝐵 − 𝑞 ) ( ≤G ‘ 𝐺 ) ( 𝐴 − 𝑝 ) ) )
101	51 93 100	mpjaodan	⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ) → ∃ 𝑥 ∈ 𝑃 𝐵 = ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐴 ) )
102	9	ad3antrrr	⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) → 𝐺 DimTarskiG≥ 2 )
103	1 2 3 4 20 22 24 28 26 102	colperpex	⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) → ∃ 𝑝 ∈ 𝑃 ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ∃ 𝑡 ∈ 𝑃 ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) )
104		r19.42v	⊢ ( ∃ 𝑡 ∈ 𝑃 ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ↔ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ∃ 𝑡 ∈ 𝑃 ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) )
105	104	rexbii	⊢ ( ∃ 𝑝 ∈ 𝑃 ∃ 𝑡 ∈ 𝑃 ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) ↔ ∃ 𝑝 ∈ 𝑃 ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ∃ 𝑡 ∈ 𝑃 ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) )
106	103 105	sylibr	⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) → ∃ 𝑝 ∈ 𝑃 ∃ 𝑡 ∈ 𝑃 ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝑞 𝐼 𝑝 ) ) ) )
107	101 106	r19.29vva	⊢ ( ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) → ∃ 𝑥 ∈ 𝑃 𝐵 = ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐴 ) )
108	5	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐺 ∈ TarskiG )
109	8	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐵 ∈ 𝑃 )
110	7	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ∈ 𝑃 )
111		simpr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐴 ≠ 𝐵 )
112	111	necomd	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐵 ≠ 𝐴 )
113	9	adantr	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → 𝐺 DimTarskiG≥ 2 )
114	1 2 3 4 108 109 110 110 112 113	colperpex	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → ∃ 𝑞 ∈ 𝑃 ( ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐵 𝐿 𝐴 ) ∧ ∃ 𝑠 ∈ 𝑃 ( ( 𝑠 ∈ ( 𝐵 𝐿 𝐴 ) ∨ 𝐵 = 𝐴 ) ∧ 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ) ) )
115		simprl	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐵 𝐿 𝐴 ) ∧ ∃ 𝑠 ∈ 𝑃 ( ( 𝑠 ∈ ( 𝐵 𝐿 𝐴 ) ∨ 𝐵 = 𝐴 ) ∧ 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ) ) ) → ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐵 𝐿 𝐴 ) )
116	1 3 4 108 110 109 111	tglinecom	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → ( 𝐴 𝐿 𝐵 ) = ( 𝐵 𝐿 𝐴 ) )
117	116	adantr	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐵 𝐿 𝐴 ) ∧ ∃ 𝑠 ∈ 𝑃 ( ( 𝑠 ∈ ( 𝐵 𝐿 𝐴 ) ∨ 𝐵 = 𝐴 ) ∧ 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ) ) ) → ( 𝐴 𝐿 𝐵 ) = ( 𝐵 𝐿 𝐴 ) )
118	115 117	breqtrrd	⊢ ( ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) ∧ ( ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐵 𝐿 𝐴 ) ∧ ∃ 𝑠 ∈ 𝑃 ( ( 𝑠 ∈ ( 𝐵 𝐿 𝐴 ) ∨ 𝐵 = 𝐴 ) ∧ 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ) ) ) → ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) )
119	118	ex	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → ( ( ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐵 𝐿 𝐴 ) ∧ ∃ 𝑠 ∈ 𝑃 ( ( 𝑠 ∈ ( 𝐵 𝐿 𝐴 ) ∨ 𝐵 = 𝐴 ) ∧ 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ) ) → ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) )
120	119	reximdv	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → ( ∃ 𝑞 ∈ 𝑃 ( ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐵 𝐿 𝐴 ) ∧ ∃ 𝑠 ∈ 𝑃 ( ( 𝑠 ∈ ( 𝐵 𝐿 𝐴 ) ∨ 𝐵 = 𝐴 ) ∧ 𝑠 ∈ ( 𝐴 𝐼 𝑞 ) ) ) → ∃ 𝑞 ∈ 𝑃 ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) )
121	114 120	mpd	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → ∃ 𝑞 ∈ 𝑃 ( 𝐵 𝐿 𝑞 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) )
122	107 121	r19.29a	⊢ ( ( 𝜑 ∧ 𝐴 ≠ 𝐵 ) → ∃ 𝑥 ∈ 𝑃 𝐵 = ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐴 ) )
123	19 122	pm2.61dane	⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 𝐵 = ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐴 ) )