Metamath Proof Explorer


Theorem opphl

Description: If two points A and C lie on opposite sides of a line D , then any point of the half line ( R A ) also lies opposite to C . Theorem 9.5 of Schwabhauser p. 69. (Contributed by Thierry Arnoux, 3-Mar-2019)

Ref Expression
Hypotheses hpg.p 𝑃 = ( Base ‘ 𝐺 )
hpg.d = ( dist ‘ 𝐺 )
hpg.i 𝐼 = ( Itv ‘ 𝐺 )
hpg.o 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃𝐷 ) ∧ 𝑏 ∈ ( 𝑃𝐷 ) ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
opphl.l 𝐿 = ( LineG ‘ 𝐺 )
opphl.d ( 𝜑𝐷 ∈ ran 𝐿 )
opphl.g ( 𝜑𝐺 ∈ TarskiG )
opphl.k 𝐾 = ( hlG ‘ 𝐺 )
opphl.a ( 𝜑𝐴𝑃 )
opphl.b ( 𝜑𝐵𝑃 )
opphl.c ( 𝜑𝐶𝑃 )
opphl.1 ( 𝜑𝐴 𝑂 𝐶 )
opphl.2 ( 𝜑𝑅𝐷 )
opphl.3 ( 𝜑𝐴 ( 𝐾𝑅 ) 𝐵 )
Assertion opphl ( 𝜑𝐵 𝑂 𝐶 )

Proof

Step Hyp Ref Expression
1 hpg.p 𝑃 = ( Base ‘ 𝐺 )
2 hpg.d = ( dist ‘ 𝐺 )
3 hpg.i 𝐼 = ( Itv ‘ 𝐺 )
4 hpg.o 𝑂 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ ( 𝑃𝐷 ) ∧ 𝑏 ∈ ( 𝑃𝐷 ) ) ∧ ∃ 𝑡𝐷 𝑡 ∈ ( 𝑎 𝐼 𝑏 ) ) }
5 opphl.l 𝐿 = ( LineG ‘ 𝐺 )
6 opphl.d ( 𝜑𝐷 ∈ ran 𝐿 )
7 opphl.g ( 𝜑𝐺 ∈ TarskiG )
8 opphl.k 𝐾 = ( hlG ‘ 𝐺 )
9 opphl.a ( 𝜑𝐴𝑃 )
10 opphl.b ( 𝜑𝐵𝑃 )
11 opphl.c ( 𝜑𝐶𝑃 )
12 opphl.1 ( 𝜑𝐴 𝑂 𝐶 )
13 opphl.2 ( 𝜑𝑅𝐷 )
14 opphl.3 ( 𝜑𝐴 ( 𝐾𝑅 ) 𝐵 )
15 6 ad8antr ( ( ( ( ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑚𝑃 ) ∧ 𝑧 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∧ 𝑦𝐷 ) ∧ ( 𝐵 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → 𝐷 ∈ ran 𝐿 )
16 7 ad8antr ( ( ( ( ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑚𝑃 ) ∧ 𝑧 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∧ 𝑦𝐷 ) ∧ ( 𝐵 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → 𝐺 ∈ TarskiG )
17 eqid ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) = ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 )
18 10 ad8antr ( ( ( ( ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑚𝑃 ) ∧ 𝑧 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∧ 𝑦𝐷 ) ∧ ( 𝐵 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → 𝐵𝑃 )
19 eqid ( pInvG ‘ 𝐺 ) = ( pInvG ‘ 𝐺 )
20 simp-4r ( ( ( ( ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑚𝑃 ) ∧ 𝑧 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∧ 𝑦𝐷 ) ∧ ( 𝐵 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → 𝑚𝑃 )
21 9 ad8antr ( ( ( ( ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑚𝑃 ) ∧ 𝑧 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∧ 𝑦𝐷 ) ∧ ( 𝐵 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → 𝐴𝑃 )
22 1 2 3 5 19 16 20 17 21 mircl ( ( ( ( ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑚𝑃 ) ∧ 𝑧 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∧ 𝑦𝐷 ) ∧ ( 𝐵 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝐴 ) ∈ 𝑃 )
23 simplr ( ( ( ( ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑚𝑃 ) ∧ 𝑧 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∧ 𝑦𝐷 ) ∧ ( 𝐵 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → 𝑦𝐷 )
24 simp-6r ( ( ( ( ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑚𝑃 ) ∧ 𝑧 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∧ 𝑦𝐷 ) ∧ ( 𝐵 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → 𝑧𝐷 )
25 13 ad8antr ( ( ( ( ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑚𝑃 ) ∧ 𝑧 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∧ 𝑦𝐷 ) ∧ ( 𝐵 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → 𝑅𝐷 )
26 11 ad8antr ( ( ( ( ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑚𝑃 ) ∧ 𝑧 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∧ 𝑦𝐷 ) ∧ ( 𝐵 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → 𝐶𝑃 )
27 simp-8r ( ( ( ( ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑚𝑃 ) ∧ 𝑧 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∧ 𝑦𝐷 ) ∧ ( 𝐵 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → 𝑥𝐷 )
28 12 ad8antr ( ( ( ( ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑚𝑃 ) ∧ 𝑧 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∧ 𝑦𝐷 ) ∧ ( 𝐵 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → 𝐴 𝑂 𝐶 )
29 simp-7r ( ( ( ( ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑚𝑃 ) ∧ 𝑧 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∧ 𝑦𝐷 ) ∧ ( 𝐵 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 )
30 5 16 29 perpln1 ( ( ( ( ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑚𝑃 ) ∧ 𝑧 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∧ 𝑦𝐷 ) ∧ ( 𝐵 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → ( 𝐴 𝐿 𝑥 ) ∈ ran 𝐿 )
31 1 2 3 5 16 30 15 29 perpcom ( ( ( ( ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑚𝑃 ) ∧ 𝑧 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∧ 𝑦𝐷 ) ∧ ( 𝐵 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝑥 ) )
32 simp-5r ( ( ( ( ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑚𝑃 ) ∧ 𝑧 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∧ 𝑦𝐷 ) ∧ ( 𝐵 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 )
33 5 16 32 perpln1 ( ( ( ( ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑚𝑃 ) ∧ 𝑧 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∧ 𝑦𝐷 ) ∧ ( 𝐵 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → ( 𝐶 𝐿 𝑧 ) ∈ ran 𝐿 )
34 1 2 3 5 16 33 15 32 perpcom ( ( ( ( ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑚𝑃 ) ∧ 𝑧 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∧ 𝑦𝐷 ) ∧ ( 𝐵 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐶 𝐿 𝑧 ) )
35 1 5 3 16 15 27 tglnpt ( ( ( ( ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑚𝑃 ) ∧ 𝑧 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∧ 𝑦𝐷 ) ∧ ( 𝐵 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → 𝑥𝑃 )
36 1 3 5 16 21 35 30 tglnne ( ( ( ( ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑚𝑃 ) ∧ 𝑧 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∧ 𝑦𝐷 ) ∧ ( 𝐵 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → 𝐴𝑥 )
37 1 3 8 21 21 35 16 36 hlid ( ( ( ( ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑚𝑃 ) ∧ 𝑧 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∧ 𝑦𝐷 ) ∧ ( 𝐵 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → 𝐴 ( 𝐾𝑥 ) 𝐴 )
38 simpllr ( ( ( ( ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑚𝑃 ) ∧ 𝑧 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∧ 𝑦𝐷 ) ∧ ( 𝐵 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → 𝑧 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑥 ) )
39 38 eqcomd ( ( ( ( ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑚𝑃 ) ∧ 𝑧 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∧ 𝑦𝐷 ) ∧ ( 𝐵 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑥 ) = 𝑧 )
40 1 2 3 4 5 15 16 8 17 21 26 27 24 20 28 31 34 21 39 opphllem6 ( ( ( ( ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑚𝑃 ) ∧ 𝑧 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∧ 𝑦𝐷 ) ∧ ( 𝐵 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → ( 𝐴 ( 𝐾𝑥 ) 𝐴 ↔ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝐴 ) ( 𝐾𝑧 ) 𝐶 ) )
41 37 40 mpbid ( ( ( ( ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑚𝑃 ) ∧ 𝑧 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∧ 𝑦𝐷 ) ∧ ( 𝐵 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝐴 ) ( 𝐾𝑧 ) 𝐶 )
42 1 2 3 4 5 15 16 8 17 21 26 27 24 20 28 31 34 21 22 37 41 opphllem5 ( ( ( ( ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑚𝑃 ) ∧ 𝑧 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∧ 𝑦𝐷 ) ∧ ( 𝐵 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → 𝐴 𝑂 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝐴 ) )
43 39 24 eqeltrd ( ( ( ( ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑚𝑃 ) ∧ 𝑧 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∧ 𝑦𝐷 ) ∧ ( 𝐵 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑥 ) ∈ 𝐷 )
44 1 2 3 5 19 16 17 15 20 27 43 mirln2 ( ( ( ( ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑚𝑃 ) ∧ 𝑧 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∧ 𝑦𝐷 ) ∧ ( 𝐵 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → 𝑚𝐷 )
45 1 2 3 5 19 16 20 17 21 mirmir ( ( ( ( ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑚𝑃 ) ∧ 𝑧 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∧ 𝑦𝐷 ) ∧ ( 𝐵 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝐴 ) ) = 𝐴 )
46 45 eqcomd ( ( ( ( ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑚𝑃 ) ∧ 𝑧 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∧ 𝑦𝐷 ) ∧ ( 𝐵 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → 𝐴 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝐴 ) ) )
47 1 5 3 7 6 13 tglnpt ( 𝜑𝑅𝑃 )
48 1 3 8 9 10 47 7 14 hlne1 ( 𝜑𝐴𝑅 )
49 48 ad8antr ( ( ( ( ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑚𝑃 ) ∧ 𝑧 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∧ 𝑦𝐷 ) ∧ ( 𝐵 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → 𝐴𝑅 )
50 1 3 8 9 10 47 7 14 hlne2 ( 𝜑𝐵𝑅 )
51 50 ad8antr ( ( ( ( ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑚𝑃 ) ∧ 𝑧 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∧ 𝑦𝐷 ) ∧ ( 𝐵 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → 𝐵𝑅 )
52 1 3 8 9 10 47 7 ishlg ( 𝜑 → ( 𝐴 ( 𝐾𝑅 ) 𝐵 ↔ ( 𝐴𝑅𝐵𝑅 ∧ ( 𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ∨ 𝐵 ∈ ( 𝑅 𝐼 𝐴 ) ) ) ) )
53 14 52 mpbid ( 𝜑 → ( 𝐴𝑅𝐵𝑅 ∧ ( 𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ∨ 𝐵 ∈ ( 𝑅 𝐼 𝐴 ) ) ) )
54 53 simp3d ( 𝜑 → ( 𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ∨ 𝐵 ∈ ( 𝑅 𝐼 𝐴 ) ) )
55 54 ad8antr ( ( ( ( ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑚𝑃 ) ∧ 𝑧 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∧ 𝑦𝐷 ) ∧ ( 𝐵 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → ( 𝐴 ∈ ( 𝑅 𝐼 𝐵 ) ∨ 𝐵 ∈ ( 𝑅 𝐼 𝐴 ) ) )
56 1 2 3 4 5 15 16 17 21 18 22 25 42 44 46 49 51 55 opphllem2 ( ( ( ( ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑚𝑃 ) ∧ 𝑧 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∧ 𝑦𝐷 ) ∧ ( 𝐵 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → 𝐵 𝑂 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝐴 ) )
57 simpr ( ( ( ( ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑚𝑃 ) ∧ 𝑧 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∧ 𝑦𝐷 ) ∧ ( 𝐵 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → ( 𝐵 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐷 )
58 5 16 57 perpln1 ( ( ( ( ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑚𝑃 ) ∧ 𝑧 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∧ 𝑦𝐷 ) ∧ ( 𝐵 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → ( 𝐵 𝐿 𝑦 ) ∈ ran 𝐿 )
59 1 2 3 5 16 58 15 57 perpcom ( ( ( ( ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑚𝑃 ) ∧ 𝑧 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∧ 𝑦𝐷 ) ∧ ( 𝐵 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → 𝐷 ( ⟂G ‘ 𝐺 ) ( 𝐵 𝐿 𝑦 ) )
60 1 5 3 16 15 24 tglnpt ( ( ( ( ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑚𝑃 ) ∧ 𝑧 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∧ 𝑦𝐷 ) ∧ ( 𝐵 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → 𝑧𝑃 )
61 1 3 8 22 26 60 16 41 hlne1 ( ( ( ( ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑚𝑃 ) ∧ 𝑧 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∧ 𝑦𝐷 ) ∧ ( 𝐵 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝐴 ) ≠ 𝑧 )
62 1 3 8 22 26 60 16 5 41 hlln ( ( ( ( ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑚𝑃 ) ∧ 𝑧 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∧ 𝑦𝐷 ) ∧ ( 𝐵 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝐴 ) ∈ ( 𝐶 𝐿 𝑧 ) )
63 1 3 5 16 26 60 33 tglnne ( ( ( ( ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑚𝑃 ) ∧ 𝑧 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∧ 𝑦𝐷 ) ∧ ( 𝐵 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → 𝐶𝑧 )
64 1 3 5 16 26 60 63 tglinerflx2 ( ( ( ( ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑚𝑃 ) ∧ 𝑧 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∧ 𝑦𝐷 ) ∧ ( 𝐵 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → 𝑧 ∈ ( 𝐶 𝐿 𝑧 ) )
65 1 3 5 16 22 60 61 61 33 62 64 tglinethru ( ( ( ( ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑚𝑃 ) ∧ 𝑧 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∧ 𝑦𝐷 ) ∧ ( 𝐵 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → ( 𝐶 𝐿 𝑧 ) = ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝐴 ) 𝐿 𝑧 ) )
66 34 65 breqtrd ( ( ( ( ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑚𝑃 ) ∧ 𝑧 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∧ 𝑦𝐷 ) ∧ ( 𝐵 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → 𝐷 ( ⟂G ‘ 𝐺 ) ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝐴 ) 𝐿 𝑧 ) )
67 1 5 3 16 15 23 tglnpt ( ( ( ( ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑚𝑃 ) ∧ 𝑧 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∧ 𝑦𝐷 ) ∧ ( 𝐵 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → 𝑦𝑃 )
68 1 3 5 16 18 67 58 tglnne ( ( ( ( ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑚𝑃 ) ∧ 𝑧 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∧ 𝑦𝐷 ) ∧ ( 𝐵 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → 𝐵𝑦 )
69 1 3 8 18 21 67 16 68 hlid ( ( ( ( ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑚𝑃 ) ∧ 𝑧 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∧ 𝑦𝐷 ) ∧ ( 𝐵 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → 𝐵 ( 𝐾𝑦 ) 𝐵 )
70 1 3 8 22 26 60 16 41 hlcomd ( ( ( ( ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑚𝑃 ) ∧ 𝑧 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∧ 𝑦𝐷 ) ∧ ( 𝐵 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → 𝐶 ( 𝐾𝑧 ) ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝐴 ) )
71 1 2 3 4 5 15 16 8 17 18 22 23 24 20 56 59 66 18 26 69 70 opphllem5 ( ( ( ( ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑚𝑃 ) ∧ 𝑧 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑥 ) ) ∧ 𝑦𝐷 ) ∧ ( 𝐵 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → 𝐵 𝑂 𝐶 )
72 1 2 3 4 5 6 7 9 11 12 oppne1 ( 𝜑 → ¬ 𝐴𝐷 )
73 1 3 8 9 10 47 7 5 14 hlln ( 𝜑𝐴 ∈ ( 𝐵 𝐿 𝑅 ) )
74 73 adantr ( ( 𝜑𝐵𝐷 ) → 𝐴 ∈ ( 𝐵 𝐿 𝑅 ) )
75 7 adantr ( ( 𝜑𝐵𝐷 ) → 𝐺 ∈ TarskiG )
76 10 adantr ( ( 𝜑𝐵𝐷 ) → 𝐵𝑃 )
77 47 adantr ( ( 𝜑𝐵𝐷 ) → 𝑅𝑃 )
78 50 adantr ( ( 𝜑𝐵𝐷 ) → 𝐵𝑅 )
79 6 adantr ( ( 𝜑𝐵𝐷 ) → 𝐷 ∈ ran 𝐿 )
80 simpr ( ( 𝜑𝐵𝐷 ) → 𝐵𝐷 )
81 13 adantr ( ( 𝜑𝐵𝐷 ) → 𝑅𝐷 )
82 1 3 5 75 76 77 78 78 79 80 81 tglinethru ( ( 𝜑𝐵𝐷 ) → 𝐷 = ( 𝐵 𝐿 𝑅 ) )
83 74 82 eleqtrrd ( ( 𝜑𝐵𝐷 ) → 𝐴𝐷 )
84 72 83 mtand ( 𝜑 → ¬ 𝐵𝐷 )
85 1 2 3 5 7 6 10 84 footex ( 𝜑 → ∃ 𝑦𝐷 ( 𝐵 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐷 )
86 85 ad6antr ( ( ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑚𝑃 ) ∧ 𝑧 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑥 ) ) → ∃ 𝑦𝐷 ( 𝐵 𝐿 𝑦 ) ( ⟂G ‘ 𝐺 ) 𝐷 )
87 71 86 r19.29a ( ( ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑚𝑃 ) ∧ 𝑧 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑥 ) ) → 𝐵 𝑂 𝐶 )
88 7 ad4antr ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → 𝐺 ∈ TarskiG )
89 6 ad4antr ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → 𝐷 ∈ ran 𝐿 )
90 simp-4r ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → 𝑥𝐷 )
91 1 5 3 88 89 90 tglnpt ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → 𝑥𝑃 )
92 simplr ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → 𝑧𝐷 )
93 1 5 3 88 89 92 tglnpt ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → 𝑧𝑃 )
94 1 2 3 4 5 6 7 9 11 12 opptgdim2 ( 𝜑𝐺 DimTarskiG≥ 2 )
95 94 ad4antr ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → 𝐺 DimTarskiG≥ 2 )
96 1 2 3 5 88 19 91 93 95 midex ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → ∃ 𝑚𝑃 𝑧 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑚 ) ‘ 𝑥 ) )
97 87 96 r19.29a ( ( ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → 𝐵 𝑂 𝐶 )
98 1 2 3 4 5 6 7 9 11 12 oppne2 ( 𝜑 → ¬ 𝐶𝐷 )
99 1 2 3 5 7 6 11 98 footex ( 𝜑 → ∃ 𝑧𝐷 ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 )
100 99 ad2antrr ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → ∃ 𝑧𝐷 ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 )
101 97 100 r19.29a ( ( ( 𝜑𝑥𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → 𝐵 𝑂 𝐶 )
102 1 2 3 5 7 6 9 72 footex ( 𝜑 → ∃ 𝑥𝐷 ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 )
103 101 102 r19.29a ( 𝜑𝐵 𝑂 𝐶 )