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

Theorem sylow3lem1 17982
Description: Lemma for sylow3 17988, 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 6643 . . 3 (𝑃 pSyl 𝐺) ∈ V
31, 2jctir 560 . 2 (𝜑 → (𝐺 ∈ Grp ∧ (𝑃 pSyl 𝐺) ∈ V))
4 sylow3.xf . . . . . . . . . . 11 (𝜑𝑋 ∈ Fin)
5 sylow3.p . . . . . . . . . . 11 (𝜑𝑃 ∈ ℙ)
6 sylow3.x . . . . . . . . . . . 12 𝑋 = (Base‘𝐺)
76fislw 17980 . . . . . . . . . . 11 ((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) → (𝑦 ∈ (𝑃 pSyl 𝐺) ↔ (𝑦 ∈ (SubGrp‘𝐺) ∧ (#‘𝑦) = (𝑃↑(𝑃 pCnt (#‘𝑋))))))
81, 4, 5, 7syl3anc 1323 . . . . . . . . . 10 (𝜑 → (𝑦 ∈ (𝑃 pSyl 𝐺) ↔ (𝑦 ∈ (SubGrp‘𝐺) ∧ (#‘𝑦) = (𝑃↑(𝑃 pCnt (#‘𝑋))))))
98biimpa 501 . . . . . . . . 9 ((𝜑𝑦 ∈ (𝑃 pSyl 𝐺)) → (𝑦 ∈ (SubGrp‘𝐺) ∧ (#‘𝑦) = (𝑃↑(𝑃 pCnt (#‘𝑋)))))
109adantrl 751 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑋𝑦 ∈ (𝑃 pSyl 𝐺))) → (𝑦 ∈ (SubGrp‘𝐺) ∧ (#‘𝑦) = (𝑃↑(𝑃 pCnt (#‘𝑋)))))
1110simpld 475 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦 ∈ (𝑃 pSyl 𝐺))) → 𝑦 ∈ (SubGrp‘𝐺))
12 simprl 793 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦 ∈ (𝑃 pSyl 𝐺))) → 𝑥𝑋)
13 sylow3lem1.a . . . . . . . 8 + = (+g𝐺)
14 sylow3lem1.d . . . . . . . 8 = (-g𝐺)
15 eqid 2621 . . . . . . . 8 (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)) = (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥))
166, 13, 14, 15conjsubg 17632 . . . . . . 7 ((𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑥𝑋) → ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)) ∈ (SubGrp‘𝐺))
1711, 12, 16syl2anc 692 . . . . . 6 ((𝜑 ∧ (𝑥𝑋𝑦 ∈ (𝑃 pSyl 𝐺))) → ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)) ∈ (SubGrp‘𝐺))
186, 13, 14, 15conjsubgen 17633 . . . . . . . . 9 ((𝑦 ∈ (SubGrp‘𝐺) ∧ 𝑥𝑋) → 𝑦 ≈ ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)))
1911, 12, 18syl2anc 692 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑋𝑦 ∈ (𝑃 pSyl 𝐺))) → 𝑦 ≈ ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)))
204adantr 481 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑦 ∈ (𝑃 pSyl 𝐺))) → 𝑋 ∈ Fin)
216subgss 17535 . . . . . . . . . . 11 (𝑦 ∈ (SubGrp‘𝐺) → 𝑦𝑋)
2211, 21syl 17 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑦 ∈ (𝑃 pSyl 𝐺))) → 𝑦𝑋)
23 ssfi 8140 . . . . . . . . . 10 ((𝑋 ∈ Fin ∧ 𝑦𝑋) → 𝑦 ∈ Fin)
2420, 22, 23syl2anc 692 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦 ∈ (𝑃 pSyl 𝐺))) → 𝑦 ∈ Fin)
256subgss 17535 . . . . . . . . . . 11 (ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)) ∈ (SubGrp‘𝐺) → ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)) ⊆ 𝑋)
2617, 25syl 17 . . . . . . . . . 10 ((𝜑 ∧ (𝑥𝑋𝑦 ∈ (𝑃 pSyl 𝐺))) → ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)) ⊆ 𝑋)
27 ssfi 8140 . . . . . . . . . 10 ((𝑋 ∈ Fin ∧ ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)) ⊆ 𝑋) → ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)) ∈ Fin)
2820, 26, 27syl2anc 692 . . . . . . . . 9 ((𝜑 ∧ (𝑥𝑋𝑦 ∈ (𝑃 pSyl 𝐺))) → ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)) ∈ Fin)
29 hashen 13091 . . . . . . . . 9 ((𝑦 ∈ Fin ∧ ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)) ∈ Fin) → ((#‘𝑦) = (#‘ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥))) ↔ 𝑦 ≈ ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥))))
3024, 28, 29syl2anc 692 . . . . . . . 8 ((𝜑 ∧ (𝑥𝑋𝑦 ∈ (𝑃 pSyl 𝐺))) → ((#‘𝑦) = (#‘ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥))) ↔ 𝑦 ≈ ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥))))
3119, 30mpbird 247 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦 ∈ (𝑃 pSyl 𝐺))) → (#‘𝑦) = (#‘ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥))))
3210simprd 479 . . . . . . 7 ((𝜑 ∧ (𝑥𝑋𝑦 ∈ (𝑃 pSyl 𝐺))) → (#‘𝑦) = (𝑃↑(𝑃 pCnt (#‘𝑋))))
3331, 32eqtr3d 2657 . . . . . 6 ((𝜑 ∧ (𝑥𝑋𝑦 ∈ (𝑃 pSyl 𝐺))) → (#‘ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥))) = (𝑃↑(𝑃 pCnt (#‘𝑋))))
346fislw 17980 . . . . . . . 8 ((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin ∧ 𝑃 ∈ ℙ) → (ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)) ∈ (𝑃 pSyl 𝐺) ↔ (ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)) ∈ (SubGrp‘𝐺) ∧ (#‘ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥))) = (𝑃↑(𝑃 pCnt (#‘𝑋))))))
351, 4, 5, 34syl3anc 1323 . . . . . . 7 (𝜑 → (ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)) ∈ (𝑃 pSyl 𝐺) ↔ (ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)) ∈ (SubGrp‘𝐺) ∧ (#‘ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥))) = (𝑃↑(𝑃 pCnt (#‘𝑋))))))
3635adantr 481 . . . . . 6 ((𝜑 ∧ (𝑥𝑋𝑦 ∈ (𝑃 pSyl 𝐺))) → (ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)) ∈ (𝑃 pSyl 𝐺) ↔ (ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)) ∈ (SubGrp‘𝐺) ∧ (#‘ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥))) = (𝑃↑(𝑃 pCnt (#‘𝑋))))))
3717, 33, 36mpbir2and 956 . . . . 5 ((𝜑 ∧ (𝑥𝑋𝑦 ∈ (𝑃 pSyl 𝐺))) → ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)) ∈ (𝑃 pSyl 𝐺))
3837ralrimivva 2967 . . . 4 (𝜑 → ∀𝑥𝑋𝑦 ∈ (𝑃 pSyl 𝐺)ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)) ∈ (𝑃 pSyl 𝐺))
39 sylow3lem1.m . . . . 5 = (𝑥𝑋, 𝑦 ∈ (𝑃 pSyl 𝐺) ↦ ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)))
4039fmpt2 7197 . . . 4 (∀𝑥𝑋𝑦 ∈ (𝑃 pSyl 𝐺)ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)) ∈ (𝑃 pSyl 𝐺) ↔ :(𝑋 × (𝑃 pSyl 𝐺))⟶(𝑃 pSyl 𝐺))
4138, 40sylib 208 . . 3 (𝜑 :(𝑋 × (𝑃 pSyl 𝐺))⟶(𝑃 pSyl 𝐺))
421adantr 481 . . . . . . . 8 ((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) → 𝐺 ∈ Grp)
43 eqid 2621 . . . . . . . . 9 (0g𝐺) = (0g𝐺)
446, 43grpidcl 17390 . . . . . . . 8 (𝐺 ∈ Grp → (0g𝐺) ∈ 𝑋)
4542, 44syl 17 . . . . . . 7 ((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) → (0g𝐺) ∈ 𝑋)
46 simpr 477 . . . . . . 7 ((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) → 𝑎 ∈ (𝑃 pSyl 𝐺))
47 simpr 477 . . . . . . . . . 10 ((𝑥 = (0g𝐺) ∧ 𝑦 = 𝑎) → 𝑦 = 𝑎)
48 simpl 473 . . . . . . . . . . . 12 ((𝑥 = (0g𝐺) ∧ 𝑦 = 𝑎) → 𝑥 = (0g𝐺))
4948oveq1d 6630 . . . . . . . . . . 11 ((𝑥 = (0g𝐺) ∧ 𝑦 = 𝑎) → (𝑥 + 𝑧) = ((0g𝐺) + 𝑧))
5049, 48oveq12d 6633 . . . . . . . . . 10 ((𝑥 = (0g𝐺) ∧ 𝑦 = 𝑎) → ((𝑥 + 𝑧) 𝑥) = (((0g𝐺) + 𝑧) (0g𝐺)))
5147, 50mpteq12dv 4703 . . . . . . . . 9 ((𝑥 = (0g𝐺) ∧ 𝑦 = 𝑎) → (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)) = (𝑧𝑎 ↦ (((0g𝐺) + 𝑧) (0g𝐺))))
5251rneqd 5323 . . . . . . . 8 ((𝑥 = (0g𝐺) ∧ 𝑦 = 𝑎) → ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)) = ran (𝑧𝑎 ↦ (((0g𝐺) + 𝑧) (0g𝐺))))
53 vex 3193 . . . . . . . . . 10 𝑎 ∈ V
5453mptex 6451 . . . . . . . . 9 (𝑧𝑎 ↦ (((0g𝐺) + 𝑧) (0g𝐺))) ∈ V
5554rnex 7062 . . . . . . . 8 ran (𝑧𝑎 ↦ (((0g𝐺) + 𝑧) (0g𝐺))) ∈ V
5652, 39, 55ovmpt2a 6756 . . . . . . 7 (((0g𝐺) ∈ 𝑋𝑎 ∈ (𝑃 pSyl 𝐺)) → ((0g𝐺) 𝑎) = ran (𝑧𝑎 ↦ (((0g𝐺) + 𝑧) (0g𝐺))))
5745, 46, 56syl2anc 692 . . . . . 6 ((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) → ((0g𝐺) 𝑎) = ran (𝑧𝑎 ↦ (((0g𝐺) + 𝑧) (0g𝐺))))
581ad2antrr 761 . . . . . . . . . . . . 13 (((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ 𝑧𝑎) → 𝐺 ∈ Grp)
59 slwsubg 17965 . . . . . . . . . . . . . . . 16 (𝑎 ∈ (𝑃 pSyl 𝐺) → 𝑎 ∈ (SubGrp‘𝐺))
6059adantl 482 . . . . . . . . . . . . . . 15 ((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) → 𝑎 ∈ (SubGrp‘𝐺))
616subgss 17535 . . . . . . . . . . . . . . 15 (𝑎 ∈ (SubGrp‘𝐺) → 𝑎𝑋)
6260, 61syl 17 . . . . . . . . . . . . . 14 ((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) → 𝑎𝑋)
6362sselda 3588 . . . . . . . . . . . . 13 (((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ 𝑧𝑎) → 𝑧𝑋)
646, 13, 43grplid 17392 . . . . . . . . . . . . 13 ((𝐺 ∈ Grp ∧ 𝑧𝑋) → ((0g𝐺) + 𝑧) = 𝑧)
6558, 63, 64syl2anc 692 . . . . . . . . . . . 12 (((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ 𝑧𝑎) → ((0g𝐺) + 𝑧) = 𝑧)
6665oveq1d 6630 . . . . . . . . . . 11 (((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ 𝑧𝑎) → (((0g𝐺) + 𝑧) (0g𝐺)) = (𝑧 (0g𝐺)))
676, 43, 14grpsubid1 17440 . . . . . . . . . . . 12 ((𝐺 ∈ Grp ∧ 𝑧𝑋) → (𝑧 (0g𝐺)) = 𝑧)
6858, 63, 67syl2anc 692 . . . . . . . . . . 11 (((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ 𝑧𝑎) → (𝑧 (0g𝐺)) = 𝑧)
6966, 68eqtrd 2655 . . . . . . . . . 10 (((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ 𝑧𝑎) → (((0g𝐺) + 𝑧) (0g𝐺)) = 𝑧)
7069mpteq2dva 4714 . . . . . . . . 9 ((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) → (𝑧𝑎 ↦ (((0g𝐺) + 𝑧) (0g𝐺))) = (𝑧𝑎𝑧))
71 mptresid 5425 . . . . . . . . 9 (𝑧𝑎𝑧) = ( I ↾ 𝑎)
7270, 71syl6eq 2671 . . . . . . . 8 ((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) → (𝑧𝑎 ↦ (((0g𝐺) + 𝑧) (0g𝐺))) = ( I ↾ 𝑎))
7372rneqd 5323 . . . . . . 7 ((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) → ran (𝑧𝑎 ↦ (((0g𝐺) + 𝑧) (0g𝐺))) = ran ( I ↾ 𝑎))
74 rnresi 5448 . . . . . . 7 ran ( I ↾ 𝑎) = 𝑎
7573, 74syl6eq 2671 . . . . . 6 ((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) → ran (𝑧𝑎 ↦ (((0g𝐺) + 𝑧) (0g𝐺))) = 𝑎)
7657, 75eqtrd 2655 . . . . 5 ((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) → ((0g𝐺) 𝑎) = 𝑎)
77 ovex 6643 . . . . . . . . . 10 ((𝑐 + 𝑧) 𝑐) ∈ V
78 oveq2 6623 . . . . . . . . . . 11 (𝑤 = ((𝑐 + 𝑧) 𝑐) → (𝑏 + 𝑤) = (𝑏 + ((𝑐 + 𝑧) 𝑐)))
7978oveq1d 6630 . . . . . . . . . 10 (𝑤 = ((𝑐 + 𝑧) 𝑐) → ((𝑏 + 𝑤) 𝑏) = ((𝑏 + ((𝑐 + 𝑧) 𝑐)) 𝑏))
8077, 79abrexco 6467 . . . . . . . . 9 {𝑢 ∣ ∃𝑤 ∈ {𝑣 ∣ ∃𝑧𝑎 𝑣 = ((𝑐 + 𝑧) 𝑐)}𝑢 = ((𝑏 + 𝑤) 𝑏)} = {𝑢 ∣ ∃𝑧𝑎 𝑢 = ((𝑏 + ((𝑐 + 𝑧) 𝑐)) 𝑏)}
81 simprr 795 . . . . . . . . . . . . 13 (((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) → 𝑐𝑋)
82 simplr 791 . . . . . . . . . . . . 13 (((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) → 𝑎 ∈ (𝑃 pSyl 𝐺))
83 simpr 477 . . . . . . . . . . . . . . . 16 ((𝑥 = 𝑐𝑦 = 𝑎) → 𝑦 = 𝑎)
84 simpl 473 . . . . . . . . . . . . . . . . . 18 ((𝑥 = 𝑐𝑦 = 𝑎) → 𝑥 = 𝑐)
8584oveq1d 6630 . . . . . . . . . . . . . . . . 17 ((𝑥 = 𝑐𝑦 = 𝑎) → (𝑥 + 𝑧) = (𝑐 + 𝑧))
8685, 84oveq12d 6633 . . . . . . . . . . . . . . . 16 ((𝑥 = 𝑐𝑦 = 𝑎) → ((𝑥 + 𝑧) 𝑥) = ((𝑐 + 𝑧) 𝑐))
8783, 86mpteq12dv 4703 . . . . . . . . . . . . . . 15 ((𝑥 = 𝑐𝑦 = 𝑎) → (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)) = (𝑧𝑎 ↦ ((𝑐 + 𝑧) 𝑐)))
8887rneqd 5323 . . . . . . . . . . . . . 14 ((𝑥 = 𝑐𝑦 = 𝑎) → ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)) = ran (𝑧𝑎 ↦ ((𝑐 + 𝑧) 𝑐)))
8953mptex 6451 . . . . . . . . . . . . . . 15 (𝑧𝑎 ↦ ((𝑐 + 𝑧) 𝑐)) ∈ V
9089rnex 7062 . . . . . . . . . . . . . 14 ran (𝑧𝑎 ↦ ((𝑐 + 𝑧) 𝑐)) ∈ V
9188, 39, 90ovmpt2a 6756 . . . . . . . . . . . . 13 ((𝑐𝑋𝑎 ∈ (𝑃 pSyl 𝐺)) → (𝑐 𝑎) = ran (𝑧𝑎 ↦ ((𝑐 + 𝑧) 𝑐)))
9281, 82, 91syl2anc 692 . . . . . . . . . . . 12 (((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) → (𝑐 𝑎) = ran (𝑧𝑎 ↦ ((𝑐 + 𝑧) 𝑐)))
93 eqid 2621 . . . . . . . . . . . . 13 (𝑧𝑎 ↦ ((𝑐 + 𝑧) 𝑐)) = (𝑧𝑎 ↦ ((𝑐 + 𝑧) 𝑐))
9493rnmpt 5341 . . . . . . . . . . . 12 ran (𝑧𝑎 ↦ ((𝑐 + 𝑧) 𝑐)) = {𝑣 ∣ ∃𝑧𝑎 𝑣 = ((𝑐 + 𝑧) 𝑐)}
9592, 94syl6eq 2671 . . . . . . . . . . 11 (((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) → (𝑐 𝑎) = {𝑣 ∣ ∃𝑧𝑎 𝑣 = ((𝑐 + 𝑧) 𝑐)})
9695rexeqdv 3138 . . . . . . . . . 10 (((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) → (∃𝑤 ∈ (𝑐 𝑎)𝑢 = ((𝑏 + 𝑤) 𝑏) ↔ ∃𝑤 ∈ {𝑣 ∣ ∃𝑧𝑎 𝑣 = ((𝑐 + 𝑧) 𝑐)}𝑢 = ((𝑏 + 𝑤) 𝑏)))
9796abbidv 2738 . . . . . . . . 9 (((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) → {𝑢 ∣ ∃𝑤 ∈ (𝑐 𝑎)𝑢 = ((𝑏 + 𝑤) 𝑏)} = {𝑢 ∣ ∃𝑤 ∈ {𝑣 ∣ ∃𝑧𝑎 𝑣 = ((𝑐 + 𝑧) 𝑐)}𝑢 = ((𝑏 + 𝑤) 𝑏)})
9842adantr 481 . . . . . . . . . . . . . . 15 (((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) → 𝐺 ∈ Grp)
9998adantr 481 . . . . . . . . . . . . . 14 ((((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → 𝐺 ∈ Grp)
100 simprl 793 . . . . . . . . . . . . . . . . 17 (((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) → 𝑏𝑋)
1016, 13grpcl 17370 . . . . . . . . . . . . . . . . 17 ((𝐺 ∈ Grp ∧ 𝑏𝑋𝑐𝑋) → (𝑏 + 𝑐) ∈ 𝑋)
10298, 100, 81, 101syl3anc 1323 . . . . . . . . . . . . . . . 16 (((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) → (𝑏 + 𝑐) ∈ 𝑋)
103102adantr 481 . . . . . . . . . . . . . . 15 ((((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → (𝑏 + 𝑐) ∈ 𝑋)
10463adantlr 750 . . . . . . . . . . . . . . 15 ((((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → 𝑧𝑋)
1056, 13grpcl 17370 . . . . . . . . . . . . . . 15 ((𝐺 ∈ Grp ∧ (𝑏 + 𝑐) ∈ 𝑋𝑧𝑋) → ((𝑏 + 𝑐) + 𝑧) ∈ 𝑋)
10699, 103, 104, 105syl3anc 1323 . . . . . . . . . . . . . 14 ((((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → ((𝑏 + 𝑐) + 𝑧) ∈ 𝑋)
10781adantr 481 . . . . . . . . . . . . . 14 ((((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → 𝑐𝑋)
108100adantr 481 . . . . . . . . . . . . . 14 ((((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → 𝑏𝑋)
1096, 13, 14grpsubsub4 17448 . . . . . . . . . . . . . 14 ((𝐺 ∈ Grp ∧ (((𝑏 + 𝑐) + 𝑧) ∈ 𝑋𝑐𝑋𝑏𝑋)) → ((((𝑏 + 𝑐) + 𝑧) 𝑐) 𝑏) = (((𝑏 + 𝑐) + 𝑧) (𝑏 + 𝑐)))
11099, 106, 107, 108, 109syl13anc 1325 . . . . . . . . . . . . 13 ((((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → ((((𝑏 + 𝑐) + 𝑧) 𝑐) 𝑏) = (((𝑏 + 𝑐) + 𝑧) (𝑏 + 𝑐)))
1116, 13grpass 17371 . . . . . . . . . . . . . . . . 17 ((𝐺 ∈ Grp ∧ (𝑏𝑋𝑐𝑋𝑧𝑋)) → ((𝑏 + 𝑐) + 𝑧) = (𝑏 + (𝑐 + 𝑧)))
11299, 108, 107, 104, 111syl13anc 1325 . . . . . . . . . . . . . . . 16 ((((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → ((𝑏 + 𝑐) + 𝑧) = (𝑏 + (𝑐 + 𝑧)))
113112oveq1d 6630 . . . . . . . . . . . . . . 15 ((((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → (((𝑏 + 𝑐) + 𝑧) 𝑐) = ((𝑏 + (𝑐 + 𝑧)) 𝑐))
1146, 13grpcl 17370 . . . . . . . . . . . . . . . . 17 ((𝐺 ∈ Grp ∧ 𝑐𝑋𝑧𝑋) → (𝑐 + 𝑧) ∈ 𝑋)
11599, 107, 104, 114syl3anc 1323 . . . . . . . . . . . . . . . 16 ((((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → (𝑐 + 𝑧) ∈ 𝑋)
1166, 13, 14grpaddsubass 17445 . . . . . . . . . . . . . . . 16 ((𝐺 ∈ Grp ∧ (𝑏𝑋 ∧ (𝑐 + 𝑧) ∈ 𝑋𝑐𝑋)) → ((𝑏 + (𝑐 + 𝑧)) 𝑐) = (𝑏 + ((𝑐 + 𝑧) 𝑐)))
11799, 108, 115, 107, 116syl13anc 1325 . . . . . . . . . . . . . . 15 ((((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → ((𝑏 + (𝑐 + 𝑧)) 𝑐) = (𝑏 + ((𝑐 + 𝑧) 𝑐)))
118113, 117eqtrd 2655 . . . . . . . . . . . . . 14 ((((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → (((𝑏 + 𝑐) + 𝑧) 𝑐) = (𝑏 + ((𝑐 + 𝑧) 𝑐)))
119118oveq1d 6630 . . . . . . . . . . . . 13 ((((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → ((((𝑏 + 𝑐) + 𝑧) 𝑐) 𝑏) = ((𝑏 + ((𝑐 + 𝑧) 𝑐)) 𝑏))
120110, 119eqtr3d 2657 . . . . . . . . . . . 12 ((((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → (((𝑏 + 𝑐) + 𝑧) (𝑏 + 𝑐)) = ((𝑏 + ((𝑐 + 𝑧) 𝑐)) 𝑏))
121120eqeq2d 2631 . . . . . . . . . . 11 ((((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) ∧ 𝑧𝑎) → (𝑢 = (((𝑏 + 𝑐) + 𝑧) (𝑏 + 𝑐)) ↔ 𝑢 = ((𝑏 + ((𝑐 + 𝑧) 𝑐)) 𝑏)))
122121rexbidva 3044 . . . . . . . . . 10 (((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) → (∃𝑧𝑎 𝑢 = (((𝑏 + 𝑐) + 𝑧) (𝑏 + 𝑐)) ↔ ∃𝑧𝑎 𝑢 = ((𝑏 + ((𝑐 + 𝑧) 𝑐)) 𝑏)))
123122abbidv 2738 . . . . . . . . 9 (((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) → {𝑢 ∣ ∃𝑧𝑎 𝑢 = (((𝑏 + 𝑐) + 𝑧) (𝑏 + 𝑐))} = {𝑢 ∣ ∃𝑧𝑎 𝑢 = ((𝑏 + ((𝑐 + 𝑧) 𝑐)) 𝑏)})
12480, 97, 1233eqtr4a 2681 . . . . . . . 8 (((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) → {𝑢 ∣ ∃𝑤 ∈ (𝑐 𝑎)𝑢 = ((𝑏 + 𝑤) 𝑏)} = {𝑢 ∣ ∃𝑧𝑎 𝑢 = (((𝑏 + 𝑐) + 𝑧) (𝑏 + 𝑐))})
125 eqid 2621 . . . . . . . . 9 (𝑤 ∈ (𝑐 𝑎) ↦ ((𝑏 + 𝑤) 𝑏)) = (𝑤 ∈ (𝑐 𝑎) ↦ ((𝑏 + 𝑤) 𝑏))
126125rnmpt 5341 . . . . . . . 8 ran (𝑤 ∈ (𝑐 𝑎) ↦ ((𝑏 + 𝑤) 𝑏)) = {𝑢 ∣ ∃𝑤 ∈ (𝑐 𝑎)𝑢 = ((𝑏 + 𝑤) 𝑏)}
127 eqid 2621 . . . . . . . . 9 (𝑧𝑎 ↦ (((𝑏 + 𝑐) + 𝑧) (𝑏 + 𝑐))) = (𝑧𝑎 ↦ (((𝑏 + 𝑐) + 𝑧) (𝑏 + 𝑐)))
128127rnmpt 5341 . . . . . . . 8 ran (𝑧𝑎 ↦ (((𝑏 + 𝑐) + 𝑧) (𝑏 + 𝑐))) = {𝑢 ∣ ∃𝑧𝑎 𝑢 = (((𝑏 + 𝑐) + 𝑧) (𝑏 + 𝑐))}
129124, 126, 1283eqtr4g 2680 . . . . . . 7 (((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) → ran (𝑤 ∈ (𝑐 𝑎) ↦ ((𝑏 + 𝑤) 𝑏)) = ran (𝑧𝑎 ↦ (((𝑏 + 𝑐) + 𝑧) (𝑏 + 𝑐))))
13041ad2antrr 761 . . . . . . . . 9 (((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) → :(𝑋 × (𝑃 pSyl 𝐺))⟶(𝑃 pSyl 𝐺))
131130, 81, 82fovrnd 6771 . . . . . . . 8 (((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) → (𝑐 𝑎) ∈ (𝑃 pSyl 𝐺))
132 simpr 477 . . . . . . . . . . . 12 ((𝑥 = 𝑏𝑦 = (𝑐 𝑎)) → 𝑦 = (𝑐 𝑎))
133 simpl 473 . . . . . . . . . . . . . 14 ((𝑥 = 𝑏𝑦 = (𝑐 𝑎)) → 𝑥 = 𝑏)
134133oveq1d 6630 . . . . . . . . . . . . 13 ((𝑥 = 𝑏𝑦 = (𝑐 𝑎)) → (𝑥 + 𝑧) = (𝑏 + 𝑧))
135134, 133oveq12d 6633 . . . . . . . . . . . 12 ((𝑥 = 𝑏𝑦 = (𝑐 𝑎)) → ((𝑥 + 𝑧) 𝑥) = ((𝑏 + 𝑧) 𝑏))
136132, 135mpteq12dv 4703 . . . . . . . . . . 11 ((𝑥 = 𝑏𝑦 = (𝑐 𝑎)) → (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)) = (𝑧 ∈ (𝑐 𝑎) ↦ ((𝑏 + 𝑧) 𝑏)))
137 oveq2 6623 . . . . . . . . . . . . 13 (𝑧 = 𝑤 → (𝑏 + 𝑧) = (𝑏 + 𝑤))
138137oveq1d 6630 . . . . . . . . . . . 12 (𝑧 = 𝑤 → ((𝑏 + 𝑧) 𝑏) = ((𝑏 + 𝑤) 𝑏))
139138cbvmptv 4720 . . . . . . . . . . 11 (𝑧 ∈ (𝑐 𝑎) ↦ ((𝑏 + 𝑧) 𝑏)) = (𝑤 ∈ (𝑐 𝑎) ↦ ((𝑏 + 𝑤) 𝑏))
140136, 139syl6eq 2671 . . . . . . . . . 10 ((𝑥 = 𝑏𝑦 = (𝑐 𝑎)) → (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)) = (𝑤 ∈ (𝑐 𝑎) ↦ ((𝑏 + 𝑤) 𝑏)))
141140rneqd 5323 . . . . . . . . 9 ((𝑥 = 𝑏𝑦 = (𝑐 𝑎)) → ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)) = ran (𝑤 ∈ (𝑐 𝑎) ↦ ((𝑏 + 𝑤) 𝑏)))
142 ovex 6643 . . . . . . . . . . 11 (𝑐 𝑎) ∈ V
143142mptex 6451 . . . . . . . . . 10 (𝑤 ∈ (𝑐 𝑎) ↦ ((𝑏 + 𝑤) 𝑏)) ∈ V
144143rnex 7062 . . . . . . . . 9 ran (𝑤 ∈ (𝑐 𝑎) ↦ ((𝑏 + 𝑤) 𝑏)) ∈ V
145141, 39, 144ovmpt2a 6756 . . . . . . . 8 ((𝑏𝑋 ∧ (𝑐 𝑎) ∈ (𝑃 pSyl 𝐺)) → (𝑏 (𝑐 𝑎)) = ran (𝑤 ∈ (𝑐 𝑎) ↦ ((𝑏 + 𝑤) 𝑏)))
146100, 131, 145syl2anc 692 . . . . . . 7 (((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) → (𝑏 (𝑐 𝑎)) = ran (𝑤 ∈ (𝑐 𝑎) ↦ ((𝑏 + 𝑤) 𝑏)))
147 simpr 477 . . . . . . . . . . 11 ((𝑥 = (𝑏 + 𝑐) ∧ 𝑦 = 𝑎) → 𝑦 = 𝑎)
148 simpl 473 . . . . . . . . . . . . 13 ((𝑥 = (𝑏 + 𝑐) ∧ 𝑦 = 𝑎) → 𝑥 = (𝑏 + 𝑐))
149148oveq1d 6630 . . . . . . . . . . . 12 ((𝑥 = (𝑏 + 𝑐) ∧ 𝑦 = 𝑎) → (𝑥 + 𝑧) = ((𝑏 + 𝑐) + 𝑧))
150149, 148oveq12d 6633 . . . . . . . . . . 11 ((𝑥 = (𝑏 + 𝑐) ∧ 𝑦 = 𝑎) → ((𝑥 + 𝑧) 𝑥) = (((𝑏 + 𝑐) + 𝑧) (𝑏 + 𝑐)))
151147, 150mpteq12dv 4703 . . . . . . . . . 10 ((𝑥 = (𝑏 + 𝑐) ∧ 𝑦 = 𝑎) → (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)) = (𝑧𝑎 ↦ (((𝑏 + 𝑐) + 𝑧) (𝑏 + 𝑐))))
152151rneqd 5323 . . . . . . . . 9 ((𝑥 = (𝑏 + 𝑐) ∧ 𝑦 = 𝑎) → ran (𝑧𝑦 ↦ ((𝑥 + 𝑧) 𝑥)) = ran (𝑧𝑎 ↦ (((𝑏 + 𝑐) + 𝑧) (𝑏 + 𝑐))))
15353mptex 6451 . . . . . . . . . 10 (𝑧𝑎 ↦ (((𝑏 + 𝑐) + 𝑧) (𝑏 + 𝑐))) ∈ V
154153rnex 7062 . . . . . . . . 9 ran (𝑧𝑎 ↦ (((𝑏 + 𝑐) + 𝑧) (𝑏 + 𝑐))) ∈ V
155152, 39, 154ovmpt2a 6756 . . . . . . . 8 (((𝑏 + 𝑐) ∈ 𝑋𝑎 ∈ (𝑃 pSyl 𝐺)) → ((𝑏 + 𝑐) 𝑎) = ran (𝑧𝑎 ↦ (((𝑏 + 𝑐) + 𝑧) (𝑏 + 𝑐))))
156102, 82, 155syl2anc 692 . . . . . . 7 (((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) → ((𝑏 + 𝑐) 𝑎) = ran (𝑧𝑎 ↦ (((𝑏 + 𝑐) + 𝑧) (𝑏 + 𝑐))))
157129, 146, 1563eqtr4rd 2666 . . . . . 6 (((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) ∧ (𝑏𝑋𝑐𝑋)) → ((𝑏 + 𝑐) 𝑎) = (𝑏 (𝑐 𝑎)))
158157ralrimivva 2967 . . . . 5 ((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) → ∀𝑏𝑋𝑐𝑋 ((𝑏 + 𝑐) 𝑎) = (𝑏 (𝑐 𝑎)))
15976, 158jca 554 . . . 4 ((𝜑𝑎 ∈ (𝑃 pSyl 𝐺)) → (((0g𝐺) 𝑎) = 𝑎 ∧ ∀𝑏𝑋𝑐𝑋 ((𝑏 + 𝑐) 𝑎) = (𝑏 (𝑐 𝑎))))
160159ralrimiva 2962 . . 3 (𝜑 → ∀𝑎 ∈ (𝑃 pSyl 𝐺)(((0g𝐺) 𝑎) = 𝑎 ∧ ∀𝑏𝑋𝑐𝑋 ((𝑏 + 𝑐) 𝑎) = (𝑏 (𝑐 𝑎))))
16141, 160jca 554 . 2 (𝜑 → ( :(𝑋 × (𝑃 pSyl 𝐺))⟶(𝑃 pSyl 𝐺) ∧ ∀𝑎 ∈ (𝑃 pSyl 𝐺)(((0g𝐺) 𝑎) = 𝑎 ∧ ∀𝑏𝑋𝑐𝑋 ((𝑏 + 𝑐) 𝑎) = (𝑏 (𝑐 𝑎)))))
1626, 13, 43isga 17664 . 2 ( ∈ (𝐺 GrpAct (𝑃 pSyl 𝐺)) ↔ ((𝐺 ∈ Grp ∧ (𝑃 pSyl 𝐺) ∈ V) ∧ ( :(𝑋 × (𝑃 pSyl 𝐺))⟶(𝑃 pSyl 𝐺) ∧ ∀𝑎 ∈ (𝑃 pSyl 𝐺)(((0g𝐺) 𝑎) = 𝑎 ∧ ∀𝑏𝑋𝑐𝑋 ((𝑏 + 𝑐) 𝑎) = (𝑏 (𝑐 𝑎))))))
1633, 161, 162sylanbrc 697 1 (𝜑 ∈ (𝐺 GrpAct (𝑃 pSyl 𝐺)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384   = wceq 1480  wcel 1987  {cab 2607  wral 2908  wrex 2909  Vcvv 3190  wss 3560   class class class wbr 4623  cmpt 4683   I cid 4994   × cxp 5082  ran crn 5085  cres 5086  wf 5853  cfv 5857  (class class class)co 6615  cmpt2 6617  cen 7912  Fincfn 7915  cexp 12816  #chash 13073  cprime 15328   pCnt cpc 15484  Basecbs 15800  +gcplusg 15881  0gc0g 16040  Grpcgrp 17362  -gcsg 17364  SubGrpcsubg 17528   GrpAct cga 17662   pSyl cslw 17887
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-8 1989  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-rep 4741  ax-sep 4751  ax-nul 4759  ax-pow 4813  ax-pr 4877  ax-un 6914  ax-inf2 8498  ax-cnex 9952  ax-resscn 9953  ax-1cn 9954  ax-icn 9955  ax-addcl 9956  ax-addrcl 9957  ax-mulcl 9958  ax-mulrcl 9959  ax-mulcom 9960  ax-addass 9961  ax-mulass 9962  ax-distr 9963  ax-i2m1 9964  ax-1ne0 9965  ax-1rid 9966  ax-rnegex 9967  ax-rrecex 9968  ax-cnre 9969  ax-pre-lttri 9970  ax-pre-lttrn 9971  ax-pre-ltadd 9972  ax-pre-mulgt0 9973  ax-pre-sup 9974
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-fal 1486  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ne 2791  df-nel 2894  df-ral 2913  df-rex 2914  df-reu 2915  df-rmo 2916  df-rab 2917  df-v 3192  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-pss 3576  df-nul 3898  df-if 4065  df-pw 4138  df-sn 4156  df-pr 4158  df-tp 4160  df-op 4162  df-uni 4410  df-int 4448  df-iun 4494  df-disj 4594  df-br 4624  df-opab 4684  df-mpt 4685  df-tr 4723  df-eprel 4995  df-id 4999  df-po 5005  df-so 5006  df-fr 5043  df-se 5044  df-we 5045  df-xp 5090  df-rel 5091  df-cnv 5092  df-co 5093  df-dm 5094  df-rn 5095  df-res 5096  df-ima 5097  df-pred 5649  df-ord 5695  df-on 5696  df-lim 5697  df-suc 5698  df-iota 5820  df-fun 5859  df-fn 5860  df-f 5861  df-f1 5862  df-fo 5863  df-f1o 5864  df-fv 5865  df-isom 5866  df-riota 6576  df-ov 6618  df-oprab 6619  df-mpt2 6620  df-om 7028  df-1st 7128  df-2nd 7129  df-wrecs 7367  df-recs 7428  df-rdg 7466  df-1o 7520  df-2o 7521  df-oadd 7524  df-omul 7525  df-er 7702  df-ec 7704  df-qs 7708  df-map 7819  df-en 7916  df-dom 7917  df-sdom 7918  df-fin 7919  df-sup 8308  df-inf 8309  df-oi 8375  df-card 8725  df-acn 8728  df-cda 8950  df-pnf 10036  df-mnf 10037  df-xr 10038  df-ltxr 10039  df-le 10040  df-sub 10228  df-neg 10229  df-div 10645  df-nn 10981  df-2 11039  df-3 11040  df-n0 11253  df-xnn0 11324  df-z 11338  df-uz 11648  df-q 11749  df-rp 11793  df-fz 12285  df-fzo 12423  df-fl 12549  df-mod 12625  df-seq 12758  df-exp 12817  df-fac 13017  df-bc 13046  df-hash 13074  df-cj 13789  df-re 13790  df-im 13791  df-sqrt 13925  df-abs 13926  df-clim 14169  df-sum 14367  df-dvds 14927  df-gcd 15160  df-prm 15329  df-pc 15485  df-ndx 15803  df-slot 15804  df-base 15805  df-sets 15806  df-ress 15807  df-plusg 15894  df-0g 16042  df-mgm 17182  df-sgrp 17224  df-mnd 17235  df-submnd 17276  df-grp 17365  df-minusg 17366  df-sbg 17367  df-mulg 17481  df-subg 17531  df-eqg 17533  df-ghm 17598  df-ga 17663  df-od 17888  df-pgp 17890  df-slw 17891
This theorem is referenced by:  sylow3lem3  17984  sylow3lem5  17986
  Copyright terms: Public domain W3C validator