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

Theorem footexALT 28739
Description: Alternative version of footex 28742 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 2734 . . . . . . . . 9 (pInvG‘𝐺) = (pInvG‘𝐺)
6 isperp.g . . . . . . . . . . . . . . 15 (𝜑𝐺 ∈ TarskiG)
76ad3antrrr 730 . . . . . . . . . . . . . 14 ((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) → 𝐺 ∈ TarskiG)
87ad2antrr 726 . . . . . . . . . . . . 13 ((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) → 𝐺 ∈ TarskiG)
98ad2antrr 726 . . . . . . . . . . . 12 ((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) → 𝐺 ∈ TarskiG)
109ad2antrr 726 . . . . . . . . . . 11 ((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) → 𝐺 ∈ TarskiG)
1110ad2antrr 726 . . . . . . . . . 10 ((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) → 𝐺 ∈ TarskiG)
1211ad2antrr 726 . . . . . . . . 9 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → 𝐺 ∈ TarskiG)
13 eqid 2734 . . . . . . . . 9 ((pInvG‘𝐺)‘𝑥) = ((pInvG‘𝐺)‘𝑥)
14 foot.x . . . . . . . . . . . . 13 (𝜑𝐶𝑃)
1514ad3antrrr 730 . . . . . . . . . . . 12 ((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) → 𝐶𝑃)
1615ad2antrr 726 . . . . . . . . . . 11 ((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) → 𝐶𝑃)
1716ad6antr 736 . . . . . . . . . 10 ((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) → 𝐶𝑃)
1817ad2antrr 726 . . . . . . . . 9 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → 𝐶𝑃)
19 simplr 768 . . . . . . . . 9 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → 𝑑𝑃)
20 simp-4r 783 . . . . . . . . . . . 12 ((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) → 𝑦𝑃)
2120ad2antrr 726 . . . . . . . . . . 11 ((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) → 𝑦𝑃)
2221ad2antrr 726 . . . . . . . . . 10 ((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) → 𝑦𝑃)
2322ad2antrr 726 . . . . . . . . 9 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → 𝑦𝑃)
24 simprr 772 . . . . . . . . . 10 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → (𝑦 𝑑) = (𝑦 𝐶))
2524eqcomd 2740 . . . . . . . . 9 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → (𝑦 𝐶) = (𝑦 𝑑))
261, 2, 3, 4, 5, 12, 13, 18, 19, 23, 25midexlem 28713 . . . . . . . 8 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → ∃𝑥𝑃 𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))
2712adantr 480 . . . . . . . . . 10 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝐺 ∈ TarskiG)
2823adantr 480 . . . . . . . . . 10 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑦𝑃)
29 simp-6r 787 . . . . . . . . . . 11 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → 𝑧𝑃)
3029adantr 480 . . . . . . . . . 10 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑧𝑃)
31 simprl 770 . . . . . . . . . 10 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑥𝑃)
32 simp-4r 783 . . . . . . . . . . . . 13 ((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) → 𝑝𝑃)
3332ad4antr 732 . . . . . . . . . . . 12 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → 𝑝𝑃)
3433adantr 480 . . . . . . . . . . 11 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑝𝑃)
35 simp-5r 785 . . . . . . . . . . . . . 14 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝)))
3635simprd 495 . . . . . . . . . . . . 13 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → (𝑦 𝑧) = (𝑦 𝑝))
3736eqcomd 2740 . . . . . . . . . . . 12 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → (𝑦 𝑝) = (𝑦 𝑧))
3837adantr 480 . . . . . . . . . . 11 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → (𝑦 𝑝) = (𝑦 𝑧))
39 simp-7r 789 . . . . . . . . . . . . . . 15 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦))
4039adantr 480 . . . . . . . . . . . . . 14 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦))
41 simpllr 775 . . . . . . . . . . . . . . . . . . . . . . 23 ((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) → 𝑎𝑃)
4241ad2antrr 726 . . . . . . . . . . . . . . . . . . . . . 22 ((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) → 𝑎𝑃)
4342ad2antrr 726 . . . . . . . . . . . . . . . . . . . . 21 ((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) → 𝑎𝑃)
4443ad2antrr 726 . . . . . . . . . . . . . . . . . . . 20 ((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) → 𝑎𝑃)
4544ad4antr 732 . . . . . . . . . . . . . . . . . . 19 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → 𝑎𝑃)
46 simplr 768 . . . . . . . . . . . . . . . . . . . 20 ((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) → 𝑏𝑃)
4746ad10antr 744 . . . . . . . . . . . . . . . . . . 19 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → 𝑏𝑃)
48 simp-11r 797 . . . . . . . . . . . . . . . . . . . 20 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏))
4948simprd 495 . . . . . . . . . . . . . . . . . . 19 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → 𝑎𝑏)
5049necomd 2985 . . . . . . . . . . . . . . . . . . . 20 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → 𝑏𝑎)
51 simp-9r 793 . . . . . . . . . . . . . . . . . . . . 21 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶)))
5251simpld 494 . . . . . . . . . . . . . . . . . . . 20 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → 𝑎 ∈ (𝑏𝐼𝑦))
531, 3, 4, 12, 47, 45, 23, 50, 52btwnlng3 28642 . . . . . . . . . . . . . . . . . . 19 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → 𝑦 ∈ (𝑏𝐿𝑎))
541, 3, 4, 12, 45, 47, 23, 49, 53lncom 28643 . . . . . . . . . . . . . . . . . 18 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → 𝑦 ∈ (𝑎𝐿𝑏))
5548simpld 494 . . . . . . . . . . . . . . . . . 18 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → 𝐴 = (𝑎𝐿𝑏))
5654, 55eleqtrrd 2837 . . . . . . . . . . . . . . . . 17 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → 𝑦𝐴)
5756adantr 480 . . . . . . . . . . . . . . . 16 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑦𝐴)
58 foot.y . . . . . . . . . . . . . . . . . . 19 (𝜑 → ¬ 𝐶𝐴)
5958ad3antrrr 730 . . . . . . . . . . . . . . . . . 18 ((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) → ¬ 𝐶𝐴)
6059ad10antr 744 . . . . . . . . . . . . . . . . 17 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → ¬ 𝐶𝐴)
6160adantr 480 . . . . . . . . . . . . . . . 16 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → ¬ 𝐶𝐴)
62 nelne2 3028 . . . . . . . . . . . . . . . 16 ((𝑦𝐴 ∧ ¬ 𝐶𝐴) → 𝑦𝐶)
6357, 61, 62syl2anc 584 . . . . . . . . . . . . . . 15 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑦𝐶)
6463necomd 2985 . . . . . . . . . . . . . 14 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝐶𝑦)
6540, 64eqnetrrd 2998 . . . . . . . . . . . . 13 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → (((pInvG‘𝐺)‘𝑝)‘𝑦) ≠ 𝑦)
66 eqid 2734 . . . . . . . . . . . . . . 15 ((pInvG‘𝐺)‘𝑝) = ((pInvG‘𝐺)‘𝑝)
671, 2, 3, 4, 5, 27, 34, 66, 28mirinv 28687 . . . . . . . . . . . . . 14 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → ((((pInvG‘𝐺)‘𝑝)‘𝑦) = 𝑦𝑝 = 𝑦))
6867necon3bid 2974 . . . . . . . . . . . . 13 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → ((((pInvG‘𝐺)‘𝑝)‘𝑦) ≠ 𝑦𝑝𝑦))
6965, 68mpbid 232 . . . . . . . . . . . 12 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑝𝑦)
7069necomd 2985 . . . . . . . . . . 11 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑦𝑝)
711, 2, 3, 27, 28, 34, 28, 30, 38, 70tgcgrneq 28504 . . . . . . . . . 10 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑦𝑧)
7271necomd 2985 . . . . . . . . . . 11 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑧𝑦)
73 eqid 2734 . . . . . . . . . . . 12 ((pInvG‘𝐺)‘𝑧) = ((pInvG‘𝐺)‘𝑧)
74 simp-4r 783 . . . . . . . . . . . . 13 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → 𝑞𝑃)
7574adantr 480 . . . . . . . . . . . 12 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑞𝑃)
76 simp-4r 783 . . . . . . . . . . . . . 14 ((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) → 𝑧𝑃)
77 simplr 768 . . . . . . . . . . . . . 14 ((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) → 𝑞𝑃)
781, 2, 3, 4, 5, 11, 76, 73, 77mircl 28682 . . . . . . . . . . . . 13 ((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) → (((pInvG‘𝐺)‘𝑧)‘𝑞) ∈ 𝑃)
7978ad3antrrr 730 . . . . . . . . . . . 12 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → (((pInvG‘𝐺)‘𝑧)‘𝑞) ∈ 𝑃)
8018adantr 480 . . . . . . . . . . . 12 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝐶𝑃)
81 simpllr 775 . . . . . . . . . . . 12 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑑𝑃)
821, 2, 3, 4, 5, 27, 34, 66, 28mirbtwn 28679 . . . . . . . . . . . . . . 15 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑝 ∈ ((((pInvG‘𝐺)‘𝑝)‘𝑦)𝐼𝑦))
8340oveq1d 7371 . . . . . . . . . . . . . . 15 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → (𝐶𝐼𝑦) = ((((pInvG‘𝐺)‘𝑝)‘𝑦)𝐼𝑦))
8482, 83eleqtrrd 2837 . . . . . . . . . . . . . 14 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑝 ∈ (𝐶𝐼𝑦))
85 simpllr 775 . . . . . . . . . . . . . . . 16 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎)))
8685simpld 494 . . . . . . . . . . . . . . 15 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → 𝑦 ∈ (𝑝𝐼𝑞))
8786adantr 480 . . . . . . . . . . . . . 14 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑦 ∈ (𝑝𝐼𝑞))
881, 2, 3, 27, 80, 34, 28, 75, 69, 84, 87tgbtwnouttr2 28516 . . . . . . . . . . . . 13 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑦 ∈ (𝐶𝐼𝑞))
891, 2, 3, 27, 80, 28, 75, 88tgbtwncom 28509 . . . . . . . . . . . 12 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑦 ∈ (𝑞𝐼𝐶))
90 simplrl 776 . . . . . . . . . . . 12 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑))
91 eqid 2734 . . . . . . . . . . . . . . . 16 (cgrG‘𝐺) = (cgrG‘𝐺)
9251simprd 495 . . . . . . . . . . . . . . . . . 18 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → (𝑎 𝑦) = (𝑎 𝐶))
9339oveq2d 7372 . . . . . . . . . . . . . . . . . 18 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → (𝑎 𝐶) = (𝑎 (((pInvG‘𝐺)‘𝑝)‘𝑦)))
9492, 93eqtrd 2769 . . . . . . . . . . . . . . . . 17 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → (𝑎 𝑦) = (𝑎 (((pInvG‘𝐺)‘𝑝)‘𝑦)))
951, 2, 3, 4, 5, 12, 45, 33, 23israg 28718 . . . . . . . . . . . . . . . . 17 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → (⟨“𝑎𝑝𝑦”⟩ ∈ (∟G‘𝐺) ↔ (𝑎 𝑦) = (𝑎 (((pInvG‘𝐺)‘𝑝)‘𝑦))))
9694, 95mpbird 257 . . . . . . . . . . . . . . . 16 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → ⟨“𝑎𝑝𝑦”⟩ ∈ (∟G‘𝐺))
9785simprd 495 . . . . . . . . . . . . . . . . . . . . . 22 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → (𝑦 𝑞) = (𝑦 𝑎))
981, 2, 3, 12, 45, 23, 45, 18, 92tgcgrcomlr 28501 . . . . . . . . . . . . . . . . . . . . . 22 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → (𝑦 𝑎) = (𝐶 𝑎))
9997, 98eqtr2d 2770 . . . . . . . . . . . . . . . . . . . . 21 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → (𝐶 𝑎) = (𝑦 𝑞))
1001, 3, 4, 12, 45, 47, 49tglinerflx1 28654 . . . . . . . . . . . . . . . . . . . . . . . 24 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → 𝑎 ∈ (𝑎𝐿𝑏))
101100, 55eleqtrrd 2837 . . . . . . . . . . . . . . . . . . . . . . 23 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → 𝑎𝐴)
102 nelne2 3028 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝑎𝐴 ∧ ¬ 𝐶𝐴) → 𝑎𝐶)
103101, 60, 102syl2anc 584 . . . . . . . . . . . . . . . . . . . . . 22 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → 𝑎𝐶)
104103necomd 2985 . . . . . . . . . . . . . . . . . . . . 21 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → 𝐶𝑎)
1051, 2, 3, 12, 18, 45, 23, 74, 99, 104tgcgrneq 28504 . . . . . . . . . . . . . . . . . . . 20 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → 𝑦𝑞)
106105necomd 2985 . . . . . . . . . . . . . . . . . . 19 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → 𝑞𝑦)
1071, 2, 3, 12, 33, 23, 74, 86tgbtwncom 28509 . . . . . . . . . . . . . . . . . . 19 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → 𝑦 ∈ (𝑞𝐼𝑝))
10835simpld 494 . . . . . . . . . . . . . . . . . . 19 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → 𝑦 ∈ (𝑎𝐼𝑧))
1091, 2, 3, 12, 23, 74, 23, 45, 97tgcgrcomlr 28501 . . . . . . . . . . . . . . . . . . 19 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → (𝑞 𝑦) = (𝑎 𝑦))
1101, 2, 3, 12, 74, 45axtgcgrrflx 28483 . . . . . . . . . . . . . . . . . . 19 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → (𝑞 𝑎) = (𝑎 𝑞))
11197eqcomd 2740 . . . . . . . . . . . . . . . . . . 19 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → (𝑦 𝑎) = (𝑦 𝑞))
1121, 2, 3, 12, 74, 23, 33, 45, 23, 29, 45, 74, 106, 107, 108, 109, 37, 110, 111axtg5seg 28486 . . . . . . . . . . . . . . . . . 18 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → (𝑝 𝑎) = (𝑧 𝑞))
1131, 2, 3, 12, 33, 45, 29, 74, 112tgcgrcomlr 28501 . . . . . . . . . . . . . . . . 17 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → (𝑎 𝑝) = (𝑞 𝑧))
1141, 2, 3, 12, 23, 33, 23, 29, 37tgcgrcomlr 28501 . . . . . . . . . . . . . . . . 17 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → (𝑝 𝑦) = (𝑧 𝑦))
1151, 2, 91, 12, 45, 33, 23, 74, 29, 23, 113, 114, 111trgcgr 28537 . . . . . . . . . . . . . . . 16 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → ⟨“𝑎𝑝𝑦”⟩(cgrG‘𝐺)⟨“𝑞𝑧𝑦”⟩)
1161, 2, 3, 4, 5, 12, 45, 33, 23, 91, 74, 29, 23, 96, 115ragcgr 28728 . . . . . . . . . . . . . . 15 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → ⟨“𝑞𝑧𝑦”⟩ ∈ (∟G‘𝐺))
1171, 2, 3, 4, 5, 12, 74, 29, 23, 116ragcom 28719 . . . . . . . . . . . . . 14 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → ⟨“𝑦𝑧𝑞”⟩ ∈ (∟G‘𝐺))
1181, 2, 3, 4, 5, 12, 23, 29, 74israg 28718 . . . . . . . . . . . . . 14 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → (⟨“𝑦𝑧𝑞”⟩ ∈ (∟G‘𝐺) ↔ (𝑦 𝑞) = (𝑦 (((pInvG‘𝐺)‘𝑧)‘𝑞))))
119117, 118mpbid 232 . . . . . . . . . . . . 13 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → (𝑦 𝑞) = (𝑦 (((pInvG‘𝐺)‘𝑧)‘𝑞)))
120119adantr 480 . . . . . . . . . . . 12 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → (𝑦 𝑞) = (𝑦 (((pInvG‘𝐺)‘𝑧)‘𝑞)))
12125adantr 480 . . . . . . . . . . . 12 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → (𝑦 𝐶) = (𝑦 𝑑))
122 eqidd 2735 . . . . . . . . . . . 12 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → (((pInvG‘𝐺)‘𝑧)‘𝑞) = (((pInvG‘𝐺)‘𝑧)‘𝑞))
123 simprr 772 . . . . . . . . . . . 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 28712 . . . . . . . . . . 11 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑦 ∈ (𝑧𝐼𝑥))
1251, 3, 4, 27, 30, 28, 31, 72, 124btwnlng3 28642 . . . . . . . . . 10 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑥 ∈ (𝑧𝐿𝑦))
1261, 3, 4, 27, 28, 30, 31, 71, 125lncom 28643 . . . . . . . . 9 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑥 ∈ (𝑦𝐿𝑧))
127 isperp.a . . . . . . . . . . . 12 (𝜑𝐴 ∈ ran 𝐿)
128127ad5antr 734 . . . . . . . . . . 11 ((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) → 𝐴 ∈ ran 𝐿)
129128ad9antr 742 . . . . . . . . . 10 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝐴 ∈ ran 𝐿)
13045adantr 480 . . . . . . . . . . . 12 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑎𝑃)
13192adantr 480 . . . . . . . . . . . . . 14 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → (𝑎 𝑦) = (𝑎 𝐶))
132131eqcomd 2740 . . . . . . . . . . . . 13 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → (𝑎 𝐶) = (𝑎 𝑦))
133103adantr 480 . . . . . . . . . . . . 13 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑎𝐶)
1341, 2, 3, 27, 130, 80, 130, 28, 132, 133tgcgrneq 28504 . . . . . . . . . . . 12 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑎𝑦)
135108adantr 480 . . . . . . . . . . . 12 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑦 ∈ (𝑎𝐼𝑧))
1361, 3, 4, 27, 130, 28, 30, 134, 135btwnlng3 28642 . . . . . . . . . . 11 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑧 ∈ (𝑎𝐿𝑦))
137101adantr 480 . . . . . . . . . . . 12 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑎𝐴)
1381, 3, 4, 27, 130, 28, 134, 134, 129, 137, 57tglinethru 28657 . . . . . . . . . . 11 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝐴 = (𝑎𝐿𝑦))
139136, 138eleqtrrd 2837 . . . . . . . . . 10 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑧𝐴)
1401, 3, 4, 27, 28, 30, 71, 71, 129, 57, 139tglinethru 28657 . . . . . . . . 9 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝐴 = (𝑦𝐿𝑧))
141126, 140eleqtrrd 2837 . . . . . . . 8 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑥𝐴)
142 nelne2 3028 . . . . . . . . . . . 12 ((𝑥𝐴 ∧ ¬ 𝐶𝐴) → 𝑥𝐶)
143141, 61, 142syl2anc 584 . . . . . . . . . . 11 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑥𝐶)
144143necomd 2985 . . . . . . . . . 10 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝐶𝑥)
1451, 3, 4, 27, 80, 31, 144tgelrnln 28651 . . . . . . . . 9 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → (𝐶𝐿𝑥) ∈ ran 𝐿)
1461, 3, 4, 27, 80, 31, 144tglinerflx2 28655 . . . . . . . . . 10 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑥 ∈ (𝐶𝐿𝑥))
147146, 141elind 4150 . . . . . . . . 9 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑥 ∈ ((𝐶𝐿𝑥) ∩ 𝐴))
1481, 3, 4, 27, 80, 31, 144tglinerflx1 28654 . . . . . . . . 9 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝐶 ∈ (𝐶𝐿𝑥))
14927adantr 480 . . . . . . . . . . . 12 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → 𝐺 ∈ TarskiG)
150130adantr 480 . . . . . . . . . . . 12 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → 𝑎𝑃)
15128adantr 480 . . . . . . . . . . . 12 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → 𝑦𝑃)
15234adantr 480 . . . . . . . . . . . 12 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → 𝑝𝑃)
15380adantr 480 . . . . . . . . . . . . . 14 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → 𝐶𝑃)
154 eqidd 2735 . . . . . . . . . . . . . . . 16 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → 𝐶 = 𝐶)
155 simpr 484 . . . . . . . . . . . . . . . 16 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → 𝑦 = 𝑥)
156 eqidd 2735 . . . . . . . . . . . . . . . 16 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → 𝑎 = 𝑎)
157154, 155, 156s3eqd 14785 . . . . . . . . . . . . . . 15 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → ⟨“𝐶𝑦𝑎”⟩ = ⟨“𝐶𝑥𝑎”⟩)
15831adantr 480 . . . . . . . . . . . . . . . 16 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → 𝑥𝑃)
15930adantr 480 . . . . . . . . . . . . . . . . 17 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → 𝑧𝑃)
160106adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑞𝑦)
1611, 2, 3, 27, 28, 75, 28, 79, 120tgcgrcomlr 28501 . . . . . . . . . . . . . . . . . . . . . 22 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → (𝑞 𝑦) = ((((pInvG‘𝐺)‘𝑧)‘𝑞) 𝑦))
1621, 2, 3, 4, 5, 27, 30, 73, 75mircgr 28678 . . . . . . . . . . . . . . . . . . . . . . . 24 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → (𝑧 (((pInvG‘𝐺)‘𝑧)‘𝑞)) = (𝑧 𝑞))
163162eqcomd 2740 . . . . . . . . . . . . . . . . . . . . . . 23 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → (𝑧 𝑞) = (𝑧 (((pInvG‘𝐺)‘𝑧)‘𝑞)))
1641, 2, 3, 27, 30, 75, 30, 79, 163tgcgrcomlr 28501 . . . . . . . . . . . . . . . . . . . . . 22 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → (𝑞 𝑧) = ((((pInvG‘𝐺)‘𝑧)‘𝑞) 𝑧))
165 eqidd 2735 . . . . . . . . . . . . . . . . . . . . . 22 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → (𝑦 𝑧) = (𝑦 𝑧))
1661, 2, 3, 27, 75, 28, 80, 79, 28, 81, 30, 30, 160, 89, 90, 161, 121, 164, 165axtg5seg 28486 . . . . . . . . . . . . . . . . . . . . 21 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → (𝐶 𝑧) = (𝑑 𝑧))
1671, 2, 3, 27, 80, 30, 81, 30, 166tgcgrcomlr 28501 . . . . . . . . . . . . . . . . . . . 20 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → (𝑧 𝐶) = (𝑧 𝑑))
168123oveq2d 7372 . . . . . . . . . . . . . . . . . . . 20 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → (𝑧 𝑑) = (𝑧 (((pInvG‘𝐺)‘𝑥)‘𝐶)))
169167, 168eqtrd 2769 . . . . . . . . . . . . . . . . . . 19 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → (𝑧 𝐶) = (𝑧 (((pInvG‘𝐺)‘𝑥)‘𝐶)))
1701, 2, 3, 4, 5, 27, 30, 31, 80israg 28718 . . . . . . . . . . . . . . . . . . 19 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → (⟨“𝑧𝑥𝐶”⟩ ∈ (∟G‘𝐺) ↔ (𝑧 𝐶) = (𝑧 (((pInvG‘𝐺)‘𝑥)‘𝐶))))
171169, 170mpbird 257 . . . . . . . . . . . . . . . . . 18 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → ⟨“𝑧𝑥𝐶”⟩ ∈ (∟G‘𝐺))
172171adantr 480 . . . . . . . . . . . . . . . . 17 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → ⟨“𝑧𝑥𝐶”⟩ ∈ (∟G‘𝐺))
17372adantr 480 . . . . . . . . . . . . . . . . . 18 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → 𝑧𝑦)
174173, 155neeqtrd 2999 . . . . . . . . . . . . . . . . 17 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → 𝑧𝑥)
175132adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → (𝑎 𝐶) = (𝑎 𝑦))
176133adantr 480 . . . . . . . . . . . . . . . . . . . . . 22 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → 𝑎𝐶)
1771, 2, 3, 149, 150, 153, 150, 151, 175, 176tgcgrneq 28504 . . . . . . . . . . . . . . . . . . . . 21 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → 𝑎𝑦)
178177necomd 2985 . . . . . . . . . . . . . . . . . . . 20 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → 𝑦𝑎)
179136adantr 480 . . . . . . . . . . . . . . . . . . . 20 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → 𝑧 ∈ (𝑎𝐿𝑦))
1801, 3, 4, 149, 151, 150, 159, 178, 179lncom 28643 . . . . . . . . . . . . . . . . . . 19 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → 𝑧 ∈ (𝑦𝐿𝑎))
181155oveq1d 7371 . . . . . . . . . . . . . . . . . . 19 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → (𝑦𝐿𝑎) = (𝑥𝐿𝑎))
182180, 181eleqtrd 2836 . . . . . . . . . . . . . . . . . 18 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → 𝑧 ∈ (𝑥𝐿𝑎))
183182orcd 873 . . . . . . . . . . . . . . . . 17 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → (𝑧 ∈ (𝑥𝐿𝑎) ∨ 𝑥 = 𝑎))
1841, 2, 3, 4, 5, 149, 159, 158, 153, 150, 172, 174, 183ragcol 28720 . . . . . . . . . . . . . . . 16 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → ⟨“𝑎𝑥𝐶”⟩ ∈ (∟G‘𝐺))
1851, 2, 3, 4, 5, 149, 150, 158, 153, 184ragcom 28719 . . . . . . . . . . . . . . 15 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → ⟨“𝐶𝑥𝑎”⟩ ∈ (∟G‘𝐺))
186157, 185eqeltrd 2834 . . . . . . . . . . . . . 14 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → ⟨“𝐶𝑦𝑎”⟩ ∈ (∟G‘𝐺))
18764adantr 480 . . . . . . . . . . . . . 14 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → 𝐶𝑦)
1881, 2, 3, 27, 80, 34, 28, 84tgbtwncom 28509 . . . . . . . . . . . . . . . 16 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑝 ∈ (𝑦𝐼𝐶))
1891, 4, 3, 27, 28, 34, 80, 188btwncolg3 28578 . . . . . . . . . . . . . . 15 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → (𝐶 ∈ (𝑦𝐿𝑝) ∨ 𝑦 = 𝑝))
190189adantr 480 . . . . . . . . . . . . . 14 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → (𝐶 ∈ (𝑦𝐿𝑝) ∨ 𝑦 = 𝑝))
1911, 2, 3, 4, 5, 149, 153, 151, 150, 152, 186, 187, 190ragcol 28720 . . . . . . . . . . . . 13 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → ⟨“𝑝𝑦𝑎”⟩ ∈ (∟G‘𝐺))
1921, 2, 3, 4, 5, 149, 152, 151, 150, 191ragcom 28719 . . . . . . . . . . . 12 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → ⟨“𝑎𝑦𝑝”⟩ ∈ (∟G‘𝐺))
19396ad2antrr 726 . . . . . . . . . . . 12 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → ⟨“𝑎𝑝𝑦”⟩ ∈ (∟G‘𝐺))
1941, 2, 3, 4, 5, 149, 150, 151, 152, 192, 193ragflat 28725 . . . . . . . . . . 11 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → 𝑦 = 𝑝)
19570adantr 480 . . . . . . . . . . . 12 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → 𝑦𝑝)
196195neneqd 2935 . . . . . . . . . . 11 ((((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) ∧ 𝑦 = 𝑥) → ¬ 𝑦 = 𝑝)
197194, 196pm2.65da 816 . . . . . . . . . 10 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → ¬ 𝑦 = 𝑥)
198197neqned 2937 . . . . . . . . 9 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → 𝑦𝑥)
199123oveq2d 7372 . . . . . . . . . . . 12 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → (𝑦 𝑑) = (𝑦 (((pInvG‘𝐺)‘𝑥)‘𝐶)))
200121, 199eqtrd 2769 . . . . . . . . . . 11 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → (𝑦 𝐶) = (𝑦 (((pInvG‘𝐺)‘𝑥)‘𝐶)))
2011, 2, 3, 4, 5, 27, 28, 31, 80israg 28718 . . . . . . . . . . 11 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → (⟨“𝑦𝑥𝐶”⟩ ∈ (∟G‘𝐺) ↔ (𝑦 𝐶) = (𝑦 (((pInvG‘𝐺)‘𝑥)‘𝐶))))
202200, 201mpbird 257 . . . . . . . . . 10 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → ⟨“𝑦𝑥𝐶”⟩ ∈ (∟G‘𝐺))
2031, 2, 3, 4, 5, 27, 28, 31, 80, 202ragcom 28719 . . . . . . . . 9 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → ⟨“𝐶𝑥𝑦”⟩ ∈ (∟G‘𝐺))
2041, 2, 3, 4, 27, 145, 129, 147, 148, 57, 144, 198, 203ragperp 28738 . . . . . . . 8 (((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) ∧ (𝑥𝑃𝑑 = (((pInvG‘𝐺)‘𝑥)‘𝐶))) → (𝐶𝐿𝑥)(⟂G‘𝐺)𝐴)
20526, 141, 204reximssdv 3152 . . . . . . 7 ((((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) ∧ 𝑑𝑃) ∧ (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶))) → ∃𝑥𝐴 (𝐶𝐿𝑥)(⟂G‘𝐺)𝐴)
2061, 2, 3, 11, 78, 22, 22, 17axtgsegcon 28485 . . . . . . 7 ((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) → ∃𝑑𝑃 (𝑦 ∈ ((((pInvG‘𝐺)‘𝑧)‘𝑞)𝐼𝑑) ∧ (𝑦 𝑑) = (𝑦 𝐶)))
207205, 206r19.29a 3142 . . . . . 6 ((((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) ∧ 𝑞𝑃) ∧ (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎))) → ∃𝑥𝐴 (𝐶𝐿𝑥)(⟂G‘𝐺)𝐴)
2081, 2, 3, 10, 32, 21, 21, 44axtgsegcon 28485 . . . . . 6 ((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) → ∃𝑞𝑃 (𝑦 ∈ (𝑝𝐼𝑞) ∧ (𝑦 𝑞) = (𝑦 𝑎)))
209207, 208r19.29a 3142 . . . . 5 ((((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) ∧ 𝑧𝑃) ∧ (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝))) → ∃𝑥𝐴 (𝐶𝐿𝑥)(⟂G‘𝐺)𝐴)
210 simplr 768 . . . . . 6 ((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) → 𝑝𝑃)
2111, 2, 3, 9, 43, 20, 20, 210axtgsegcon 28485 . . . . 5 ((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) → ∃𝑧𝑃 (𝑦 ∈ (𝑎𝐼𝑧) ∧ (𝑦 𝑧) = (𝑦 𝑝)))
212209, 211r19.29a 3142 . . . 4 ((((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) ∧ 𝑝𝑃) ∧ 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦)) → ∃𝑥𝐴 (𝐶𝐿𝑥)(⟂G‘𝐺)𝐴)
213 simplr 768 . . . . 5 ((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) → 𝑦𝑃)
214 simprr 772 . . . . 5 ((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) → (𝑎 𝑦) = (𝑎 𝐶))
2151, 2, 3, 4, 5, 8, 66, 213, 16, 42, 214midexlem 28713 . . . 4 ((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) → ∃𝑝𝑃 𝐶 = (((pInvG‘𝐺)‘𝑝)‘𝑦))
216212, 215r19.29a 3142 . . 3 ((((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) ∧ 𝑦𝑃) ∧ (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶))) → ∃𝑥𝐴 (𝐶𝐿𝑥)(⟂G‘𝐺)𝐴)
2171, 2, 3, 7, 46, 41, 41, 15axtgsegcon 28485 . . 3 ((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) → ∃𝑦𝑃 (𝑎 ∈ (𝑏𝐼𝑦) ∧ (𝑎 𝑦) = (𝑎 𝐶)))
218216, 217r19.29a 3142 . 2 ((((𝜑𝑎𝑃) ∧ 𝑏𝑃) ∧ (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏)) → ∃𝑥𝐴 (𝐶𝐿𝑥)(⟂G‘𝐺)𝐴)
2191, 3, 4, 6, 127tgisline 28648 . 2 (𝜑 → ∃𝑎𝑃𝑏𝑃 (𝐴 = (𝑎𝐿𝑏) ∧ 𝑎𝑏))
220218, 219r19.29vva 3194 1 (𝜑 → ∃𝑥𝐴 (𝐶𝐿𝑥)(⟂G‘𝐺)𝐴)
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wa 395  wo 847   = wceq 1541  wcel 2113  wne 2930  wrex 3058   class class class wbr 5096  ran crn 5623  cfv 6490  (class class class)co 7356  ⟨“cs3 14763  Basecbs 17134  distcds 17184  TarskiGcstrkg 28448  Itvcitv 28454  LineGclng 28455  cgrGccgrg 28531  pInvGcmir 28673  ∟Gcrag 28714  ⟂Gcperpg 28716
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-rep 5222  ax-sep 5239  ax-nul 5249  ax-pow 5308  ax-pr 5375  ax-un 7678  ax-cnex 11080  ax-resscn 11081  ax-1cn 11082  ax-icn 11083  ax-addcl 11084  ax-addrcl 11085  ax-mulcl 11086  ax-mulrcl 11087  ax-mulcom 11088  ax-addass 11089  ax-mulass 11090  ax-distr 11091  ax-i2m1 11092  ax-1ne0 11093  ax-1rid 11094  ax-rnegex 11095  ax-rrecex 11096  ax-cnre 11097  ax-pre-lttri 11098  ax-pre-lttrn 11099  ax-pre-ltadd 11100  ax-pre-mulgt0 11101
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-nel 3035  df-ral 3050  df-rex 3059  df-rmo 3348  df-reu 3349  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-tp 4583  df-op 4585  df-uni 4862  df-int 4901  df-iun 4946  df-br 5097  df-opab 5159  df-mpt 5178  df-tr 5204  df-id 5517  df-eprel 5522  df-po 5530  df-so 5531  df-fr 5575  df-we 5577  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-pred 6257  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-om 7807  df-1st 7931  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-1o 8395  df-oadd 8399  df-er 8633  df-map 8763  df-pm 8764  df-en 8882  df-dom 8883  df-sdom 8884  df-fin 8885  df-dju 9811  df-card 9849  df-pnf 11166  df-mnf 11167  df-xr 11168  df-ltxr 11169  df-le 11170  df-sub 11364  df-neg 11365  df-nn 12144  df-2 12206  df-3 12207  df-n0 12400  df-xnn0 12473  df-z 12487  df-uz 12750  df-fz 13422  df-fzo 13569  df-hash 14252  df-word 14435  df-concat 14492  df-s1 14518  df-s2 14769  df-s3 14770  df-trkgc 28469  df-trkgb 28470  df-trkgcb 28471  df-trkg 28474  df-cgrg 28532  df-leg 28604  df-mir 28674  df-rag 28715  df-perpg 28717
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator