Metamath Proof Explorer

Theorem colperpexlem3

Description: Lemma for colperpex . Case 1 of theorem 8.21 of Schwabhauser p. 63. (Contributed by Thierry Arnoux, 20-Nov-2019)

Ref Expression
Hypotheses colperpex.p ⊢ 𝑃 = ( Base ‘ 𝐺 )
colperpex.d ⊢ − = ( dist ‘ 𝐺 )
colperpex.i ⊢ 𝐼 = ( Itv ‘ 𝐺 )
colperpex.l ⊢ 𝐿 = ( LineG ‘ 𝐺 )
colperpex.g ⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
colperpex.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
colperpex.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
colperpex.3 ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
colperpex.4 ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
colperpexlem3.1 ⊢ ( 𝜑 → ¬ 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) )
Assertion colperpexlem3 ( 𝜑 → ∃ 𝑝 ∈ 𝑃 ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ∃ 𝑡 ∈ 𝑃 ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) ) )

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 colperpex.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
7 colperpex.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝑃 )
8 colperpex.3 ⊢ ( 𝜑 → 𝐶 ∈ 𝑃 )
9 colperpex.4 ⊢ ( 𝜑 → 𝐴 ≠ 𝐵 )
10 colperpexlem3.1 ⊢ ( 𝜑 → ¬ 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) )
11 eqid ⊢ ( pInvG ‘ 𝐺 ) = ( pInvG ‘ 𝐺 )
12 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) → 𝐺 ∈ TarskiG )
13 eqid ⊢ ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) = ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 )
14 1 3 4 5 6 7 9 tgelrnln ⊢ ( 𝜑 → ( 𝐴 𝐿 𝐵 ) ∈ ran 𝐿 )
15 14 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) → ( 𝐴 𝐿 𝐵 ) ∈ ran 𝐿 )
16 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) → 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) )
17 1 4 3 12 15 16 tglnpt ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) → 𝑥 ∈ 𝑃 )
18 eqid ⊢ ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) = ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 )
19 8 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) → 𝐶 ∈ 𝑃 )
20 1 2 3 4 11 12 17 18 19 mircl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ∈ 𝑃 )
21 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) → 𝐴 ∈ 𝑃 )
22 eqid ⊢ ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) = ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 )
23 1 2 3 4 11 12 21 22 19 mircl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) ∈ 𝑃 )
24 1 2 3 4 11 12 21 22 19 mircgr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) → ( 𝐴 − ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) ) = ( 𝐴 − 𝐶 ) )
25 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) → 𝐵 ∈ 𝑃 )
26 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) → ¬ 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) )
27 nelne2 ⊢ ( ( 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ∧ ¬ 𝐶 ∈ ( 𝐴 𝐿 𝐵 ) ) → 𝑥 ≠ 𝐶 )
28 16 26 27 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) → 𝑥 ≠ 𝐶 )
29 1 3 4 12 17 19 28 tgelrnln ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) → ( 𝑥 𝐿 𝐶 ) ∈ ran 𝐿 )
30 1 3 4 12 17 19 28 tglinecom ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) → ( 𝑥 𝐿 𝐶 ) = ( 𝐶 𝐿 𝑥 ) )
31 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) → ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) )
32 30 31 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) → ( 𝑥 𝐿 𝐶 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) )
33 1 2 3 4 12 29 15 32 perpcom ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) → ( 𝐴 𝐿 𝐵 ) ( ⟂G ‘ 𝐺 ) ( 𝑥 𝐿 𝐶 ) )
34 1 2 3 4 12 21 25 16 19 33 perprag ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) → ⟨“ 𝐴 𝑥 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
35 1 2 3 4 11 12 21 17 19 israg ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) → ( ⟨“ 𝐴 𝑥 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) ↔ ( 𝐴 − 𝐶 ) = ( 𝐴 − ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) )
36 34 35 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) → ( 𝐴 − 𝐶 ) = ( 𝐴 − ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) )
37 24 36 eqtr2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) → ( 𝐴 − ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) = ( 𝐴 − ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) ) )
38 1 2 3 4 11 12 13 20 23 21 37 midexlem ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) → ∃ 𝑝 ∈ 𝑃 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) )
39 12 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) → 𝐺 ∈ TarskiG )
40 23 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) ∈ 𝑃 )
41 21 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) → 𝐴 ∈ 𝑃 )
42 19 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) → 𝐶 ∈ 𝑃 )
43 20 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ∈ 𝑃 )
44 17 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) → 𝑥 ∈ 𝑃 )
45 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) → 𝑝 ∈ 𝑃 )
46 1 2 3 4 11 39 41 22 42 mirbtwn ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) → 𝐴 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) 𝐼 𝐶 ) )
47 1 2 3 4 11 39 44 18 42 mirbtwn ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) → 𝑥 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) 𝐼 𝐶 ) )
48 1 2 3 4 11 39 45 13 43 mirbtwn ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) → 𝑝 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) )
49 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) )
50 49 eqcomd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) )
51 50 oveq1d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) → ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) = ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) )
52 48 51 eleqtrd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) → 𝑝 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) 𝐼 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) )
53 1 2 3 39 40 41 42 43 44 45 46 47 52 tgtrisegint ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) → ∃ 𝑡 ∈ 𝑃 ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) )
54 39 ad3antrrr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 = 𝐴 ) → 𝐺 ∈ TarskiG )
55 41 ad3antrrr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 = 𝐴 ) → 𝐴 ∈ 𝑃 )
56 simpllr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 = 𝐴 ) → 𝑡 ∈ 𝑃 )
57 simplrr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 = 𝐴 ) → 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) )
58 simpr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 = 𝐴 ) → 𝑥 = 𝐴 )
59 58 oveq2d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 = 𝐴 ) → ( 𝐴 𝐼 𝑥 ) = ( 𝐴 𝐼 𝐴 ) )
60 57 59 eleqtrd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 = 𝐴 ) → 𝑡 ∈ ( 𝐴 𝐼 𝐴 ) )
61 1 2 3 54 55 56 60 axtgbtwnid ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 = 𝐴 ) → 𝐴 = 𝑡 )
62 61 eqcomd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 = 𝐴 ) → 𝑡 = 𝐴 )
63 62 oveq1d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 = 𝐴 ) → ( 𝑡 𝐿 𝑝 ) = ( 𝐴 𝐿 𝑝 ) )
64 50 ad3antrrr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 = 𝐴 ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) )
65 58 fveq2d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 = 𝐴 ) → ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) = ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) )
66 65 fveq1d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 = 𝐴 ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) )
67 64 66 eqtr4d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 = 𝐴 ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) )
68 45 ad3antrrr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 = 𝐴 ) → 𝑝 ∈ 𝑃 )
69 43 ad3antrrr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 = 𝐴 ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ∈ 𝑃 )
70 1 2 3 4 11 54 68 13 69 mirinv ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 = 𝐴 ) → ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ↔ 𝑝 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) )
71 67 70 mpbid ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 = 𝐴 ) → 𝑝 = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) )
72 44 ad3antrrr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 = 𝐴 ) → 𝑥 ∈ 𝑃 )
73 58 oveq1d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 = 𝐴 ) → ( 𝑥 𝐼 𝑥 ) = ( 𝐴 𝐼 𝑥 ) )
74 57 73 eleqtrrd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 = 𝐴 ) → 𝑡 ∈ ( 𝑥 𝐼 𝑥 ) )
75 1 2 3 54 72 56 74 axtgbtwnid ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 = 𝐴 ) → 𝑥 = 𝑡 )
76 75 eqcomd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 = 𝐴 ) → 𝑡 = 𝑥 )
77 71 76 oveq12d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 = 𝐴 ) → ( 𝑝 𝐿 𝑡 ) = ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) 𝐿 𝑥 ) )
78 34 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) → ⟨“ 𝐴 𝑥 𝐶 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
79 1 2 3 4 11 39 45 13 43 50 mircom ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) )
80 28 ad2antrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) → 𝑥 ≠ 𝐶 )
81 1 2 3 4 39 11 22 18 13 41 44 42 45 78 79 80 colperpexlem2 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) → 𝐴 ≠ 𝑝 )
82 81 ad3antrrr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 = 𝐴 ) → 𝐴 ≠ 𝑝 )
83 62 82 eqnetrd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 = 𝐴 ) → 𝑡 ≠ 𝑝 )
84 1 3 4 54 56 68 83 tglinecom ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 = 𝐴 ) → ( 𝑡 𝐿 𝑝 ) = ( 𝑝 𝐿 𝑡 ) )
85 42 ad3antrrr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 = 𝐴 ) → 𝐶 ∈ 𝑃 )
86 80 ad3antrrr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 = 𝐴 ) → 𝑥 ≠ 𝐶 )
87 54 adantr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 = 𝐴 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) = 𝑥 ) → 𝐺 ∈ TarskiG )
88 72 adantr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 = 𝐴 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) = 𝑥 ) → 𝑥 ∈ 𝑃 )
89 85 adantr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 = 𝐴 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) = 𝑥 ) → 𝐶 ∈ 𝑃 )
90 1 2 3 4 11 87 88 18 mircinv ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 = 𝐴 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) = 𝑥 ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝑥 ) = 𝑥 )
91 simpr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 = 𝐴 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) = 𝑥 ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) = 𝑥 )
92 90 91 eqtr4d ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 = 𝐴 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) = 𝑥 ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝑥 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) )
93 1 2 3 4 11 87 88 18 88 89 92 mireq ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 = 𝐴 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) = 𝑥 ) → 𝑥 = 𝐶 )
94 86 adantr ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 = 𝐴 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) = 𝑥 ) → 𝑥 ≠ 𝐶 )
95 94 neneqd ⊢ ( ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 = 𝐴 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) = 𝑥 ) → ¬ 𝑥 = 𝐶 )
96 93 95 pm2.65da ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 = 𝐴 ) → ¬ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) = 𝑥 )
97 96 neqned ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 = 𝐴 ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ≠ 𝑥 )
98 47 ad3antrrr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 = 𝐴 ) → 𝑥 ∈ ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) 𝐼 𝐶 ) )
99 1 3 4 54 72 85 69 86 98 btwnlng2 ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 = 𝐴 ) → ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ∈ ( 𝑥 𝐿 𝐶 ) )
100 1 3 4 54 72 85 86 69 97 99 tglineelsb2 ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 = 𝐴 ) → ( 𝑥 𝐿 𝐶 ) = ( 𝑥 𝐿 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) )
101 28 necomd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) → 𝐶 ≠ 𝑥 )
102 101 ad5antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 = 𝐴 ) → 𝐶 ≠ 𝑥 )
103 1 3 4 54 85 72 102 tglinecom ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 = 𝐴 ) → ( 𝐶 𝐿 𝑥 ) = ( 𝑥 𝐿 𝐶 ) )
104 1 3 4 54 69 72 97 tglinecom ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 = 𝐴 ) → ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) 𝐿 𝑥 ) = ( 𝑥 𝐿 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) )
105 100 103 104 3eqtr4d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 = 𝐴 ) → ( 𝐶 𝐿 𝑥 ) = ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) 𝐿 𝑥 ) )
106 77 84 105 3eqtr4d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 = 𝐴 ) → ( 𝑡 𝐿 𝑝 ) = ( 𝐶 𝐿 𝑥 ) )
107 63 106 eqtr3d ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 = 𝐴 ) → ( 𝐴 𝐿 𝑝 ) = ( 𝐶 𝐿 𝑥 ) )
108 31 ad5antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 = 𝐴 ) → ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) )
109 107 108 eqbrtrd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 = 𝐴 ) → ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) )
110 39 ad3antrrr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 ≠ 𝐴 ) → 𝐺 ∈ TarskiG )
111 41 ad3antrrr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 ≠ 𝐴 ) → 𝐴 ∈ 𝑃 )
112 45 ad3antrrr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 ≠ 𝐴 ) → 𝑝 ∈ 𝑃 )
113 81 ad3antrrr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 ≠ 𝐴 ) → 𝐴 ≠ 𝑝 )
114 1 3 4 110 111 112 113 tgelrnln ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 ≠ 𝐴 ) → ( 𝐴 𝐿 𝑝 ) ∈ ran 𝐿 )
115 15 ad5antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 ≠ 𝐴 ) → ( 𝐴 𝐿 𝐵 ) ∈ ran 𝐿 )
116 1 3 4 110 111 112 113 tglinerflx1 ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 ≠ 𝐴 ) → 𝐴 ∈ ( 𝐴 𝐿 𝑝 ) )
117 9 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) → 𝐴 ≠ 𝐵 )
118 1 3 4 12 21 25 117 tglinerflx1 ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) → 𝐴 ∈ ( 𝐴 𝐿 𝐵 ) )
119 118 ad5antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 ≠ 𝐴 ) → 𝐴 ∈ ( 𝐴 𝐿 𝐵 ) )
120 116 119 elind ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 ≠ 𝐴 ) → 𝐴 ∈ ( ( 𝐴 𝐿 𝑝 ) ∩ ( 𝐴 𝐿 𝐵 ) ) )
121 1 3 4 110 111 112 113 tglinerflx2 ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 ≠ 𝐴 ) → 𝑝 ∈ ( 𝐴 𝐿 𝑝 ) )
122 16 ad5antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 ≠ 𝐴 ) → 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) )
123 113 necomd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 ≠ 𝐴 ) → 𝑝 ≠ 𝐴 )
124 simpr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 ≠ 𝐴 ) → 𝑥 ≠ 𝐴 )
125 44 ad3antrrr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 ≠ 𝐴 ) → 𝑥 ∈ 𝑃 )
126 1 2 3 4 39 11 22 18 13 41 44 42 45 78 79 colperpexlem1 ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) → ⟨“ 𝑥 𝐴 𝑝 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
127 126 ad3antrrr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 ≠ 𝐴 ) → ⟨“ 𝑥 𝐴 𝑝 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
128 1 2 3 4 11 110 125 111 112 127 ragcom ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 ≠ 𝐴 ) → ⟨“ 𝑝 𝐴 𝑥 ”⟩ ∈ ( ∟G ‘ 𝐺 ) )
129 1 2 3 4 110 114 115 120 121 122 123 124 128 ragperp ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 ≠ 𝐴 ) → ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) )
130 109 129 pm2.61dane ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) → ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) )
131 118 ad5antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 = 𝐴 ) → 𝐴 ∈ ( 𝐴 𝐿 𝐵 ) )
132 62 131 eqeltrd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 = 𝐴 ) → 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) )
133 132 orcd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 = 𝐴 ) → ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
134 25 ad5antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 ≠ 𝐴 ) → 𝐵 ∈ 𝑃 )
135 117 ad5antr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 ≠ 𝐴 ) → 𝐴 ≠ 𝐵 )
136 simpllr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 ≠ 𝐴 ) → 𝑡 ∈ 𝑃 )
137 124 necomd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 ≠ 𝐴 ) → 𝐴 ≠ 𝑥 )
138 simplrr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 ≠ 𝐴 ) → 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) )
139 1 3 4 110 111 125 136 137 138 btwnlng1 ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 ≠ 𝐴 ) → 𝑡 ∈ ( 𝐴 𝐿 𝑥 ) )
140 1 3 4 110 111 134 135 125 124 122 136 139 tglineeltr ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 ≠ 𝐴 ) → 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) )
141 140 orcd ⊢ ( ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) ∧ 𝑥 ≠ 𝐴 ) → ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
142 133 141 pm2.61dane ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) → ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) )
143 39 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) → 𝐺 ∈ TarskiG )
144 45 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) → 𝑝 ∈ 𝑃 )
145 simplr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) → 𝑡 ∈ 𝑃 )
146 42 ad2antrr ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) → 𝐶 ∈ 𝑃 )
147 simprl ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) → 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) )
148 1 2 3 143 144 145 146 147 tgbtwncom ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) → 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) )
149 130 142 148 jca32 ⊢ ( ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) ∧ ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) ) → ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) ) )
150 149 ex ⊢ ( ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) ∧ 𝑡 ∈ 𝑃 ) → ( ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) → ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) ) ) )
151 150 reximdva ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) → ( ∃ 𝑡 ∈ 𝑃 ( 𝑡 ∈ ( 𝑝 𝐼 𝐶 ) ∧ 𝑡 ∈ ( 𝐴 𝐼 𝑥 ) ) → ∃ 𝑡 ∈ 𝑃 ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) ) ) )
152 53 151 mpd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) → ∃ 𝑡 ∈ 𝑃 ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) ) )
153 r19.42v ⊢ ( ∃ 𝑡 ∈ 𝑃 ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) ) ↔ ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ∃ 𝑡 ∈ 𝑃 ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) ) )
154 152 153 sylib ⊢ ( ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) ∧ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) ) → ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ∃ 𝑡 ∈ 𝑃 ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) ) )
155 154 ex ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) ∧ 𝑝 ∈ 𝑃 ) → ( ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) → ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ∃ 𝑡 ∈ 𝑃 ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) ) ) )
156 155 reximdva ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) → ( ∃ 𝑝 ∈ 𝑃 ( ( ( pInvG ‘ 𝐺 ) ‘ 𝐴 ) ‘ 𝐶 ) = ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑝 ) ‘ ( ( ( pInvG ‘ 𝐺 ) ‘ 𝑥 ) ‘ 𝐶 ) ) → ∃ 𝑝 ∈ 𝑃 ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ∃ 𝑡 ∈ 𝑃 ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) ) ) )
157 38 156 mpd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ) ∧ ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ) → ∃ 𝑝 ∈ 𝑃 ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ∃ 𝑡 ∈ 𝑃 ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) ) )
158 1 2 3 4 5 14 8 10 footex ⊢ ( 𝜑 → ∃ 𝑥 ∈ ( 𝐴 𝐿 𝐵 ) ( 𝐶 𝐿 𝑥 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) )
159 157 158 r19.29a ⊢ ( 𝜑 → ∃ 𝑝 ∈ 𝑃 ( ( 𝐴 𝐿 𝑝 ) ( ⟂G ‘ 𝐺 ) ( 𝐴 𝐿 𝐵 ) ∧ ∃ 𝑡 ∈ 𝑃 ( ( 𝑡 ∈ ( 𝐴 𝐿 𝐵 ) ∨ 𝐴 = 𝐵 ) ∧ 𝑡 ∈ ( 𝐶 𝐼 𝑝 ) ) ) )