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	⊢ ( 𝜑 → 𝐺 Dim_TarskiG≥ 2 )
95	94	ad4antr	⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐷 ) ∧ ( 𝐴 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) ∧ 𝑧 ∈ 𝐷 ) ∧ ( 𝐶 𝐿 𝑧 ) ( ⟂G ‘ 𝐺 ) 𝐷 ) → 𝐺 Dim_TarskiG≥ 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	⊢ ( 𝜑 → 𝐵 𝑂 𝐶 )

Metamath Proof Explorer

Theorem opphl

Proof