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

Theorem sylow3lem1 18242
 Description: Lemma for sylow3 18248, first part. (Contributed by Mario Carneiro, 19-Jan-2015.)
Hypotheses
Ref Expression
sylow3.x 𝑋 = (Base‘𝐺)
sylow3.g (𝜑𝐺 ∈ Grp)
sylow3.xf (𝜑𝑋 ∈ Fin)
sylow3.p (𝜑𝑃 ∈ ℙ)
sylow3lem1.a + = (+g𝐺)
sylow3lem1.d = (-g𝐺)
sylow3lem1.m = (𝑥𝑋, 𝑦 ∈ (𝑃 pSyl 𝐺) ↦ ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)))
Assertion
Ref Expression
sylow3lem1 (𝜑 ∈ (𝐺 GrpAct (𝑃 pSyl 𝐺)))
Distinct variable groups:   𝑥,𝑦,𝑧,   𝑥, ,𝑦,𝑧   𝑥,𝑋,𝑦,𝑧   𝑥,𝐺,𝑦,𝑧   𝜑,𝑥,𝑦,𝑧   𝑥, + ,𝑦,𝑧   𝑥,𝑃,𝑦,𝑧

Proof of Theorem sylow3lem1
Dummy variables 𝑎 𝑏 𝑐 𝑢 𝑣 𝑤 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 sylow3.g . . 3 (𝜑𝐺 ∈ Grp)
2 ovex 6841 . . 3 (𝑃 pSyl 𝐺) ∈ V
31, 2jctir 562 . 2 (𝜑 → (𝐺 ∈ Grp ∧ (𝑃 pSyl 𝐺) ∈ V))
4 sylow3.xf . . . . . . . . . . 11 (𝜑𝑋 ∈ Fin)
5 sylow3.p . . . . . . . . . . 11 (𝜑𝑃 ∈ ℙ)
6 sylow3.x . . . . . . . . . . . 12 𝑋 = (Base‘𝐺)
76fislw 18240 . . . . . . . . . . 11 ((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) → (𝑦 ∈ (𝑃 pSyl 𝐺) ↔ (𝑦 ∈ (SubGrp‘𝐺) ∧ (♯‘𝑦) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))))
81, 4, 5, 7syl3anc 1477 . . . . . . . . . 10 (𝜑 → (𝑦 ∈ (𝑃 pSyl 𝐺) ↔ (𝑦 ∈ (SubGrp‘𝐺) ∧ (♯‘𝑦) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))))
98biimpa 502 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝑃 pSyl 𝐺)) → (𝑦 ∈ (SubGrp‘𝐺) ∧ (♯‘𝑦) = (𝑃↑(𝑃 pCnt (♯‘𝑋)))))
109adantrl 754 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑋𝑦 ∈ (𝑃 pSyl 𝐺))) → (𝑦 ∈ (SubGrp‘𝐺) ∧ (♯‘𝑦) = (𝑃↑(𝑃 pCnt (♯‘𝑋)))))
1110simpld 477 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦 ∈ (𝑃 pSyl 𝐺))) → 𝑦 ∈ (SubGrp‘𝐺))
12 simprl 811 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦 ∈ (𝑃 pSyl 𝐺))) → 𝑥𝑋)
13 sylow3lem1.a . . . . . . . 8 + = (+g𝐺)
14 sylow3lem1.d . . . . . . . 8 = (-g𝐺)
15 eqid 2760 . . . . . . . 8 (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)) = (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥))
166, 13, 14, 15conjsubg 17893 . . . . . . 7 ((𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑥𝑋) → ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)) ∈ (SubGrp‘𝐺))
1711, 12, 16syl2anc 696 . . . . . 6 ((𝜑 ∧ (𝑥𝑋𝑦 ∈ (𝑃 pSyl 𝐺))) → ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)) ∈ (SubGrp‘𝐺))
186, 13, 14, 15conjsubgen 17894 . . . . . . . . 9 ((𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑥𝑋) → 𝑦 ≈ ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)))
1911, 12, 18syl2anc 696 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑋𝑦 ∈ (𝑃 pSyl 𝐺))) → 𝑦 ≈ ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)))
204adantr 472 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑦 ∈ (𝑃 pSyl 𝐺))) → 𝑋 ∈ Fin)
216subgss 17796 . . . . . . . . . . 11 (𝑦 ∈ (SubGrp‘𝐺) → 𝑦𝑋)
2211, 21syl 17 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑦 ∈ (𝑃 pSyl 𝐺))) → 𝑦𝑋)
23 ssfi 8345 . . . . . . . . . 10 ((𝑋 ∈ Fin ∧ 𝑦𝑋) → 𝑦 ∈ Fin)
2420, 22, 23syl2anc 696 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦 ∈ (𝑃 pSyl 𝐺))) → 𝑦 ∈ Fin)
256subgss 17796 . . . . . . . . . . 11 (ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)) ∈ (SubGrp‘𝐺) → ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)) ⊆ 𝑋)
2617, 25syl 17 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑦 ∈ (𝑃 pSyl 𝐺))) → ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)) ⊆ 𝑋)
27 ssfi 8345 . . . . . . . . . 10 ((𝑋 ∈ Fin ∧ ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)) ⊆ 𝑋) → ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)) ∈ Fin)
2820, 26, 27syl2anc 696 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦 ∈ (𝑃 pSyl 𝐺))) → ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)) ∈ Fin)
29 hashen 13329 . . . . . . . . 9 ((𝑦 ∈ Fin ∧ ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)) ∈ Fin) → ((♯‘𝑦) = (♯‘ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥))) ↔ 𝑦 ≈ ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥))))
3024, 28, 29syl2anc 696 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑋𝑦 ∈ (𝑃 pSyl 𝐺))) → ((♯‘𝑦) = (♯‘ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥))) ↔ 𝑦 ≈ ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥))))
3119, 30mpbird 247 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦 ∈ (𝑃 pSyl 𝐺))) → (♯‘𝑦) = (♯‘ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥))))
3210simprd 482 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦 ∈ (𝑃 pSyl 𝐺))) → (♯‘𝑦) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))
3331, 32eqtr3d 2796 . . . . . 6 ((𝜑 ∧ (𝑥𝑋𝑦 ∈ (𝑃 pSyl 𝐺))) → (♯‘ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥))) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))
346fislw 18240 . . . . . . . 8 ((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) → (ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)) ∈ (𝑃 pSyl 𝐺) ↔ (ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)) ∈ (SubGrp‘𝐺) ∧ (♯‘ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥))) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))))
351, 4, 5, 34syl3anc 1477 . . . . . . 7 (𝜑 → (ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)) ∈ (𝑃 pSyl 𝐺) ↔ (ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)) ∈ (SubGrp‘𝐺) ∧ (♯‘ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥))) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))))
3635adantr 472 . . . . . 6 ((𝜑 ∧ (𝑥𝑋𝑦 ∈ (𝑃 pSyl 𝐺))) → (ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)) ∈ (𝑃 pSyl 𝐺) ↔ (ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)) ∈ (SubGrp‘𝐺) ∧ (♯‘ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥))) = (𝑃↑(𝑃 pCnt (♯‘𝑋))))))
3717, 33, 36mpbir2and 995 . . . . 5 ((𝜑 ∧ (𝑥𝑋𝑦 ∈ (𝑃 pSyl 𝐺))) → ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)) ∈ (𝑃 pSyl 𝐺))
3837ralrimivva 3109 . . . 4 (𝜑 → ∀𝑥𝑋𝑦 ∈ (𝑃 pSyl 𝐺)ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)) ∈ (𝑃 pSyl 𝐺))
39 sylow3lem1.m . . . . 5 = (𝑥𝑋, 𝑦 ∈ (𝑃 pSyl 𝐺) ↦ ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)))
4039fmpt2 7405 . . . 4 (∀𝑥𝑋𝑦 ∈ (𝑃 pSyl 𝐺)ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)) ∈ (𝑃 pSyl 𝐺) ↔ :(𝑋 × (𝑃 pSyl 𝐺))⟶(𝑃 pSyl 𝐺))
4138, 40sylib 208 . . 3 (𝜑 :(𝑋 × (𝑃 pSyl 𝐺))⟶(𝑃 pSyl 𝐺))
421adantr 472 . . . . . . . 8 ((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) → 𝐺 ∈ Grp)
43 eqid 2760 . . . . . . . . 9 (0g𝐺) = (0g𝐺)
446, 43grpidcl 17651 . . . . . . . 8 (𝐺 ∈ Grp → (0g𝐺) ∈ 𝑋)
4542, 44syl 17 . . . . . . 7 ((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) → (0g𝐺) ∈ 𝑋)
46 simpr 479 . . . . . . 7 ((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) → 𝑎 ∈ (𝑃 pSyl 𝐺))
47 simpr 479 . . . . . . . . . 10 ((𝑥 = (0g𝐺) ∧ 𝑦 = 𝑎) → 𝑦 = 𝑎)
48 simpl 474 . . . . . . . . . . . 12 ((𝑥 = (0g𝐺) ∧ 𝑦 = 𝑎) → 𝑥 = (0g𝐺))
4948oveq1d 6828 . . . . . . . . . . 11 ((𝑥 = (0g𝐺) ∧ 𝑦 = 𝑎) → (𝑥 + 𝑧) = ((0g𝐺) + 𝑧))
5049, 48oveq12d 6831 . . . . . . . . . 10 ((𝑥 = (0g𝐺) ∧ 𝑦 = 𝑎) → ((𝑥 + 𝑧) 𝑥) = (((0g𝐺) + 𝑧) (0g𝐺)))
5147, 50mpteq12dv 4885 . . . . . . . . 9 ((𝑥 = (0g𝐺) ∧ 𝑦 = 𝑎) → (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)) = (𝑧𝑎 ↦ (((0g𝐺) + 𝑧) (0g𝐺))))
5251rneqd 5508 . . . . . . . 8 ((𝑥 = (0g𝐺) ∧ 𝑦 = 𝑎) → ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)) = ran (𝑧𝑎 ↦ (((0g𝐺) + 𝑧) (0g𝐺))))
53 vex 3343 . . . . . . . . . 10 𝑎 ∈ V
5453mptex 6650 . . . . . . . . 9 (𝑧𝑎 ↦ (((0g𝐺) + 𝑧) (0g𝐺))) ∈ V
5554rnex 7265 . . . . . . . 8 ran (𝑧𝑎 ↦ (((0g𝐺) + 𝑧) (0g𝐺))) ∈ V
5652, 39, 55ovmpt2a 6956 . . . . . . 7 (((0g𝐺) ∈ 𝑋𝑎 ∈ (𝑃 pSyl 𝐺)) → ((0g𝐺) 𝑎) = ran (𝑧𝑎 ↦ (((0g𝐺) + 𝑧) (0g𝐺))))
5745, 46, 56syl2anc 696 . . . . . 6 ((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) → ((0g𝐺) 𝑎) = ran (𝑧𝑎 ↦ (((0g𝐺) + 𝑧) (0g𝐺))))
581ad2antrr 764 . . . . . . . . . . . . 13 (((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ 𝑧𝑎) → 𝐺 ∈ Grp)
59 slwsubg 18225 . . . . . . . . . . . . . . . 16 (𝑎 ∈ (𝑃 pSyl 𝐺) → 𝑎 ∈ (SubGrp‘𝐺))
6059adantl 473 . . . . . . . . . . . . . . 15 ((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) → 𝑎 ∈ (SubGrp‘𝐺))
616subgss 17796 . . . . . . . . . . . . . . 15 (𝑎 ∈ (SubGrp‘𝐺) → 𝑎𝑋)
6260, 61syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) → 𝑎𝑋)
6362sselda 3744 . . . . . . . . . . . . 13 (((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ 𝑧𝑎) → 𝑧𝑋)
646, 13, 43grplid 17653 . . . . . . . . . . . . 13 ((𝐺 ∈ Grp ∧ 𝑧𝑋) → ((0g𝐺) + 𝑧) = 𝑧)
6558, 63, 64syl2anc 696 . . . . . . . . . . . 12 (((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ 𝑧𝑎) → ((0g𝐺) + 𝑧) = 𝑧)
6665oveq1d 6828 . . . . . . . . . . 11 (((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ 𝑧𝑎) → (((0g𝐺) + 𝑧) (0g𝐺)) = (𝑧 (0g𝐺)))
676, 43, 14grpsubid1 17701 . . . . . . . . . . . 12 ((𝐺 ∈ Grp ∧ 𝑧𝑋) → (𝑧 (0g𝐺)) = 𝑧)
6858, 63, 67syl2anc 696 . . . . . . . . . . 11 (((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ 𝑧𝑎) → (𝑧 (0g𝐺)) = 𝑧)
6966, 68eqtrd 2794 . . . . . . . . . 10 (((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ 𝑧𝑎) → (((0g𝐺) + 𝑧) (0g𝐺)) = 𝑧)
7069mpteq2dva 4896 . . . . . . . . 9 ((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) → (𝑧𝑎 ↦ (((0g𝐺) + 𝑧) (0g𝐺))) = (𝑧𝑎𝑧))
71 mptresid 5614 . . . . . . . . 9 (𝑧𝑎𝑧) = ( I ↾ 𝑎)
7270, 71syl6eq 2810 . . . . . . . 8 ((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) → (𝑧𝑎 ↦ (((0g𝐺) + 𝑧) (0g𝐺))) = ( I ↾ 𝑎))
7372rneqd 5508 . . . . . . 7 ((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) → ran (𝑧𝑎 ↦ (((0g𝐺) + 𝑧) (0g𝐺))) = ran ( I ↾ 𝑎))
74 rnresi 5637 . . . . . . 7 ran ( I ↾ 𝑎) = 𝑎
7573, 74syl6eq 2810 . . . . . 6 ((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) → ran (𝑧𝑎 ↦ (((0g𝐺) + 𝑧) (0g𝐺))) = 𝑎)
7657, 75eqtrd 2794 . . . . 5 ((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) → ((0g𝐺) 𝑎) = 𝑎)
77 ovex 6841 . . . . . . . . . 10 ((𝑐 + 𝑧) 𝑐) ∈ V
78 oveq2 6821 . . . . . . . . . . 11 (𝑤 = ((𝑐 + 𝑧) 𝑐) → (𝑏 + 𝑤) = (𝑏 + ((𝑐 + 𝑧) 𝑐)))
7978oveq1d 6828 . . . . . . . . . 10 (𝑤 = ((𝑐 + 𝑧) 𝑐) → ((𝑏 + 𝑤) 𝑏) = ((𝑏 + ((𝑐 + 𝑧) 𝑐)) 𝑏))
8077, 79abrexco 6665 . . . . . . . . 9 {𝑢 ∣ ∃𝑤 ∈ {𝑣 ∣ ∃𝑧𝑎 𝑣 = ((𝑐 + 𝑧) 𝑐)}𝑢 = ((𝑏 + 𝑤) 𝑏)} = {𝑢 ∣ ∃𝑧𝑎 𝑢 = ((𝑏 + ((𝑐 + 𝑧) 𝑐)) 𝑏)}
81 simprr 813 . . . . . . . . . . . . 13 (((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) → 𝑐𝑋)
82 simplr 809 . . . . . . . . . . . . 13 (((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) → 𝑎 ∈ (𝑃 pSyl 𝐺))
83 simpr 479 . . . . . . . . . . . . . . . 16 ((𝑥 = 𝑐𝑦 = 𝑎) → 𝑦 = 𝑎)
84 simpl 474 . . . . . . . . . . . . . . . . . 18 ((𝑥 = 𝑐𝑦 = 𝑎) → 𝑥 = 𝑐)
8584oveq1d 6828 . . . . . . . . . . . . . . . . 17 ((𝑥 = 𝑐𝑦 = 𝑎) → (𝑥 + 𝑧) = (𝑐 + 𝑧))
8685, 84oveq12d 6831 . . . . . . . . . . . . . . . 16 ((𝑥 = 𝑐𝑦 = 𝑎) → ((𝑥 + 𝑧) 𝑥) = ((𝑐 + 𝑧) 𝑐))
8783, 86mpteq12dv 4885 . . . . . . . . . . . . . . 15 ((𝑥 = 𝑐𝑦 = 𝑎) → (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)) = (𝑧𝑎 ↦ ((𝑐 + 𝑧) 𝑐)))
8887rneqd 5508 . . . . . . . . . . . . . 14 ((𝑥 = 𝑐𝑦 = 𝑎) → ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)) = ran (𝑧𝑎 ↦ ((𝑐 + 𝑧) 𝑐)))
8953mptex 6650 . . . . . . . . . . . . . . 15 (𝑧𝑎 ↦ ((𝑐 + 𝑧) 𝑐)) ∈ V
9089rnex 7265 . . . . . . . . . . . . . 14 ran (𝑧𝑎 ↦ ((𝑐 + 𝑧) 𝑐)) ∈ V
9188, 39, 90ovmpt2a 6956 . . . . . . . . . . . . 13 ((𝑐𝑋𝑎 ∈ (𝑃 pSyl 𝐺)) → (𝑐 𝑎) = ran (𝑧𝑎 ↦ ((𝑐 + 𝑧) 𝑐)))
9281, 82, 91syl2anc 696 . . . . . . . . . . . 12 (((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) → (𝑐 𝑎) = ran (𝑧𝑎 ↦ ((𝑐 + 𝑧) 𝑐)))
93 eqid 2760 . . . . . . . . . . . . 13 (𝑧𝑎 ↦ ((𝑐 + 𝑧) 𝑐)) = (𝑧𝑎 ↦ ((𝑐 + 𝑧) 𝑐))
9493rnmpt 5526 . . . . . . . . . . . 12 ran (𝑧𝑎 ↦ ((𝑐 + 𝑧) 𝑐)) = {𝑣 ∣ ∃𝑧𝑎 𝑣 = ((𝑐 + 𝑧) 𝑐)}
9592, 94syl6eq 2810 . . . . . . . . . . 11 (((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) → (𝑐 𝑎) = {𝑣 ∣ ∃𝑧𝑎 𝑣 = ((𝑐 + 𝑧) 𝑐)})
9695rexeqdv 3284 . . . . . . . . . 10 (((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) → (∃𝑤 ∈ (𝑐 𝑎)𝑢 = ((𝑏 + 𝑤) 𝑏) ↔ ∃𝑤 ∈ {𝑣 ∣ ∃𝑧𝑎 𝑣 = ((𝑐 + 𝑧) 𝑐)}𝑢 = ((𝑏 + 𝑤) 𝑏)))
9796abbidv 2879 . . . . . . . . 9 (((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) → {𝑢 ∣ ∃𝑤 ∈ (𝑐 𝑎)𝑢 = ((𝑏 + 𝑤) 𝑏)} = {𝑢 ∣ ∃𝑤 ∈ {𝑣 ∣ ∃𝑧𝑎 𝑣 = ((𝑐 + 𝑧) 𝑐)}𝑢 = ((𝑏 + 𝑤) 𝑏)})
9842adantr 472 . . . . . . . . . . . . . . 15 (((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) → 𝐺 ∈ Grp)
9998adantr 472 . . . . . . . . . . . . . 14 ((((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → 𝐺 ∈ Grp)
100 simprl 811 . . . . . . . . . . . . . . . . 17 (((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) → 𝑏𝑋)
1016, 13grpcl 17631 . . . . . . . . . . . . . . . . 17 ((𝐺 ∈ Grp ∧ 𝑏𝑋𝑐𝑋) → (𝑏 + 𝑐) ∈ 𝑋)
10298, 100, 81, 101syl3anc 1477 . . . . . . . . . . . . . . . 16 (((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) → (𝑏 + 𝑐) ∈ 𝑋)
103102adantr 472 . . . . . . . . . . . . . . 15 ((((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → (𝑏 + 𝑐) ∈ 𝑋)
10463adantlr 753 . . . . . . . . . . . . . . 15 ((((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → 𝑧𝑋)
1056, 13grpcl 17631 . . . . . . . . . . . . . . 15 ((𝐺 ∈ Grp ∧ (𝑏 + 𝑐) ∈ 𝑋𝑧𝑋) → ((𝑏 + 𝑐) + 𝑧) ∈ 𝑋)
10699, 103, 104, 105syl3anc 1477 . . . . . . . . . . . . . 14 ((((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → ((𝑏 + 𝑐) + 𝑧) ∈ 𝑋)
10781adantr 472 . . . . . . . . . . . . . 14 ((((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → 𝑐𝑋)
108100adantr 472 . . . . . . . . . . . . . 14 ((((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → 𝑏𝑋)
1096, 13, 14grpsubsub4 17709 . . . . . . . . . . . . . 14 ((𝐺 ∈ Grp ∧ (((𝑏 + 𝑐) + 𝑧) ∈ 𝑋𝑐𝑋𝑏𝑋)) → ((((𝑏 + 𝑐) + 𝑧) 𝑐) 𝑏) = (((𝑏 + 𝑐) + 𝑧) (𝑏 + 𝑐)))
11099, 106, 107, 108, 109syl13anc 1479 . . . . . . . . . . . . 13 ((((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → ((((𝑏 + 𝑐) + 𝑧) 𝑐) 𝑏) = (((𝑏 + 𝑐) + 𝑧) (𝑏 + 𝑐)))
1116, 13grpass 17632 . . . . . . . . . . . . . . . . 17 ((𝐺 ∈ Grp ∧ (𝑏𝑋𝑐𝑋𝑧𝑋)) → ((𝑏 + 𝑐) + 𝑧) = (𝑏 + (𝑐 + 𝑧)))
11299, 108, 107, 104, 111syl13anc 1479 . . . . . . . . . . . . . . . 16 ((((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → ((𝑏 + 𝑐) + 𝑧) = (𝑏 + (𝑐 + 𝑧)))
113112oveq1d 6828 . . . . . . . . . . . . . . 15 ((((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → (((𝑏 + 𝑐) + 𝑧) 𝑐) = ((𝑏 + (𝑐 + 𝑧)) 𝑐))
1146, 13grpcl 17631 . . . . . . . . . . . . . . . . 17 ((𝐺 ∈ Grp ∧ 𝑐𝑋𝑧𝑋) → (𝑐 + 𝑧) ∈ 𝑋)
11599, 107, 104, 114syl3anc 1477 . . . . . . . . . . . . . . . 16 ((((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → (𝑐 + 𝑧) ∈ 𝑋)
1166, 13, 14grpaddsubass 17706 . . . . . . . . . . . . . . . 16 ((𝐺 ∈ Grp ∧ (𝑏𝑋 ∧ (𝑐 + 𝑧) ∈ 𝑋𝑐𝑋)) → ((𝑏 + (𝑐 + 𝑧)) 𝑐) = (𝑏 + ((𝑐 + 𝑧) 𝑐)))
11799, 108, 115, 107, 116syl13anc 1479 . . . . . . . . . . . . . . 15 ((((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → ((𝑏 + (𝑐 + 𝑧)) 𝑐) = (𝑏 + ((𝑐 + 𝑧) 𝑐)))
118113, 117eqtrd 2794 . . . . . . . . . . . . . 14 ((((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → (((𝑏 + 𝑐) + 𝑧) 𝑐) = (𝑏 + ((𝑐 + 𝑧) 𝑐)))
119118oveq1d 6828 . . . . . . . . . . . . 13 ((((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → ((((𝑏 + 𝑐) + 𝑧) 𝑐) 𝑏) = ((𝑏 + ((𝑐 + 𝑧) 𝑐)) 𝑏))
120110, 119eqtr3d 2796 . . . . . . . . . . . 12 ((((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → (((𝑏 + 𝑐) + 𝑧) (𝑏 + 𝑐)) = ((𝑏 + ((𝑐 + 𝑧) 𝑐)) 𝑏))
121120eqeq2d 2770 . . . . . . . . . . 11 ((((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → (𝑢 = (((𝑏 + 𝑐) + 𝑧) (𝑏 + 𝑐)) ↔ 𝑢 = ((𝑏 + ((𝑐 + 𝑧) 𝑐)) 𝑏)))
122121rexbidva 3187 . . . . . . . . . 10 (((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) → (∃𝑧𝑎 𝑢 = (((𝑏 + 𝑐) + 𝑧) (𝑏 + 𝑐)) ↔ ∃𝑧𝑎 𝑢 = ((𝑏 + ((𝑐 + 𝑧) 𝑐)) 𝑏)))
123122abbidv 2879 . . . . . . . . 9 (((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) → {𝑢 ∣ ∃𝑧𝑎 𝑢 = (((𝑏 + 𝑐) + 𝑧) (𝑏 + 𝑐))} = {𝑢 ∣ ∃𝑧𝑎 𝑢 = ((𝑏 + ((𝑐 + 𝑧) 𝑐)) 𝑏)})
12480, 97, 1233eqtr4a 2820 . . . . . . . 8 (((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) → {𝑢 ∣ ∃𝑤 ∈ (𝑐 𝑎)𝑢 = ((𝑏 + 𝑤) 𝑏)} = {𝑢 ∣ ∃𝑧𝑎 𝑢 = (((𝑏 + 𝑐) + 𝑧) (𝑏 + 𝑐))})
125 eqid 2760 . . . . . . . . 9 (𝑤 ∈ (𝑐 𝑎) ↦ ((𝑏 + 𝑤) 𝑏)) = (𝑤 ∈ (𝑐 𝑎) ↦ ((𝑏 + 𝑤) 𝑏))
126125rnmpt 5526 . . . . . . . 8 ran (𝑤 ∈ (𝑐 𝑎) ↦ ((𝑏 + 𝑤) 𝑏)) = {𝑢 ∣ ∃𝑤 ∈ (𝑐 𝑎)𝑢 = ((𝑏 + 𝑤) 𝑏)}
127 eqid 2760 . . . . . . . . 9 (𝑧𝑎 ↦ (((𝑏 + 𝑐) + 𝑧) (𝑏 + 𝑐))) = (𝑧𝑎 ↦ (((𝑏 + 𝑐) + 𝑧) (𝑏 + 𝑐)))
128127rnmpt 5526 . . . . . . . 8 ran (𝑧𝑎 ↦ (((𝑏 + 𝑐) + 𝑧) (𝑏 + 𝑐))) = {𝑢 ∣ ∃𝑧𝑎 𝑢 = (((𝑏 + 𝑐) + 𝑧) (𝑏 + 𝑐))}
129124, 126, 1283eqtr4g 2819 . . . . . . 7 (((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) → ran (𝑤 ∈ (𝑐 𝑎) ↦ ((𝑏 + 𝑤) 𝑏)) = ran (𝑧𝑎 ↦ (((𝑏 + 𝑐) + 𝑧) (𝑏 + 𝑐))))
13041ad2antrr 764 . . . . . . . . 9 (((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) → :(𝑋 × (𝑃 pSyl 𝐺))⟶(𝑃 pSyl 𝐺))
131130, 81, 82fovrnd 6971 . . . . . . . 8 (((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) → (𝑐 𝑎) ∈ (𝑃 pSyl 𝐺))
132 simpr 479 . . . . . . . . . . . 12 ((𝑥 = 𝑏𝑦 = (𝑐 𝑎)) → 𝑦 = (𝑐 𝑎))
133 simpl 474 . . . . . . . . . . . . . 14 ((𝑥 = 𝑏𝑦 = (𝑐 𝑎)) → 𝑥 = 𝑏)
134133oveq1d 6828 . . . . . . . . . . . . 13 ((𝑥 = 𝑏𝑦 = (𝑐 𝑎)) → (𝑥 + 𝑧) = (𝑏 + 𝑧))
135134, 133oveq12d 6831 . . . . . . . . . . . 12 ((𝑥 = 𝑏𝑦 = (𝑐 𝑎)) → ((𝑥 + 𝑧) 𝑥) = ((𝑏 + 𝑧) 𝑏))
136132, 135mpteq12dv 4885 . . . . . . . . . . 11 ((𝑥 = 𝑏𝑦 = (𝑐 𝑎)) → (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)) = (𝑧 ∈ (𝑐 𝑎) ↦ ((𝑏 + 𝑧) 𝑏)))
137 oveq2 6821 . . . . . . . . . . . . 13 (𝑧 = 𝑤 → (𝑏 + 𝑧) = (𝑏 + 𝑤))
138137oveq1d 6828 . . . . . . . . . . . 12 (𝑧 = 𝑤 → ((𝑏 + 𝑧) 𝑏) = ((𝑏 + 𝑤) 𝑏))
139138cbvmptv 4902 . . . . . . . . . . 11 (𝑧 ∈ (𝑐 𝑎) ↦ ((𝑏 + 𝑧) 𝑏)) = (𝑤 ∈ (𝑐 𝑎) ↦ ((𝑏 + 𝑤) 𝑏))
140136, 139syl6eq 2810 . . . . . . . . . 10 ((𝑥 = 𝑏𝑦 = (𝑐 𝑎)) → (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)) = (𝑤 ∈ (𝑐 𝑎) ↦ ((𝑏 + 𝑤) 𝑏)))
141140rneqd 5508 . . . . . . . . 9 ((𝑥 = 𝑏𝑦 = (𝑐 𝑎)) → ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)) = ran (𝑤 ∈ (𝑐 𝑎) ↦ ((𝑏 + 𝑤) 𝑏)))
142 ovex 6841 . . . . . . . . . . 11 (𝑐 𝑎) ∈ V
143142mptex 6650 . . . . . . . . . 10 (𝑤 ∈ (𝑐 𝑎) ↦ ((𝑏 + 𝑤) 𝑏)) ∈ V
144143rnex 7265 . . . . . . . . 9 ran (𝑤 ∈ (𝑐 𝑎) ↦ ((𝑏 + 𝑤) 𝑏)) ∈ V
145141, 39, 144ovmpt2a 6956 . . . . . . . 8 ((𝑏𝑋 ∧ (𝑐 𝑎) ∈ (𝑃 pSyl 𝐺)) → (𝑏 (𝑐 𝑎)) = ran (𝑤 ∈ (𝑐 𝑎) ↦ ((𝑏 + 𝑤) 𝑏)))
146100, 131, 145syl2anc 696 . . . . . . 7 (((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) → (𝑏 (𝑐 𝑎)) = ran (𝑤 ∈ (𝑐 𝑎) ↦ ((𝑏 + 𝑤) 𝑏)))
147 simpr 479 . . . . . . . . . . 11 ((𝑥 = (𝑏 + 𝑐) ∧ 𝑦 = 𝑎) → 𝑦 = 𝑎)
148 simpl 474 . . . . . . . . . . . . 13 ((𝑥 = (𝑏 + 𝑐) ∧ 𝑦 = 𝑎) → 𝑥 = (𝑏 + 𝑐))
149148oveq1d 6828 . . . . . . . . . . . 12 ((𝑥 = (𝑏 + 𝑐) ∧ 𝑦 = 𝑎) → (𝑥 + 𝑧) = ((𝑏 + 𝑐) + 𝑧))
150149, 148oveq12d 6831 . . . . . . . . . . 11 ((𝑥 = (𝑏 + 𝑐) ∧ 𝑦 = 𝑎) → ((𝑥 + 𝑧) 𝑥) = (((𝑏 + 𝑐) + 𝑧) (𝑏 + 𝑐)))
151147, 150mpteq12dv 4885 . . . . . . . . . 10 ((𝑥 = (𝑏 + 𝑐) ∧ 𝑦 = 𝑎) → (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)) = (𝑧𝑎 ↦ (((𝑏 + 𝑐) + 𝑧) (𝑏 + 𝑐))))
152151rneqd 5508 . . . . . . . . 9 ((𝑥 = (𝑏 + 𝑐) ∧ 𝑦 = 𝑎) → ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)) = ran (𝑧𝑎 ↦ (((𝑏 + 𝑐) + 𝑧) (𝑏 + 𝑐))))
15353mptex 6650 . . . . . . . . . 10 (𝑧𝑎 ↦ (((𝑏 + 𝑐) + 𝑧) (𝑏 + 𝑐))) ∈ V
154153rnex 7265 . . . . . . . . 9 ran (𝑧𝑎 ↦ (((𝑏 + 𝑐) + 𝑧) (𝑏 + 𝑐))) ∈ V
155152, 39, 154ovmpt2a 6956 . . . . . . . 8 (((𝑏 + 𝑐) ∈ 𝑋𝑎 ∈ (𝑃 pSyl 𝐺)) → ((𝑏 + 𝑐) 𝑎) = ran (𝑧𝑎 ↦ (((𝑏 + 𝑐) + 𝑧) (𝑏 + 𝑐))))
156102, 82, 155syl2anc 696 . . . . . . 7 (((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) → ((𝑏 + 𝑐) 𝑎) = ran (𝑧𝑎 ↦ (((𝑏 + 𝑐) + 𝑧) (𝑏 + 𝑐))))
157129, 146, 1563eqtr4rd 2805 . . . . . 6 (((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) → ((𝑏 + 𝑐) 𝑎) = (𝑏 (𝑐 𝑎)))
158157ralrimivva 3109 . . . . 5 ((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) → ∀𝑏𝑋𝑐𝑋 ((𝑏 + 𝑐) 𝑎) = (𝑏 (𝑐 𝑎)))
15976, 158jca 555 . . . 4 ((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) → (((0g𝐺) 𝑎) = 𝑎 ∧ ∀𝑏𝑋𝑐𝑋 ((𝑏 + 𝑐) 𝑎) = (𝑏 (𝑐 𝑎))))
160159ralrimiva 3104 . . 3 (𝜑 → ∀𝑎 ∈ (𝑃 pSyl 𝐺)(((0g𝐺) 𝑎) = 𝑎 ∧ ∀𝑏𝑋𝑐𝑋 ((𝑏 + 𝑐) 𝑎) = (𝑏 (𝑐 𝑎))))
16141, 160jca 555 . 2 (𝜑 → ( :(𝑋 × (𝑃 pSyl 𝐺))⟶(𝑃 pSyl 𝐺) ∧ ∀𝑎 ∈ (𝑃 pSyl 𝐺)(((0g𝐺) 𝑎) = 𝑎 ∧ ∀𝑏𝑋𝑐𝑋 ((𝑏 + 𝑐) 𝑎) = (𝑏 (𝑐 𝑎)))))
1626, 13, 43isga 17924 . 2 ( ∈ (𝐺 GrpAct (𝑃 pSyl 𝐺)) ↔ ((𝐺 ∈ Grp ∧ (𝑃 pSyl 𝐺) ∈ V) ∧ ( :(𝑋 × (𝑃 pSyl 𝐺))⟶(𝑃 pSyl 𝐺) ∧ ∀𝑎 ∈ (𝑃 pSyl 𝐺)(((0g𝐺) 𝑎) = 𝑎 ∧ ∀𝑏𝑋𝑐𝑋 ((𝑏 + 𝑐) 𝑎) = (𝑏 (𝑐 𝑎))))))
1633, 161, 162sylanbrc 701 1 (𝜑 ∈ (𝐺 GrpAct (𝑃 pSyl 𝐺)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   = wceq 1632   ∈ wcel 2139  {cab 2746  ∀wral 3050  ∃wrex 3051  Vcvv 3340   ⊆ wss 3715   class class class wbr 4804   ↦ cmpt 4881   I cid 5173   × cxp 5264  ran crn 5267   ↾ cres 5268  ⟶wf 6045  ‘cfv 6049  (class class class)co 6813   ↦ cmpt2 6815   ≈ cen 8118  Fincfn 8121  ↑cexp 13054  ♯chash 13311  ℙcprime 15587   pCnt cpc 15743  Basecbs 16059  +gcplusg 16143  0gc0g 16302  Grpcgrp 17623  -gcsg 17625  SubGrpcsubg 17789   GrpAct cga 17922   pSyl cslw 18147 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114  ax-inf2 8711  ax-cnex 10184  ax-resscn 10185  ax-1cn 10186  ax-icn 10187  ax-addcl 10188  ax-addrcl 10189  ax-mulcl 10190  ax-mulrcl 10191  ax-mulcom 10192  ax-addass 10193  ax-mulass 10194  ax-distr 10195  ax-i2m1 10196  ax-1ne0 10197  ax-1rid 10198  ax-rnegex 10199  ax-rrecex 10200  ax-cnre 10201  ax-pre-lttri 10202  ax-pre-lttrn 10203  ax-pre-ltadd 10204  ax-pre-mulgt0 10205  ax-pre-sup 10206 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1635  df-fal 1638  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-nel 3036  df-ral 3055  df-rex 3056  df-reu 3057  df-rmo 3058  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-pss 3731  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-tp 4326  df-op 4328  df-uni 4589  df-int 4628  df-iun 4674  df-disj 4773  df-br 4805  df-opab 4865  df-mpt 4882  df-tr 4905  df-id 5174  df-eprel 5179  df-po 5187  df-so 5188  df-fr 5225  df-se 5226  df-we 5227  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-pred 5841  df-ord 5887  df-on 5888  df-lim 5889  df-suc 5890  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-isom 6058  df-riota 6774  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-om 7231  df-1st 7333  df-2nd 7334  df-wrecs 7576  df-recs 7637  df-rdg 7675  df-1o 7729  df-2o 7730  df-oadd 7733  df-omul 7734  df-er 7911  df-ec 7913  df-qs 7917  df-map 8025  df-en 8122  df-dom 8123  df-sdom 8124  df-fin 8125  df-sup 8513  df-inf 8514  df-oi 8580  df-card 8955  df-acn 8958  df-cda 9182  df-pnf 10268  df-mnf 10269  df-xr 10270  df-ltxr 10271  df-le 10272  df-sub 10460  df-neg 10461  df-div 10877  df-nn 11213  df-2 11271  df-3 11272  df-n0 11485  df-xnn0 11556  df-z 11570  df-uz 11880  df-q 11982  df-rp 12026  df-fz 12520  df-fzo 12660  df-fl 12787  df-mod 12863  df-seq 12996  df-exp 13055  df-fac 13255  df-bc 13284  df-hash 13312  df-cj 14038  df-re 14039  df-im 14040  df-sqrt 14174  df-abs 14175  df-clim 14418  df-sum 14616  df-dvds 15183  df-gcd 15419  df-prm 15588  df-pc 15744  df-ndx 16062  df-slot 16063  df-base 16065  df-sets 16066  df-ress 16067  df-plusg 16156  df-0g 16304  df-mgm 17443  df-sgrp 17485  df-mnd 17496  df-submnd 17537  df-grp 17626  df-minusg 17627  df-sbg 17628  df-mulg 17742  df-subg 17792  df-eqg 17794  df-ghm 17859  df-ga 17923  df-od 18148  df-pgp 18150  df-slw 18151 This theorem is referenced by:  sylow3lem3  18244  sylow3lem5  18246
 Copyright terms: Public domain W3C validator