MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  footexALT Structured version   Visualization version   GIF version

Theorem footexALT 27660
Description: Alternative version of footex 27663 which minimization requires a notably long time. (Contributed by Thierry Arnoux, 19-Oct-2019.) (New usage is discouraged.) (Proof modification is discouraged.)
Hypotheses
Ref Expression
isperp.p 𝑃 = (Base‘𝐺)
isperp.d = (dist‘𝐺)
isperp.i 𝐼 = (Itv‘𝐺)
isperp.l 𝐿 = (LineG‘𝐺)
isperp.g (𝜑𝐺 ∈ TarskiG)
isperp.a (𝜑𝐴 ∈ ran 𝐿)
foot.x (𝜑𝐶𝑃)
foot.y (𝜑 → ¬ 𝐶𝐴)
Assertion
Ref Expression
footexALT (𝜑 → ∃𝑥𝐴 (𝐶𝐿𝑥)(⟂G‘𝐺)𝐴)
Distinct variable groups:   𝑥,𝐴   𝑥,𝐺   𝜑,𝑥   𝑥,𝐶   𝑥,𝐼   𝑥,   𝑥,𝐿   𝑥,𝑃

Proof of Theorem footexALT
Dummy variables 𝑎 𝑏 𝑑 𝑝 𝑞 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 isperp.p . . . . . . . . 9 𝑃 = (Base‘𝐺)
2 isperp.d . . . . . . . . 9 = (dist‘𝐺)
3 isperp.i . . . . . . . . 9 𝐼 = (Itv‘𝐺)
4 isperp.l . . . . . . . . 9 𝐿 = (LineG‘𝐺)
5 eqid 2736 . . . . . . . . 9 (pInvG‘𝐺) = (pInvG‘𝐺)
6 isperp.g . . . . . . . . . . . . . . 15 (𝜑𝐺 ∈ TarskiG)
76ad3antrrr 728 . . . . . . . . . . . . . 14 ((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) → 𝐺 ∈ TarskiG)
87ad2antrr 724 . . . . . . . . . . . . 13 ((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) → 𝐺 ∈ TarskiG)
98ad2antrr 724 . . . . . . . . . . . 12 ((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) → 𝐺 ∈ TarskiG)
109ad2antrr 724 . . . . . . . . . . 11 ((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) → 𝐺 ∈ TarskiG)
1110ad2antrr 724 . . . . . . . . . 10 ((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) → 𝐺 ∈ TarskiG)
1211ad2antrr 724 . . . . . . . . 9 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → 𝐺 ∈ TarskiG)
13 eqid 2736 . . . . . . . . 9 ((pInvG‘𝐺)‘𝑥) = ((pInvG‘𝐺)‘𝑥)
14 foot.x . . . . . . . . . . . . 13 (𝜑𝐶𝑃)
1514ad3antrrr 728 . . . . . . . . . . . 12 ((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) → 𝐶𝑃)
1615ad2antrr 724 . . . . . . . . . . 11 ((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) → 𝐶𝑃)
1716ad6antr 734 . . . . . . . . . 10 ((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) → 𝐶𝑃)
1817ad2antrr 724 . . . . . . . . 9 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → 𝐶𝑃)
19 simplr 767 . . . . . . . . 9 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → 𝑑𝑃)
20 simp-4r 782 . . . . . . . . . . . 12 ((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) → 𝑦𝑃)
2120ad2antrr 724 . . . . . . . . . . 11 ((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) → 𝑦𝑃)
2221ad2antrr 724 . . . . . . . . . 10 ((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) → 𝑦𝑃)
2322ad2antrr 724 . . . . . . . . 9 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → 𝑦𝑃)
24 simprr 771 . . . . . . . . . 10 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → (𝑦 𝑑) = (𝑦 𝐶))
2524eqcomd 2742 . . . . . . . . 9 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → (𝑦 𝐶) = (𝑦 𝑑))
261, 2, 3, 4, 5, 12, 13, 18, 19, 23, 25midexlem 27634 . . . . . . . 8 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → ∃𝑥𝑃 𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))
2712adantr 481 . . . . . . . . . 10 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝐺 ∈ TarskiG)
2823adantr 481 . . . . . . . . . 10 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑦𝑃)
29 simp-6r 786 . . . . . . . . . . 11 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → 𝑧𝑃)
3029adantr 481 . . . . . . . . . 10 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑧𝑃)
31 simprl 769 . . . . . . . . . 10 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑥𝑃)
32 simp-4r 782 . . . . . . . . . . . . 13 ((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) → 𝑝𝑃)
3332ad4antr 730 . . . . . . . . . . . 12 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → 𝑝𝑃)
3433adantr 481 . . . . . . . . . . 11 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑝𝑃)
35 simp-5r 784 . . . . . . . . . . . . . 14 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝)))
3635simprd 496 . . . . . . . . . . . . 13 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → (𝑦 𝑧) = (𝑦 𝑝))
3736eqcomd 2742 . . . . . . . . . . . 12 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → (𝑦 𝑝) = (𝑦 𝑧))
3837adantr 481 . . . . . . . . . . 11 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → (𝑦 𝑝) = (𝑦 𝑧))
39 simp-7r 788 . . . . . . . . . . . . . . 15 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦))
4039adantr 481 . . . . . . . . . . . . . 14 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦))
41 simpllr 774 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) → 𝑎𝑃)
4241ad2antrr 724 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) → 𝑎𝑃)
4342ad2antrr 724 . . . . . . . . . . . . . . . . . . . . 21 ((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) → 𝑎𝑃)
4443ad2antrr 724 . . . . . . . . . . . . . . . . . . . 20 ((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) → 𝑎𝑃)
4544ad4antr 730 . . . . . . . . . . . . . . . . . . 19 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → 𝑎𝑃)
46 simplr 767 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) → 𝑏𝑃)
4746ad10antr 742 . . . . . . . . . . . . . . . . . . 19 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → 𝑏𝑃)
48 simp-11r 796 . . . . . . . . . . . . . . . . . . . 20 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏))
4948simprd 496 . . . . . . . . . . . . . . . . . . 19 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → 𝑎𝑏)
5049necomd 2999 . . . . . . . . . . . . . . . . . . . 20 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → 𝑏𝑎)
51 simp-9r 792 . . . . . . . . . . . . . . . . . . . . 21 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶)))
5251simpld 495 . . . . . . . . . . . . . . . . . . . 20 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → 𝑎 ∈ (𝑏𝐼𝑦))
531, 3, 4, 12, 47, 45, 23, 50, 52btwnlng3 27563 . . . . . . . . . . . . . . . . . . 19 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → 𝑦 ∈ (𝑏𝐿𝑎))
541, 3, 4, 12, 45, 47, 23, 49, 53lncom 27564 . . . . . . . . . . . . . . . . . 18 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → 𝑦 ∈ (𝑎𝐿𝑏))
5548simpld 495 . . . . . . . . . . . . . . . . . 18 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → 𝐴 = (𝑎𝐿𝑏))
5654, 55eleqtrrd 2841 . . . . . . . . . . . . . . . . 17 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → 𝑦𝐴)
5756adantr 481 . . . . . . . . . . . . . . . 16 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑦𝐴)
58 foot.y . . . . . . . . . . . . . . . . . . 19 (𝜑 → ¬ 𝐶𝐴)
5958ad3antrrr 728 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) → ¬ 𝐶𝐴)
6059ad10antr 742 . . . . . . . . . . . . . . . . 17 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → ¬ 𝐶𝐴)
6160adantr 481 . . . . . . . . . . . . . . . 16 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → ¬ 𝐶𝐴)
62 nelne2 3042 . . . . . . . . . . . . . . . 16 ((𝑦𝐴 ∧ ¬ 𝐶𝐴) → 𝑦𝐶)
6357, 61, 62syl2anc 584 . . . . . . . . . . . . . . 15 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑦𝐶)
6463necomd 2999 . . . . . . . . . . . . . 14 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝐶𝑦)
6540, 64eqnetrrd 3012 . . . . . . . . . . . . 13 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → (((pInvG‘𝐺)‘𝑝)‘𝑦) ≠ 𝑦)
66 eqid 2736 . . . . . . . . . . . . . . 15 ((pInvG‘𝐺)‘𝑝) = ((pInvG‘𝐺)‘𝑝)
671, 2, 3, 4, 5, 27, 34, 66, 28mirinv 27608 . . . . . . . . . . . . . 14 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → ((((pInvG‘𝐺)‘𝑝)‘𝑦) = 𝑦𝑝 = 𝑦))
6867necon3bid 2988 . . . . . . . . . . . . 13 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → ((((pInvG‘𝐺)‘𝑝)‘𝑦) ≠ 𝑦𝑝𝑦))
6965, 68mpbid 231 . . . . . . . . . . . 12 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑝𝑦)
7069necomd 2999 . . . . . . . . . . 11 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑦𝑝)
711, 2, 3, 27, 28, 34, 28, 30, 38, 70tgcgrneq 27425 . . . . . . . . . 10 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑦𝑧)
7271necomd 2999 . . . . . . . . . . 11 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑧𝑦)
73 eqid 2736 . . . . . . . . . . . 12 ((pInvG‘𝐺)‘𝑧) = ((pInvG‘𝐺)‘𝑧)
74 simp-4r 782 . . . . . . . . . . . . 13 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → 𝑞𝑃)
7574adantr 481 . . . . . . . . . . . 12 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑞𝑃)
76 simp-4r 782 . . . . . . . . . . . . . 14 ((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) → 𝑧𝑃)
77 simplr 767 . . . . . . . . . . . . . 14 ((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) → 𝑞𝑃)
781, 2, 3, 4, 5, 11, 76, 73, 77mircl 27603 . . . . . . . . . . . . 13 ((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) → (((pInvG‘𝐺)‘𝑧)‘𝑞) ∈ 𝑃)
7978ad3antrrr 728 . . . . . . . . . . . 12 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → (((pInvG‘𝐺)‘𝑧)‘𝑞) ∈ 𝑃)
8018adantr 481 . . . . . . . . . . . 12 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝐶𝑃)
81 simpllr 774 . . . . . . . . . . . 12 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑑𝑃)
821, 2, 3, 4, 5, 27, 34, 66, 28mirbtwn 27600 . . . . . . . . . . . . . . 15 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑝 ∈ ((((pInvG‘𝐺)‘𝑝)‘𝑦)𝐼𝑦))
8340oveq1d 7372 . . . . . . . . . . . . . . 15 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → (𝐶𝐼𝑦) = ((((pInvG‘𝐺)‘𝑝)‘𝑦)𝐼𝑦))
8482, 83eleqtrrd 2841 . . . . . . . . . . . . . 14 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑝 ∈ (𝐶𝐼𝑦))
85 simpllr 774 . . . . . . . . . . . . . . . 16 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎)))
8685simpld 495 . . . . . . . . . . . . . . 15 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → 𝑦 ∈ (𝑝𝐼𝑞))
8786adantr 481 . . . . . . . . . . . . . 14 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑦 ∈ (𝑝𝐼𝑞))
881, 2, 3, 27, 80, 34, 28, 75, 69, 84, 87tgbtwnouttr2 27437 . . . . . . . . . . . . 13 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑦 ∈ (𝐶𝐼𝑞))
891, 2, 3, 27, 80, 28, 75, 88tgbtwncom 27430 . . . . . . . . . . . 12 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑦 ∈ (𝑞𝐼𝐶))
90 simplrl 775 . . . . . . . . . . . 12 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑))
91 eqid 2736 . . . . . . . . . . . . . . . 16 (cgrG‘𝐺) = (cgrG‘𝐺)
9251simprd 496 . . . . . . . . . . . . . . . . . 18 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → (𝑎 𝑦) = (𝑎 𝐶))
9339oveq2d 7373 . . . . . . . . . . . . . . . . . 18 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → (𝑎 𝐶) = (𝑎 (((pInvG‘𝐺)‘𝑝)‘𝑦)))
9492, 93eqtrd 2776 . . . . . . . . . . . . . . . . 17 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → (𝑎 𝑦) = (𝑎 (((pInvG‘𝐺)‘𝑝)‘𝑦)))
951, 2, 3, 4, 5, 12, 45, 33, 23israg 27639 . . . . . . . . . . . . . . . . 17 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → (⟨“𝑎𝑝𝑦”⟩ ∈ (∟G‘𝐺) ↔ (𝑎 𝑦) = (𝑎 (((pInvG‘𝐺)‘𝑝)‘𝑦))))
9694, 95mpbird 256 . . . . . . . . . . . . . . . 16 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → ⟨“𝑎𝑝𝑦”⟩ ∈ (∟G‘𝐺))
9785simprd 496 . . . . . . . . . . . . . . . . . . . . . 22 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → (𝑦 𝑞) = (𝑦 𝑎))
981, 2, 3, 12, 45, 23, 45, 18, 92tgcgrcomlr 27422 . . . . . . . . . . . . . . . . . . . . . 22 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → (𝑦 𝑎) = (𝐶 𝑎))
9997, 98eqtr2d 2777 . . . . . . . . . . . . . . . . . . . . 21 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → (𝐶 𝑎) = (𝑦 𝑞))
1001, 3, 4, 12, 45, 47, 49tglinerflx1 27575 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → 𝑎 ∈ (𝑎𝐿𝑏))
101100, 55eleqtrrd 2841 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → 𝑎𝐴)
102 nelne2 3042 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑎𝐴 ∧ ¬ 𝐶𝐴) → 𝑎𝐶)
103101, 60, 102syl2anc 584 . . . . . . . . . . . . . . . . . . . . . 22 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → 𝑎𝐶)
104103necomd 2999 . . . . . . . . . . . . . . . . . . . . 21 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → 𝐶𝑎)
1051, 2, 3, 12, 18, 45, 23, 74, 99, 104tgcgrneq 27425 . . . . . . . . . . . . . . . . . . . 20 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → 𝑦𝑞)
106105necomd 2999 . . . . . . . . . . . . . . . . . . 19 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → 𝑞𝑦)
1071, 2, 3, 12, 33, 23, 74, 86tgbtwncom 27430 . . . . . . . . . . . . . . . . . . 19 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → 𝑦 ∈ (𝑞𝐼𝑝))
10835simpld 495 . . . . . . . . . . . . . . . . . . 19 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → 𝑦 ∈ (𝑎𝐼𝑧))
1091, 2, 3, 12, 23, 74, 23, 45, 97tgcgrcomlr 27422 . . . . . . . . . . . . . . . . . . 19 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → (𝑞 𝑦) = (𝑎 𝑦))
1101, 2, 3, 12, 74, 45axtgcgrrflx 27404 . . . . . . . . . . . . . . . . . . 19 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → (𝑞 𝑎) = (𝑎 𝑞))
11197eqcomd 2742 . . . . . . . . . . . . . . . . . . 19 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → (𝑦 𝑎) = (𝑦 𝑞))
1121, 2, 3, 12, 74, 23, 33, 45, 23, 29, 45, 74, 106, 107, 108, 109, 37, 110, 111axtg5seg 27407 . . . . . . . . . . . . . . . . . 18 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → (𝑝 𝑎) = (𝑧 𝑞))
1131, 2, 3, 12, 33, 45, 29, 74, 112tgcgrcomlr 27422 . . . . . . . . . . . . . . . . 17 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → (𝑎 𝑝) = (𝑞 𝑧))
1141, 2, 3, 12, 23, 33, 23, 29, 37tgcgrcomlr 27422 . . . . . . . . . . . . . . . . 17 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → (𝑝 𝑦) = (𝑧 𝑦))
1151, 2, 91, 12, 45, 33, 23, 74, 29, 23, 113, 114, 111trgcgr 27458 . . . . . . . . . . . . . . . 16 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → ⟨“𝑎𝑝𝑦”⟩(cgrG‘𝐺)⟨“𝑞𝑧𝑦”⟩)
1161, 2, 3, 4, 5, 12, 45, 33, 23, 91, 74, 29, 23, 96, 115ragcgr 27649 . . . . . . . . . . . . . . 15 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → ⟨“𝑞𝑧𝑦”⟩ ∈ (∟G‘𝐺))
1171, 2, 3, 4, 5, 12, 74, 29, 23, 116ragcom 27640 . . . . . . . . . . . . . 14 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → ⟨“𝑦𝑧𝑞”⟩ ∈ (∟G‘𝐺))
1181, 2, 3, 4, 5, 12, 23, 29, 74israg 27639 . . . . . . . . . . . . . 14 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → (⟨“𝑦𝑧𝑞”⟩ ∈ (∟G‘𝐺) ↔ (𝑦 𝑞) = (𝑦 (((pInvG‘𝐺)‘𝑧)‘𝑞))))
119117, 118mpbid 231 . . . . . . . . . . . . 13 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → (𝑦 𝑞) = (𝑦 (((pInvG‘𝐺)‘𝑧)‘𝑞)))
120119adantr 481 . . . . . . . . . . . 12 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → (𝑦 𝑞) = (𝑦 (((pInvG‘𝐺)‘𝑧)‘𝑞)))
12125adantr 481 . . . . . . . . . . . 12 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → (𝑦 𝐶) = (𝑦 𝑑))
122 eqidd 2737 . . . . . . . . . . . 12 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → (((pInvG‘𝐺)‘𝑧)‘𝑞) = (((pInvG‘𝐺)‘𝑧)‘𝑞))
123 simprr 771 . . . . . . . . . . . 12 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))
1241, 2, 3, 4, 5, 27, 73, 13, 75, 79, 28, 80, 81, 30, 31, 89, 90, 120, 121, 122, 123krippen 27633 . . . . . . . . . . 11 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑦 ∈ (𝑧𝐼𝑥))
1251, 3, 4, 27, 30, 28, 31, 72, 124btwnlng3 27563 . . . . . . . . . 10 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑥 ∈ (𝑧𝐿𝑦))
1261, 3, 4, 27, 28, 30, 31, 71, 125lncom 27564 . . . . . . . . 9 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑥 ∈ (𝑦𝐿𝑧))
127 isperp.a . . . . . . . . . . . 12 (𝜑𝐴 ∈ ran 𝐿)
128127ad5antr 732 . . . . . . . . . . 11 ((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) → 𝐴 ∈ ran 𝐿)
129128ad9antr 740 . . . . . . . . . 10 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝐴 ∈ ran 𝐿)
13045adantr 481 . . . . . . . . . . . 12 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑎𝑃)
13192adantr 481 . . . . . . . . . . . . . 14 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → (𝑎 𝑦) = (𝑎 𝐶))
132131eqcomd 2742 . . . . . . . . . . . . 13 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → (𝑎 𝐶) = (𝑎 𝑦))
133103adantr 481 . . . . . . . . . . . . 13 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑎𝐶)
1341, 2, 3, 27, 130, 80, 130, 28, 132, 133tgcgrneq 27425 . . . . . . . . . . . 12 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑎𝑦)
135108adantr 481 . . . . . . . . . . . 12 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑦 ∈ (𝑎𝐼𝑧))
1361, 3, 4, 27, 130, 28, 30, 134, 135btwnlng3 27563 . . . . . . . . . . 11 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑧 ∈ (𝑎𝐿𝑦))
137101adantr 481 . . . . . . . . . . . 12 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑎𝐴)
1381, 3, 4, 27, 130, 28, 134, 134, 129, 137, 57tglinethru 27578 . . . . . . . . . . 11 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝐴 = (𝑎𝐿𝑦))
139136, 138eleqtrrd 2841 . . . . . . . . . 10 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑧𝐴)
1401, 3, 4, 27, 28, 30, 71, 71, 129, 57, 139tglinethru 27578 . . . . . . . . 9 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝐴 = (𝑦𝐿𝑧))
141126, 140eleqtrrd 2841 . . . . . . . 8 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑥𝐴)
142 nelne2 3042 . . . . . . . . . . . 12 ((𝑥𝐴 ∧ ¬ 𝐶𝐴) → 𝑥𝐶)
143141, 61, 142syl2anc 584 . . . . . . . . . . 11 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑥𝐶)
144143necomd 2999 . . . . . . . . . 10 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝐶𝑥)
1451, 3, 4, 27, 80, 31, 144tgelrnln 27572 . . . . . . . . 9 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → (𝐶𝐿𝑥) ∈ ran 𝐿)
1461, 3, 4, 27, 80, 31, 144tglinerflx2 27576 . . . . . . . . . 10 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑥 ∈ (𝐶𝐿𝑥))
147146, 141elind 4154 . . . . . . . . 9 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑥 ∈ ((𝐶𝐿𝑥) ∩ 𝐴))
1481, 3, 4, 27, 80, 31, 144tglinerflx1 27575 . . . . . . . . 9 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝐶 ∈ (𝐶𝐿𝑥))
14927adantr 481 . . . . . . . . . . . 12 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → 𝐺 ∈ TarskiG)
150130adantr 481 . . . . . . . . . . . 12 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → 𝑎𝑃)
15128adantr 481 . . . . . . . . . . . 12 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → 𝑦𝑃)
15234adantr 481 . . . . . . . . . . . 12 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → 𝑝𝑃)
15380adantr 481 . . . . . . . . . . . . . 14 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → 𝐶𝑃)
154 eqidd 2737 . . . . . . . . . . . . . . . 16 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → 𝐶 = 𝐶)
155 simpr 485 . . . . . . . . . . . . . . . 16 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → 𝑦 = 𝑥)
156 eqidd 2737 . . . . . . . . . . . . . . . 16 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → 𝑎 = 𝑎)
157154, 155, 156s3eqd 14753 . . . . . . . . . . . . . . 15 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → ⟨“𝐶𝑦𝑎”⟩ = ⟨“𝐶𝑥𝑎”⟩)
15831adantr 481 . . . . . . . . . . . . . . . 16 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → 𝑥𝑃)
15930adantr 481 . . . . . . . . . . . . . . . . 17 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → 𝑧𝑃)
160106adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑞𝑦)
1611, 2, 3, 27, 28, 75, 28, 79, 120tgcgrcomlr 27422 . . . . . . . . . . . . . . . . . . . . . 22 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → (𝑞 𝑦) = ((((pInvG‘𝐺)‘𝑧)‘𝑞) 𝑦))
1621, 2, 3, 4, 5, 27, 30, 73, 75mircgr 27599 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → (𝑧 (((pInvG‘𝐺)‘𝑧)‘𝑞)) = (𝑧 𝑞))
163162eqcomd 2742 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → (𝑧 𝑞) = (𝑧 (((pInvG‘𝐺)‘𝑧)‘𝑞)))
1641, 2, 3, 27, 30, 75, 30, 79, 163tgcgrcomlr 27422 . . . . . . . . . . . . . . . . . . . . . 22 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → (𝑞 𝑧) = ((((pInvG‘𝐺)‘𝑧)‘𝑞) 𝑧))
165 eqidd 2737 . . . . . . . . . . . . . . . . . . . . . 22 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → (𝑦 𝑧) = (𝑦 𝑧))
1661, 2, 3, 27, 75, 28, 80, 79, 28, 81, 30, 30, 160, 89, 90, 161, 121, 164, 165axtg5seg 27407 . . . . . . . . . . . . . . . . . . . . 21 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → (𝐶 𝑧) = (𝑑 𝑧))
1671, 2, 3, 27, 80, 30, 81, 30, 166tgcgrcomlr 27422 . . . . . . . . . . . . . . . . . . . 20 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → (𝑧 𝐶) = (𝑧 𝑑))
168123oveq2d 7373 . . . . . . . . . . . . . . . . . . . 20 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → (𝑧 𝑑) = (𝑧 (((pInvG‘𝐺)‘𝑥)‘𝐶)))
169167, 168eqtrd 2776 . . . . . . . . . . . . . . . . . . 19 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → (𝑧 𝐶) = (𝑧 (((pInvG‘𝐺)‘𝑥)‘𝐶)))
1701, 2, 3, 4, 5, 27, 30, 31, 80israg 27639 . . . . . . . . . . . . . . . . . . 19 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → (⟨“𝑧𝑥𝐶”⟩ ∈ (∟G‘𝐺) ↔ (𝑧 𝐶) = (𝑧 (((pInvG‘𝐺)‘𝑥)‘𝐶))))
171169, 170mpbird 256 . . . . . . . . . . . . . . . . . 18 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → ⟨“𝑧𝑥𝐶”⟩ ∈ (∟G‘𝐺))
172171adantr 481 . . . . . . . . . . . . . . . . 17 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → ⟨“𝑧𝑥𝐶”⟩ ∈ (∟G‘𝐺))
17372adantr 481 . . . . . . . . . . . . . . . . . 18 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → 𝑧𝑦)
174173, 155neeqtrd 3013 . . . . . . . . . . . . . . . . 17 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → 𝑧𝑥)
175132adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → (𝑎 𝐶) = (𝑎 𝑦))
176133adantr 481 . . . . . . . . . . . . . . . . . . . . . 22 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → 𝑎𝐶)
1771, 2, 3, 149, 150, 153, 150, 151, 175, 176tgcgrneq 27425 . . . . . . . . . . . . . . . . . . . . 21 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → 𝑎𝑦)
178177necomd 2999 . . . . . . . . . . . . . . . . . . . 20 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → 𝑦𝑎)
179136adantr 481 . . . . . . . . . . . . . . . . . . . 20 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → 𝑧 ∈ (𝑎𝐿𝑦))
1801, 3, 4, 149, 151, 150, 159, 178, 179lncom 27564 . . . . . . . . . . . . . . . . . . 19 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → 𝑧 ∈ (𝑦𝐿𝑎))
181155oveq1d 7372 . . . . . . . . . . . . . . . . . . 19 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → (𝑦𝐿𝑎) = (𝑥𝐿𝑎))
182180, 181eleqtrd 2840 . . . . . . . . . . . . . . . . . 18 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → 𝑧 ∈ (𝑥𝐿𝑎))
183182orcd 871 . . . . . . . . . . . . . . . . 17 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → (𝑧 ∈ (𝑥𝐿𝑎) ∨ 𝑥 = 𝑎))
1841, 2, 3, 4, 5, 149, 159, 158, 153, 150, 172, 174, 183ragcol 27641 . . . . . . . . . . . . . . . 16 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → ⟨“𝑎𝑥𝐶”⟩ ∈ (∟G‘𝐺))
1851, 2, 3, 4, 5, 149, 150, 158, 153, 184ragcom 27640 . . . . . . . . . . . . . . 15 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → ⟨“𝐶𝑥𝑎”⟩ ∈ (∟G‘𝐺))
186157, 185eqeltrd 2838 . . . . . . . . . . . . . 14 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → ⟨“𝐶𝑦𝑎”⟩ ∈ (∟G‘𝐺))
18764adantr 481 . . . . . . . . . . . . . 14 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → 𝐶𝑦)
1881, 2, 3, 27, 80, 34, 28, 84tgbtwncom 27430 . . . . . . . . . . . . . . . 16 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑝 ∈ (𝑦𝐼𝐶))
1891, 4, 3, 27, 28, 34, 80, 188btwncolg3 27499 . . . . . . . . . . . . . . 15 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → (𝐶 ∈ (𝑦𝐿𝑝) ∨ 𝑦 = 𝑝))
190189adantr 481 . . . . . . . . . . . . . 14 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → (𝐶 ∈ (𝑦𝐿𝑝) ∨ 𝑦 = 𝑝))
1911, 2, 3, 4, 5, 149, 153, 151, 150, 152, 186, 187, 190ragcol 27641 . . . . . . . . . . . . 13 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → ⟨“𝑝𝑦𝑎”⟩ ∈ (∟G‘𝐺))
1921, 2, 3, 4, 5, 149, 152, 151, 150, 191ragcom 27640 . . . . . . . . . . . 12 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → ⟨“𝑎𝑦𝑝”⟩ ∈ (∟G‘𝐺))
19396ad2antrr 724 . . . . . . . . . . . 12 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → ⟨“𝑎𝑝𝑦”⟩ ∈ (∟G‘𝐺))
1941, 2, 3, 4, 5, 149, 150, 151, 152, 192, 193ragflat 27646 . . . . . . . . . . 11 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → 𝑦 = 𝑝)
19570adantr 481 . . . . . . . . . . . 12 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → 𝑦𝑝)
196195neneqd 2948 . . . . . . . . . . 11 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → ¬ 𝑦 = 𝑝)
197194, 196pm2.65da 815 . . . . . . . . . 10 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → ¬ 𝑦 = 𝑥)
198197neqned 2950 . . . . . . . . 9 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑦𝑥)
199123oveq2d 7373 . . . . . . . . . . . 12 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → (𝑦 𝑑) = (𝑦 (((pInvG‘𝐺)‘𝑥)‘𝐶)))
200121, 199eqtrd 2776 . . . . . . . . . . 11 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → (𝑦 𝐶) = (𝑦 (((pInvG‘𝐺)‘𝑥)‘𝐶)))
2011, 2, 3, 4, 5, 27, 28, 31, 80israg 27639 . . . . . . . . . . 11 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → (⟨“𝑦𝑥𝐶”⟩ ∈ (∟G‘𝐺) ↔ (𝑦 𝐶) = (𝑦 (((pInvG‘𝐺)‘𝑥)‘𝐶))))
202200, 201mpbird 256 . . . . . . . . . 10 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → ⟨“𝑦𝑥𝐶”⟩ ∈ (∟G‘𝐺))
2031, 2, 3, 4, 5, 27, 28, 31, 80, 202ragcom 27640 . . . . . . . . 9 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → ⟨“𝐶𝑥𝑦”⟩ ∈ (∟G‘𝐺))
2041, 2, 3, 4, 27, 145, 129, 147, 148, 57, 144, 198, 203ragperp 27659 . . . . . . . 8 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → (𝐶𝐿𝑥)(⟂G‘𝐺)𝐴)
20526, 141, 204reximssdv 3169 . . . . . . 7 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → ∃𝑥𝐴 (𝐶𝐿𝑥)(⟂G‘𝐺)𝐴)
2061, 2, 3, 11, 78, 22, 22, 17axtgsegcon 27406 . . . . . . 7 ((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) → ∃𝑑𝑃 (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶)))
207205, 206r19.29a 3159 . . . . . 6 ((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) → ∃𝑥𝐴 (𝐶𝐿𝑥)(⟂G‘𝐺)𝐴)
2081, 2, 3, 10, 32, 21, 21, 44axtgsegcon 27406 . . . . . 6 ((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) → ∃𝑞𝑃 (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎)))
209207, 208r19.29a 3159 . . . . 5 ((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) → ∃𝑥𝐴 (𝐶𝐿𝑥)(⟂G‘𝐺)𝐴)
210 simplr 767 . . . . . 6 ((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) → 𝑝𝑃)
2111, 2, 3, 9, 43, 20, 20, 210axtgsegcon 27406 . . . . 5 ((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) → ∃𝑧𝑃 (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝)))
212209, 211r19.29a 3159 . . . 4 ((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) → ∃𝑥𝐴 (𝐶𝐿𝑥)(⟂G‘𝐺)𝐴)
213 simplr 767 . . . . 5 ((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) → 𝑦𝑃)
214 simprr 771 . . . . 5 ((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) → (𝑎 𝑦) = (𝑎 𝐶))
2151, 2, 3, 4, 5, 8, 66, 213, 16, 42, 214midexlem 27634 . . . 4 ((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) → ∃𝑝𝑃 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦))
216212, 215r19.29a 3159 . . 3 ((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) → ∃𝑥𝐴 (𝐶𝐿𝑥)(⟂G‘𝐺)𝐴)
2171, 2, 3, 7, 46, 41, 41, 15axtgsegcon 27406 . . 3 ((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) → ∃𝑦𝑃 (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶)))
218216, 217r19.29a 3159 . 2 ((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) → ∃𝑥𝐴 (𝐶𝐿𝑥)(⟂G‘𝐺)𝐴)
2191, 3, 4, 6, 127tgisline 27569 . 2 (𝜑 → ∃𝑎𝑃𝑏𝑃 (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏))
220218, 219r19.29vva 3207 1 (𝜑 → ∃𝑥𝐴 (𝐶𝐿𝑥)(⟂G‘𝐺)𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 396  wo 845   = wceq 1541  wcel 2106  wne 2943  wrex 3073   class class class wbr 5105  ran crn 5634  cfv 6496  (class class class)co 7357  ⟨“cs3 14731  Basecbs 17083  distcds 17142  TarskiGcstrkg 27369  Itvcitv 27375  LineGclng 27376  cgrGccgrg 27452  pInvGcmir 27594  ∟Gcrag 27635  ⟂Gcperpg 27637
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-rep 5242  ax-sep 5256  ax-nul 5263  ax-pow 5320  ax-pr 5384  ax-un 7672  ax-cnex 11107  ax-resscn 11108  ax-1cn 11109  ax-icn 11110  ax-addcl 11111  ax-addrcl 11112  ax-mulcl 11113  ax-mulrcl 11114  ax-mulcom 11115  ax-addass 11116  ax-mulass 11117  ax-distr 11118  ax-i2m1 11119  ax-1ne0 11120  ax-1rid 11121  ax-rnegex 11122  ax-rrecex 11123  ax-cnre 11124  ax-pre-lttri 11125  ax-pre-lttrn 11126  ax-pre-ltadd 11127  ax-pre-mulgt0 11128
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-nel 3050  df-ral 3065  df-rex 3074  df-rmo 3353  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-tp 4591  df-op 4593  df-uni 4866  df-int 4908  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-riota 7313  df-ov 7360  df-oprab 7361  df-mpo 7362  df-om 7803  df-1st 7921  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-1o 8412  df-oadd 8416  df-er 8648  df-map 8767  df-pm 8768  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-dju 9837  df-card 9875  df-pnf 11191  df-mnf 11192  df-xr 11193  df-ltxr 11194  df-le 11195  df-sub 11387  df-neg 11388  df-nn 12154  df-2 12216  df-3 12217  df-n0 12414  df-xnn0 12486  df-z 12500  df-uz 12764  df-fz 13425  df-fzo 13568  df-hash 14231  df-word 14403  df-concat 14459  df-s1 14484  df-s2 14737  df-s3 14738  df-trkgc 27390  df-trkgb 27391  df-trkgcb 27392  df-trkg 27395  df-cgrg 27453  df-leg 27525  df-mir 27595  df-rag 27636  df-perpg 27638
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator