Metamath Proof Explorer

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 ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝑃 𝐵 = ( ( 𝑆 ‘ 𝑥 ) ‘ 𝐴 ) )