Metamath Proof Explorer

Theorem footex

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

Ref Expression
Hypotheses isperp.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
isperp.d ⊢ − = ( dist ‘ 𝐺 )
isperp.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
isperp.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
isperp.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
isperp.a ⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
foot.x ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
foot.y ⊢ ( 𝜑 → ¬ 𝐶 ∈ 𝐴 )
Assertion footex ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐴 )

Proof

Step Hyp Ref Expression
1 isperp.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
2 isperp.d ⊢ − = ( dist ‘ 𝐺 )
3 isperp.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
4 isperp.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
5 isperp.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
6 isperp.a ⊢ ( 𝜑 → 𝐴 ∈ ran 𝐿 )
7 foot.x ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
8 foot.y ⊢ ( 𝜑 → ¬ 𝐶 ∈ 𝐴 )
9 eqid ⊢ ( pInvG ‘ 𝐺 ) = ( pInvG ‘ 𝐺 )
10 5 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) → 𝐺 ∈ TarskiG )
11 10 ad2antrr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) → 𝐺 ∈ TarskiG )
12 11 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) → 𝐺 ∈ TarskiG )
13 12 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) → 𝐺 ∈ TarskiG )
14 13 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑧 ) ‘ 𝑞 ) 𝐼 𝑑 ) ∧ ( 𝑦 − 𝑑 ) = ( 𝑦 − 𝐶 ) ) ) → 𝐺 ∈ TarskiG )
15 eqid ⊢ ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) = ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 )
16 7 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) → 𝐶 ∈ 𝑃 )
17 16 ad6antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) → 𝐶 ∈ 𝑃 )
18 17 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑧 ) ‘ 𝑞 ) 𝐼 𝑑 ) ∧ ( 𝑦 − 𝑑 ) = ( 𝑦 − 𝐶 ) ) ) → 𝐶 ∈ 𝑃 )
19 simplr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑧 ) ‘ 𝑞 ) 𝐼 𝑑 ) ∧ ( 𝑦 − 𝑑 ) = ( 𝑦 − 𝐶 ) ) ) → 𝑑 ∈ 𝑃 )
20 simp-4r ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) → 𝑦 ∈ 𝑃 )
21 20 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) → 𝑦 ∈ 𝑃 )
22 21 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) → 𝑦 ∈ 𝑃 )
23 22 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑧 ) ‘ 𝑞 ) 𝐼 𝑑 ) ∧ ( 𝑦 − 𝑑 ) = ( 𝑦 − 𝐶 ) ) ) → 𝑦 ∈ 𝑃 )
24 simprr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑧 ) ‘ 𝑞 ) 𝐼 𝑑 ) ∧ ( 𝑦 − 𝑑 ) = ( 𝑦 − 𝐶 ) ) ) → ( 𝑦 − 𝑑 ) = ( 𝑦 − 𝐶 ) )
25 24 eqcomd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑧 ) ‘ 𝑞 ) 𝐼 𝑑 ) ∧ ( 𝑦 − 𝑑 ) = ( 𝑦 − 𝐶 ) ) ) → ( 𝑦 − 𝐶 ) = ( 𝑦 − 𝑑 ) )
26 1 2 3 4 9 14 15 18 19 23 25 midexlem ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑧 ) ‘ 𝑞 ) 𝐼 𝑑 ) ∧ ( 𝑦 − 𝑑 ) = ( 𝑦 − 𝐶 ) ) ) → ∃ 𝑥 ∈ 𝑃 𝑑 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) )
27 12 ad5antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑧 ) ‘ 𝑞 ) 𝐼 𝑑 ) ∧ ( 𝑦 − 𝑑 ) = ( 𝑦 − 𝐶 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑑 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) → 𝐺 ∈ TarskiG )
28 6 ad5antr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) → 𝐴 ∈ ran 𝐿 )
29 28 ad9antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑧 ) ‘ 𝑞 ) 𝐼 𝑑 ) ∧ ( 𝑦 − 𝑑 ) = ( 𝑦 − 𝐶 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑑 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) → 𝐴 ∈ ran 𝐿 )
30 18 adantr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑧 ) ‘ 𝑞 ) 𝐼 𝑑 ) ∧ ( 𝑦 − 𝑑 ) = ( 𝑦 − 𝐶 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑑 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) → 𝐶 ∈ 𝑃 )
31 8 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) → ¬ 𝐶 ∈ 𝐴 )
32 31 ad10antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑧 ) ‘ 𝑞 ) 𝐼 𝑑 ) ∧ ( 𝑦 − 𝑑 ) = ( 𝑦 − 𝐶 ) ) ) → ¬ 𝐶 ∈ 𝐴 )
33 32 adantr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑧 ) ‘ 𝑞 ) 𝐼 𝑑 ) ∧ ( 𝑦 − 𝑑 ) = ( 𝑦 − 𝐶 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑑 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) → ¬ 𝐶 ∈ 𝐴 )
34 simp-7r ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) → 𝑎 ∈ 𝑃 )
35 34 ad2antrr ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) → 𝑎 ∈ 𝑃 )
36 35 ad5antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑧 ) ‘ 𝑞 ) 𝐼 𝑑 ) ∧ ( 𝑦 − 𝑑 ) = ( 𝑦 − 𝐶 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑑 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) → 𝑎 ∈ 𝑃 )
37 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) → 𝑏 ∈ 𝑃 )
38 37 ad10antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑧 ) ‘ 𝑞 ) 𝐼 𝑑 ) ∧ ( 𝑦 − 𝑑 ) = ( 𝑦 − 𝐶 ) ) ) → 𝑏 ∈ 𝑃 )
39 38 adantr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑧 ) ‘ 𝑞 ) 𝐼 𝑑 ) ∧ ( 𝑦 − 𝑑 ) = ( 𝑦 − 𝐶 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑑 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) → 𝑏 ∈ 𝑃 )
40 simp-4r ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) → 𝑝 ∈ 𝑃 )
41 40 ad5antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑧 ) ‘ 𝑞 ) 𝐼 𝑑 ) ∧ ( 𝑦 − 𝑑 ) = ( 𝑦 − 𝐶 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑑 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) → 𝑝 ∈ 𝑃 )
42 simprl ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑧 ) ‘ 𝑞 ) 𝐼 𝑑 ) ∧ ( 𝑦 − 𝑑 ) = ( 𝑦 − 𝐶 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑑 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) → 𝑥 ∈ 𝑃 )
43 21 ad5antr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑧 ) ‘ 𝑞 ) 𝐼 𝑑 ) ∧ ( 𝑦 − 𝑑 ) = ( 𝑦 − 𝐶 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑑 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) → 𝑦 ∈ 𝑃 )
44 simp-7r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑧 ) ‘ 𝑞 ) 𝐼 𝑑 ) ∧ ( 𝑦 − 𝑑 ) = ( 𝑦 − 𝐶 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑑 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) → 𝑧 ∈ 𝑃 )
45 simpllr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑧 ) ‘ 𝑞 ) 𝐼 𝑑 ) ∧ ( 𝑦 − 𝑑 ) = ( 𝑦 − 𝐶 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑑 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) → 𝑑 ∈ 𝑃 )
46 simp-11r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑧 ) ‘ 𝑞 ) 𝐼 𝑑 ) ∧ ( 𝑦 − 𝑑 ) = ( 𝑦 − 𝐶 ) ) ) → ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) )
47 46 simpld ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑧 ) ‘ 𝑞 ) 𝐼 𝑑 ) ∧ ( 𝑦 − 𝑑 ) = ( 𝑦 − 𝐶 ) ) ) → 𝐴 = ( 𝑎 𝐿 𝑏 ) )
48 47 adantr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑧 ) ‘ 𝑞 ) 𝐼 𝑑 ) ∧ ( 𝑦 − 𝑑 ) = ( 𝑦 − 𝐶 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑑 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) → 𝐴 = ( 𝑎 𝐿 𝑏 ) )
49 46 simprd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑧 ) ‘ 𝑞 ) 𝐼 𝑑 ) ∧ ( 𝑦 − 𝑑 ) = ( 𝑦 − 𝐶 ) ) ) → 𝑎 ≠ 𝑏 )
50 49 adantr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑧 ) ‘ 𝑞 ) 𝐼 𝑑 ) ∧ ( 𝑦 − 𝑑 ) = ( 𝑦 − 𝐶 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑑 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) → 𝑎 ≠ 𝑏 )
51 simp-9r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑧 ) ‘ 𝑞 ) 𝐼 𝑑 ) ∧ ( 𝑦 − 𝑑 ) = ( 𝑦 − 𝐶 ) ) ) → ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) )
52 51 simpld ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑧 ) ‘ 𝑞 ) 𝐼 𝑑 ) ∧ ( 𝑦 − 𝑑 ) = ( 𝑦 − 𝐶 ) ) ) → 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) )
53 52 adantr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑧 ) ‘ 𝑞 ) 𝐼 𝑑 ) ∧ ( 𝑦 − 𝑑 ) = ( 𝑦 − 𝐶 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑑 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) → 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) )
54 51 simprd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑧 ) ‘ 𝑞 ) 𝐼 𝑑 ) ∧ ( 𝑦 − 𝑑 ) = ( 𝑦 − 𝐶 ) ) ) → ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) )
55 54 adantr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑧 ) ‘ 𝑞 ) 𝐼 𝑑 ) ∧ ( 𝑦 − 𝑑 ) = ( 𝑦 − 𝐶 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑑 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) → ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) )
56 simp-7r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑧 ) ‘ 𝑞 ) 𝐼 𝑑 ) ∧ ( 𝑦 − 𝑑 ) = ( 𝑦 − 𝐶 ) ) ) → 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) )
57 56 adantr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑧 ) ‘ 𝑞 ) 𝐼 𝑑 ) ∧ ( 𝑦 − 𝑑 ) = ( 𝑦 − 𝐶 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑑 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) → 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) )
58 simp-5r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑧 ) ‘ 𝑞 ) 𝐼 𝑑 ) ∧ ( 𝑦 − 𝑑 ) = ( 𝑦 − 𝐶 ) ) ) → ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) )
59 58 simpld ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑧 ) ‘ 𝑞 ) 𝐼 𝑑 ) ∧ ( 𝑦 − 𝑑 ) = ( 𝑦 − 𝐶 ) ) ) → 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) )
60 59 adantr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑧 ) ‘ 𝑞 ) 𝐼 𝑑 ) ∧ ( 𝑦 − 𝑑 ) = ( 𝑦 − 𝐶 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑑 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) → 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) )
61 58 simprd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑧 ) ‘ 𝑞 ) 𝐼 𝑑 ) ∧ ( 𝑦 − 𝑑 ) = ( 𝑦 − 𝐶 ) ) ) → ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) )
62 61 adantr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑧 ) ‘ 𝑞 ) 𝐼 𝑑 ) ∧ ( 𝑦 − 𝑑 ) = ( 𝑦 − 𝐶 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑑 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) → ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) )
63 simp-5r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑧 ) ‘ 𝑞 ) 𝐼 𝑑 ) ∧ ( 𝑦 − 𝑑 ) = ( 𝑦 − 𝐶 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑑 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) → 𝑞 ∈ 𝑃 )
64 simpllr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑧 ) ‘ 𝑞 ) 𝐼 𝑑 ) ∧ ( 𝑦 − 𝑑 ) = ( 𝑦 − 𝐶 ) ) ) → ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) )
65 64 simpld ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑧 ) ‘ 𝑞 ) 𝐼 𝑑 ) ∧ ( 𝑦 − 𝑑 ) = ( 𝑦 − 𝐶 ) ) ) → 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) )
66 65 adantr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑧 ) ‘ 𝑞 ) 𝐼 𝑑 ) ∧ ( 𝑦 − 𝑑 ) = ( 𝑦 − 𝐶 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑑 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) → 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) )
67 64 simprd ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑧 ) ‘ 𝑞 ) 𝐼 𝑑 ) ∧ ( 𝑦 − 𝑑 ) = ( 𝑦 − 𝐶 ) ) ) → ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) )
68 67 adantr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑧 ) ‘ 𝑞 ) 𝐼 𝑑 ) ∧ ( 𝑦 − 𝑑 ) = ( 𝑦 − 𝐶 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑑 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) → ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) )
69 simplrl ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑧 ) ‘ 𝑞 ) 𝐼 𝑑 ) ∧ ( 𝑦 − 𝑑 ) = ( 𝑦 − 𝐶 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑑 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) → 𝑦 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑧 ) ‘ 𝑞 ) 𝐼 𝑑 ) )
70 24 adantr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑧 ) ‘ 𝑞 ) 𝐼 𝑑 ) ∧ ( 𝑦 − 𝑑 ) = ( 𝑦 − 𝐶 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑑 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) → ( 𝑦 − 𝑑 ) = ( 𝑦 − 𝐶 ) )
71 simprr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑧 ) ‘ 𝑞 ) 𝐼 𝑑 ) ∧ ( 𝑦 − 𝑑 ) = ( 𝑦 − 𝐶 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑑 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) → 𝑑 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) )
72 1 2 3 4 27 29 30 33 36 39 41 42 43 44 45 48 50 53 55 57 60 62 63 66 68 69 70 71 footexlem1 ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑧 ) ‘ 𝑞 ) 𝐼 𝑑 ) ∧ ( 𝑦 − 𝑑 ) = ( 𝑦 − 𝐶 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑑 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) → 𝑥 ∈ 𝐴 )
73 1 2 3 4 27 29 30 33 36 39 41 42 43 44 45 48 50 53 55 57 60 62 63 66 68 69 70 71 footexlem2 ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑧 ) ‘ 𝑞 ) 𝐼 𝑑 ) ∧ ( 𝑦 − 𝑑 ) = ( 𝑦 − 𝐶 ) ) ) ∧ ( 𝑥 ∈ 𝑃 ∧ 𝑑 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) → ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐴 )
74 26 72 73 reximssdv ⊢ ( ( ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) ∧ 𝑑 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑧 ) ‘ 𝑞 ) 𝐼 𝑑 ) ∧ ( 𝑦 − 𝑑 ) = ( 𝑦 − 𝐶 ) ) ) → ∃ 𝑥 ∈ 𝐴 ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐴 )
75 simp-4r ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) → 𝑧 ∈ 𝑃 )
76 eqid ⊢ ( ( pInvG ‘ 𝐺 ) ‘ 𝑧 ) = ( ( pInvG ‘ 𝐺 ) ‘ 𝑧 )
77 simplr ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) → 𝑞 ∈ 𝑃 )
78 1 2 3 4 9 13 75 76 77 mircl ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑧 ) ‘ 𝑞 ) ∈ 𝑃 )
79 1 2 3 13 78 22 22 17 axtgsegcon ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) → ∃ 𝑑 ∈ 𝑃 ( 𝑦 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑧 ) ‘ 𝑞 ) 𝐼 𝑑 ) ∧ ( 𝑦 − 𝑑 ) = ( 𝑦 − 𝐶 ) ) )
80 74 79 r19.29a ⊢ ( ( ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) ∧ 𝑞 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) ) → ∃ 𝑥 ∈ 𝐴 ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐴 )
81 1 2 3 12 40 21 21 35 axtgsegcon ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) → ∃ 𝑞 ∈ 𝑃 ( 𝑦 ∈ ( 𝑝 𝐼 𝑞 ) ∧ ( 𝑦 − 𝑞 ) = ( 𝑦 − 𝑎 ) ) )
82 80 81 r19.29a ⊢ ( ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) ∧ 𝑧 ∈ 𝑃 ) ∧ ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) ) → ∃ 𝑥 ∈ 𝐴 ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐴 )
83 simplr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) → 𝑝 ∈ 𝑃 )
84 1 2 3 11 34 20 20 83 axtgsegcon ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) → ∃ 𝑧 ∈ 𝑃 ( 𝑦 ∈ ( 𝑎 𝐼 𝑧 ) ∧ ( 𝑦 − 𝑧 ) = ( 𝑦 − 𝑝 ) ) )
85 82 84 r19.29a ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) ) → ∃ 𝑥 ∈ 𝐴 ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐴 )
86 eqid ⊢ ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) = ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 )
87 simplr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) → 𝑦 ∈ 𝑃 )
88 simp-5r ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) → 𝑎 ∈ 𝑃 )
89 simprr ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) → ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) )
90 1 2 3 4 9 10 86 87 16 88 89 midexlem ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) → ∃ 𝑝 ∈ 𝑃 𝐶 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ 𝑦 ) )
91 85 90 r19.29a ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) ∧ 𝑦 ∈ 𝑃 ) ∧ ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) ) → ∃ 𝑥 ∈ 𝐴 ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐴 )
92 5 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) → 𝐺 ∈ TarskiG )
93 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) → 𝑎 ∈ 𝑃 )
94 7 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) → 𝐶 ∈ 𝑃 )
95 1 2 3 92 37 93 93 94 axtgsegcon ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) → ∃ 𝑦 ∈ 𝑃 ( 𝑎 ∈ ( 𝑏 𝐼 𝑦 ) ∧ ( 𝑎 − 𝑦 ) = ( 𝑎 − 𝐶 ) ) )
96 91 95 r19.29a ⊢ ( ( ( ( 𝜑 ∧ 𝑎 ∈ 𝑃 ) ∧ 𝑏 ∈ 𝑃 ) ∧ ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) ) → ∃ 𝑥 ∈ 𝐴 ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐴 )
97 1 3 4 5 6 tgisline ⊢ ( 𝜑 → ∃ 𝑎 ∈ 𝑃 ∃ 𝑏 ∈ 𝑃 ( 𝐴 = ( 𝑎 𝐿 𝑏 ) ∧ 𝑎 ≠ 𝑏 ) )
98 96 97 r19.29vva ⊢ ( 𝜑 → ∃ 𝑥 ∈ 𝐴 ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐴 )