MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ablfaclem3 Structured version   Visualization version   GIF version
Theorem ablfaclem3 20048
Description: Lemma for ablfac 20049. (Contributed by Mario Carneiro, 27-Apr-2016.) (Revised by Mario Carneiro, 3-May-2016.)
Hypotheses
Ref Expression
ablfac.b 𝐡 = (Baseβ€˜πΊ)
ablfac.c 𝐢 = {π‘Ÿ ∈ (SubGrpβ€˜πΊ) ∣ (𝐺 β†Ύs π‘Ÿ) ∈ (CycGrp ∩ ran pGrp )}
ablfac.1 (πœ‘ β†’ 𝐺 ∈ Abel)
ablfac.2 (πœ‘ β†’ 𝐡 ∈ Fin)
ablfac.o 𝑂 = (odβ€˜πΊ)
ablfac.a 𝐴 = {𝑀 ∈ β„™ ∣ 𝑀 βˆ₯ (β™―β€˜π΅)}
ablfac.s 𝑆 = (𝑝 ∈ 𝐴 ↦ {π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ (𝑝↑(𝑝 pCnt (β™―β€˜π΅)))})
ablfac.w π‘Š = (𝑔 ∈ (SubGrpβ€˜πΊ) ↦ {𝑠 ∈ Word 𝐢 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑔)})
Assertion
Ref Expression
ablfaclem3 (πœ‘ β†’ (π‘Šβ€˜π΅) β‰  βˆ…)
Distinct variable groups:   𝑠,𝑝,π‘₯,𝐴   𝑔,π‘Ÿ,𝑠,𝑆   𝑔,𝑝,𝑀,π‘₯,𝐡,π‘Ÿ,𝑠   𝑂,𝑝,π‘₯   𝐢,𝑔,𝑝,𝑠,𝑀,π‘₯   π‘Š,𝑝,𝑀,π‘₯   πœ‘,𝑝,𝑠,𝑀,π‘₯   𝑔,𝐺,𝑝,π‘Ÿ,𝑠,𝑀,π‘₯
Allowed substitution hints:   πœ‘(𝑔,π‘Ÿ)   𝐴(𝑀,𝑔,π‘Ÿ)   𝐢(π‘Ÿ)   𝑆(π‘₯,𝑀,𝑝)   𝑂(𝑀,𝑔,𝑠,π‘Ÿ)   π‘Š(𝑔,𝑠,π‘Ÿ)
Proof of Theorem ablfaclem3
Dummy variables π‘Ž 𝑏 𝑐 𝑓 β„Ž π‘ž 𝑑 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fzfid 13970 . . . 4 (πœ‘ β†’ (1...(β™―β€˜π΅)) ∈ Fin)
2 ablfac.a . . . . 5 𝐴 = {𝑀 ∈ β„™ ∣ 𝑀 βˆ₯ (β™―β€˜π΅)}
3 prmnn 16644 . . . . . . . 8 (𝑀 ∈ β„™ β†’ 𝑀 ∈ β„•)
433ad2ant2 1131 . . . . . . 7 ((πœ‘ ∧ 𝑀 ∈ β„™ ∧ 𝑀 βˆ₯ (β™―β€˜π΅)) β†’ 𝑀 ∈ β„•)
5 prmz 16645 . . . . . . . . 9 (𝑀 ∈ β„™ β†’ 𝑀 ∈ β„€)
6 ablfac.1 . . . . . . . . . . 11 (πœ‘ β†’ 𝐺 ∈ Abel)
7 ablgrp 19744 . . . . . . . . . . 11 (𝐺 ∈ Abel β†’ 𝐺 ∈ Grp)
8 ablfac.b . . . . . . . . . . . 12 𝐡 = (Baseβ€˜πΊ)
98grpbn0 18927 . . . . . . . . . . 11 (𝐺 ∈ Grp β†’ 𝐡 β‰  βˆ…)
106, 7, 93syl 18 . . . . . . . . . 10 (πœ‘ β†’ 𝐡 β‰  βˆ…)
11 ablfac.2 . . . . . . . . . . 11 (πœ‘ β†’ 𝐡 ∈ Fin)
12 hashnncl 14357 . . . . . . . . . . 11 (𝐡 ∈ Fin β†’ ((β™―β€˜π΅) ∈ β„• ↔ 𝐡 β‰  βˆ…))
1311, 12syl 17 . . . . . . . . . 10 (πœ‘ β†’ ((β™―β€˜π΅) ∈ β„• ↔ 𝐡 β‰  βˆ…))
1410, 13mpbird 256 . . . . . . . . 9 (πœ‘ β†’ (β™―β€˜π΅) ∈ β„•)
15 dvdsle 16286 . . . . . . . . 9 ((𝑀 ∈ β„€ ∧ (β™―β€˜π΅) ∈ β„•) β†’ (𝑀 βˆ₯ (β™―β€˜π΅) β†’ 𝑀 ≀ (β™―β€˜π΅)))
165, 14, 15syl2anr 595 . . . . . . . 8 ((πœ‘ ∧ 𝑀 ∈ β„™) β†’ (𝑀 βˆ₯ (β™―β€˜π΅) β†’ 𝑀 ≀ (β™―β€˜π΅)))
17163impia 1114 . . . . . . 7 ((πœ‘ ∧ 𝑀 ∈ β„™ ∧ 𝑀 βˆ₯ (β™―β€˜π΅)) β†’ 𝑀 ≀ (β™―β€˜π΅))
1814nnzd 12615 . . . . . . . . 9 (πœ‘ β†’ (β™―β€˜π΅) ∈ β„€)
19183ad2ant1 1130 . . . . . . . 8 ((πœ‘ ∧ 𝑀 ∈ β„™ ∧ 𝑀 βˆ₯ (β™―β€˜π΅)) β†’ (β™―β€˜π΅) ∈ β„€)
20 fznn 13601 . . . . . . . 8 ((β™―β€˜π΅) ∈ β„€ β†’ (𝑀 ∈ (1...(β™―β€˜π΅)) ↔ (𝑀 ∈ β„• ∧ 𝑀 ≀ (β™―β€˜π΅))))
2119, 20syl 17 . . . . . . 7 ((πœ‘ ∧ 𝑀 ∈ β„™ ∧ 𝑀 βˆ₯ (β™―β€˜π΅)) β†’ (𝑀 ∈ (1...(β™―β€˜π΅)) ↔ (𝑀 ∈ β„• ∧ 𝑀 ≀ (β™―β€˜π΅))))
224, 17, 21mpbir2and 711 . . . . . 6 ((πœ‘ ∧ 𝑀 ∈ β„™ ∧ 𝑀 βˆ₯ (β™―β€˜π΅)) β†’ 𝑀 ∈ (1...(β™―β€˜π΅)))
2322rabssdv 4064 . . . . 5 (πœ‘ β†’ {𝑀 ∈ β„™ ∣ 𝑀 βˆ₯ (β™―β€˜π΅)} βŠ† (1...(β™―β€˜π΅)))
242, 23eqsstrid 4021 . . . 4 (πœ‘ β†’ 𝐴 βŠ† (1...(β™―β€˜π΅)))
251, 24ssfid 9290 . . 3 (πœ‘ β†’ 𝐴 ∈ Fin)
26 dfin5 3947 . . . . . . . 8 (Word 𝐢 ∩ (π‘Šβ€˜(π‘†β€˜π‘ž))) = {𝑦 ∈ Word 𝐢 ∣ 𝑦 ∈ (π‘Šβ€˜(π‘†β€˜π‘ž))}
27 ablfac.o . . . . . . . . . . . . . 14 𝑂 = (odβ€˜πΊ)
28 ablfac.s . . . . . . . . . . . . . 14 𝑆 = (𝑝 ∈ 𝐴 ↦ {π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ (𝑝↑(𝑝 pCnt (β™―β€˜π΅)))})
292ssrab3 4072 . . . . . . . . . . . . . . 15 𝐴 βŠ† β„™
3029a1i 11 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝐴 βŠ† β„™)
318, 27, 28, 6, 11, 30ablfac1b 20031 . . . . . . . . . . . . 13 (πœ‘ β†’ 𝐺dom DProd 𝑆)
328fvexi 6906 . . . . . . . . . . . . . . . 16 𝐡 ∈ V
3332rabex 5329 . . . . . . . . . . . . . . 15 {π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ (𝑝↑(𝑝 pCnt (β™―β€˜π΅)))} ∈ V
3433, 28dmmpti 6694 . . . . . . . . . . . . . 14 dom 𝑆 = 𝐴
3534a1i 11 . . . . . . . . . . . . 13 (πœ‘ β†’ dom 𝑆 = 𝐴)
3631, 35dprdf2 19968 . . . . . . . . . . . 12 (πœ‘ β†’ 𝑆:𝐴⟢(SubGrpβ€˜πΊ))
3736ffvelcdmda 7089 . . . . . . . . . . 11 ((πœ‘ ∧ π‘ž ∈ 𝐴) β†’ (π‘†β€˜π‘ž) ∈ (SubGrpβ€˜πΊ))
38 ablfac.c . . . . . . . . . . . 12 𝐢 = {π‘Ÿ ∈ (SubGrpβ€˜πΊ) ∣ (𝐺 β†Ύs π‘Ÿ) ∈ (CycGrp ∩ ran pGrp )}
39 ablfac.w . . . . . . . . . . . 12 π‘Š = (𝑔 ∈ (SubGrpβ€˜πΊ) ↦ {𝑠 ∈ Word 𝐢 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑔)})
408, 38, 6, 11, 27, 2, 28, 39ablfaclem1 20046 . . . . . . . . . . 11 ((π‘†β€˜π‘ž) ∈ (SubGrpβ€˜πΊ) β†’ (π‘Šβ€˜(π‘†β€˜π‘ž)) = {𝑠 ∈ Word 𝐢 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (π‘†β€˜π‘ž))})
4137, 40syl 17 . . . . . . . . . 10 ((πœ‘ ∧ π‘ž ∈ 𝐴) β†’ (π‘Šβ€˜(π‘†β€˜π‘ž)) = {𝑠 ∈ Word 𝐢 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (π‘†β€˜π‘ž))})
42 ssrab2 4069 . . . . . . . . . 10 {𝑠 ∈ Word 𝐢 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (π‘†β€˜π‘ž))} βŠ† Word 𝐢
4341, 42eqsstrdi 4027 . . . . . . . . 9 ((πœ‘ ∧ π‘ž ∈ 𝐴) β†’ (π‘Šβ€˜(π‘†β€˜π‘ž)) βŠ† Word 𝐢)
44 sseqin2 4209 . . . . . . . . 9 ((π‘Šβ€˜(π‘†β€˜π‘ž)) βŠ† Word 𝐢 ↔ (Word 𝐢 ∩ (π‘Šβ€˜(π‘†β€˜π‘ž))) = (π‘Šβ€˜(π‘†β€˜π‘ž)))
4543, 44sylib 217 . . . . . . . 8 ((πœ‘ ∧ π‘ž ∈ 𝐴) β†’ (Word 𝐢 ∩ (π‘Šβ€˜(π‘†β€˜π‘ž))) = (π‘Šβ€˜(π‘†β€˜π‘ž)))
4626, 45eqtr3id 2779 . . . . . . 7 ((πœ‘ ∧ π‘ž ∈ 𝐴) β†’ {𝑦 ∈ Word 𝐢 ∣ 𝑦 ∈ (π‘Šβ€˜(π‘†β€˜π‘ž))} = (π‘Šβ€˜(π‘†β€˜π‘ž)))
4746, 41eqtrd 2765 . . . . . 6 ((πœ‘ ∧ π‘ž ∈ 𝐴) β†’ {𝑦 ∈ Word 𝐢 ∣ 𝑦 ∈ (π‘Šβ€˜(π‘†β€˜π‘ž))} = {𝑠 ∈ Word 𝐢 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (π‘†β€˜π‘ž))})
48 eqid 2725 . . . . . . . . 9 (Baseβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž))) = (Baseβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž)))
49 eqid 2725 . . . . . . . . 9 {π‘Ÿ ∈ (SubGrpβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž))) ∣ ((𝐺 β†Ύs (π‘†β€˜π‘ž)) β†Ύs π‘Ÿ) ∈ (CycGrp ∩ ran pGrp )} = {π‘Ÿ ∈ (SubGrpβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž))) ∣ ((𝐺 β†Ύs (π‘†β€˜π‘ž)) β†Ύs π‘Ÿ) ∈ (CycGrp ∩ ran pGrp )}
50 eqid 2725 . . . . . . . . . . 11 (𝐺 β†Ύs (π‘†β€˜π‘ž)) = (𝐺 β†Ύs (π‘†β€˜π‘ž))
5150subgabl 19795 . . . . . . . . . 10 ((𝐺 ∈ Abel ∧ (π‘†β€˜π‘ž) ∈ (SubGrpβ€˜πΊ)) β†’ (𝐺 β†Ύs (π‘†β€˜π‘ž)) ∈ Abel)
526, 37, 51syl2an2r 683 . . . . . . . . 9 ((πœ‘ ∧ π‘ž ∈ 𝐴) β†’ (𝐺 β†Ύs (π‘†β€˜π‘ž)) ∈ Abel)
5330sselda 3972 . . . . . . . . . 10 ((πœ‘ ∧ π‘ž ∈ 𝐴) β†’ π‘ž ∈ β„™)
5450subgbas 19089 . . . . . . . . . . . . . 14 ((π‘†β€˜π‘ž) ∈ (SubGrpβ€˜πΊ) β†’ (π‘†β€˜π‘ž) = (Baseβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž))))
5537, 54syl 17 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘ž ∈ 𝐴) β†’ (π‘†β€˜π‘ž) = (Baseβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž))))
5655fveq2d 6896 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘ž ∈ 𝐴) β†’ (β™―β€˜(π‘†β€˜π‘ž)) = (β™―β€˜(Baseβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž)))))
578, 27, 28, 6, 11, 30ablfac1a 20030 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘ž ∈ 𝐴) β†’ (β™―β€˜(π‘†β€˜π‘ž)) = (π‘žβ†‘(π‘ž pCnt (β™―β€˜π΅))))
5856, 57eqtr3d 2767 . . . . . . . . . . 11 ((πœ‘ ∧ π‘ž ∈ 𝐴) β†’ (β™―β€˜(Baseβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž)))) = (π‘žβ†‘(π‘ž pCnt (β™―β€˜π΅))))
5958oveq2d 7432 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘ž ∈ 𝐴) β†’ (π‘ž pCnt (β™―β€˜(Baseβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž))))) = (π‘ž pCnt (π‘žβ†‘(π‘ž pCnt (β™―β€˜π΅)))))
6014adantr 479 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ π‘ž ∈ 𝐴) β†’ (β™―β€˜π΅) ∈ β„•)
6153, 60pccld 16818 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ π‘ž ∈ 𝐴) β†’ (π‘ž pCnt (β™―β€˜π΅)) ∈ β„•0)
6261nn0zd 12614 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘ž ∈ 𝐴) β†’ (π‘ž pCnt (β™―β€˜π΅)) ∈ β„€)
63 pcid 16841 . . . . . . . . . . . . . 14 ((π‘ž ∈ β„™ ∧ (π‘ž pCnt (β™―β€˜π΅)) ∈ β„€) β†’ (π‘ž pCnt (π‘žβ†‘(π‘ž pCnt (β™―β€˜π΅)))) = (π‘ž pCnt (β™―β€˜π΅)))
6453, 62, 63syl2anc 582 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘ž ∈ 𝐴) β†’ (π‘ž pCnt (π‘žβ†‘(π‘ž pCnt (β™―β€˜π΅)))) = (π‘ž pCnt (β™―β€˜π΅)))
6559, 64eqtrd 2765 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘ž ∈ 𝐴) β†’ (π‘ž pCnt (β™―β€˜(Baseβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž))))) = (π‘ž pCnt (β™―β€˜π΅)))
6665oveq2d 7432 . . . . . . . . . . 11 ((πœ‘ ∧ π‘ž ∈ 𝐴) β†’ (π‘žβ†‘(π‘ž pCnt (β™―β€˜(Baseβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž)))))) = (π‘žβ†‘(π‘ž pCnt (β™―β€˜π΅))))
6758, 66eqtr4d 2768 . . . . . . . . . 10 ((πœ‘ ∧ π‘ž ∈ 𝐴) β†’ (β™―β€˜(Baseβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž)))) = (π‘žβ†‘(π‘ž pCnt (β™―β€˜(Baseβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž)))))))
6850subggrp 19088 . . . . . . . . . . . 12 ((π‘†β€˜π‘ž) ∈ (SubGrpβ€˜πΊ) β†’ (𝐺 β†Ύs (π‘†β€˜π‘ž)) ∈ Grp)
6937, 68syl 17 . . . . . . . . . . 11 ((πœ‘ ∧ π‘ž ∈ 𝐴) β†’ (𝐺 β†Ύs (π‘†β€˜π‘ž)) ∈ Grp)
7011adantr 479 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘ž ∈ 𝐴) β†’ 𝐡 ∈ Fin)
718subgss 19086 . . . . . . . . . . . . . 14 ((π‘†β€˜π‘ž) ∈ (SubGrpβ€˜πΊ) β†’ (π‘†β€˜π‘ž) βŠ† 𝐡)
7237, 71syl 17 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘ž ∈ 𝐴) β†’ (π‘†β€˜π‘ž) βŠ† 𝐡)
7370, 72ssfid 9290 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘ž ∈ 𝐴) β†’ (π‘†β€˜π‘ž) ∈ Fin)
7455, 73eqeltrrd 2826 . . . . . . . . . . 11 ((πœ‘ ∧ π‘ž ∈ 𝐴) β†’ (Baseβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž))) ∈ Fin)
7548pgpfi2 19565 . . . . . . . . . . 11 (((𝐺 β†Ύs (π‘†β€˜π‘ž)) ∈ Grp ∧ (Baseβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž))) ∈ Fin) β†’ (π‘ž pGrp (𝐺 β†Ύs (π‘†β€˜π‘ž)) ↔ (π‘ž ∈ β„™ ∧ (β™―β€˜(Baseβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž)))) = (π‘žβ†‘(π‘ž pCnt (β™―β€˜(Baseβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž)))))))))
7669, 74, 75syl2anc 582 . . . . . . . . . 10 ((πœ‘ ∧ π‘ž ∈ 𝐴) β†’ (π‘ž pGrp (𝐺 β†Ύs (π‘†β€˜π‘ž)) ↔ (π‘ž ∈ β„™ ∧ (β™―β€˜(Baseβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž)))) = (π‘žβ†‘(π‘ž pCnt (β™―β€˜(Baseβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž)))))))))
7753, 67, 76mpbir2and 711 . . . . . . . . 9 ((πœ‘ ∧ π‘ž ∈ 𝐴) β†’ π‘ž pGrp (𝐺 β†Ύs (π‘†β€˜π‘ž)))
7848, 49, 52, 77, 74pgpfac 20045 . . . . . . . 8 ((πœ‘ ∧ π‘ž ∈ 𝐴) β†’ βˆƒπ‘  ∈ Word {π‘Ÿ ∈ (SubGrpβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž))) ∣ ((𝐺 β†Ύs (π‘†β€˜π‘ž)) β†Ύs π‘Ÿ) ∈ (CycGrp ∩ ran pGrp )} ((𝐺 β†Ύs (π‘†β€˜π‘ž))dom DProd 𝑠 ∧ ((𝐺 β†Ύs (π‘†β€˜π‘ž)) DProd 𝑠) = (Baseβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž)))))
79 ssrab2 4069 . . . . . . . . . . . . . 14 {π‘Ÿ ∈ (SubGrpβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž))) ∣ ((𝐺 β†Ύs (π‘†β€˜π‘ž)) β†Ύs π‘Ÿ) ∈ (CycGrp ∩ ran pGrp )} βŠ† (SubGrpβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž)))
80 sswrd 14504 . . . . . . . . . . . . . 14 ({π‘Ÿ ∈ (SubGrpβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž))) ∣ ((𝐺 β†Ύs (π‘†β€˜π‘ž)) β†Ύs π‘Ÿ) ∈ (CycGrp ∩ ran pGrp )} βŠ† (SubGrpβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž))) β†’ Word {π‘Ÿ ∈ (SubGrpβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž))) ∣ ((𝐺 β†Ύs (π‘†β€˜π‘ž)) β†Ύs π‘Ÿ) ∈ (CycGrp ∩ ran pGrp )} βŠ† Word (SubGrpβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž))))
8179, 80ax-mp 5 . . . . . . . . . . . . 13 Word {π‘Ÿ ∈ (SubGrpβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž))) ∣ ((𝐺 β†Ύs (π‘†β€˜π‘ž)) β†Ύs π‘Ÿ) ∈ (CycGrp ∩ ran pGrp )} βŠ† Word (SubGrpβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž)))
8281sseli 3968 . . . . . . . . . . . 12 (𝑠 ∈ Word {π‘Ÿ ∈ (SubGrpβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž))) ∣ ((𝐺 β†Ύs (π‘†β€˜π‘ž)) β†Ύs π‘Ÿ) ∈ (CycGrp ∩ ran pGrp )} β†’ 𝑠 ∈ Word (SubGrpβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž))))
8337adantr 479 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ π‘ž ∈ 𝐴) ∧ 𝑠 ∈ Word (SubGrpβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž)))) β†’ (π‘†β€˜π‘ž) ∈ (SubGrpβ€˜πΊ))
8483adantr 479 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ π‘ž ∈ 𝐴) ∧ 𝑠 ∈ Word (SubGrpβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž)))) ∧ (𝐺 β†Ύs (π‘†β€˜π‘ž))dom DProd 𝑠) β†’ (π‘†β€˜π‘ž) ∈ (SubGrpβ€˜πΊ))
8550subgdmdprd 19995 . . . . . . . . . . . . . . . . . . 19 ((π‘†β€˜π‘ž) ∈ (SubGrpβ€˜πΊ) β†’ ((𝐺 β†Ύs (π‘†β€˜π‘ž))dom DProd 𝑠 ↔ (𝐺dom DProd 𝑠 ∧ ran 𝑠 βŠ† 𝒫 (π‘†β€˜π‘ž))))
8683, 85syl 17 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ π‘ž ∈ 𝐴) ∧ 𝑠 ∈ Word (SubGrpβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž)))) β†’ ((𝐺 β†Ύs (π‘†β€˜π‘ž))dom DProd 𝑠 ↔ (𝐺dom DProd 𝑠 ∧ ran 𝑠 βŠ† 𝒫 (π‘†β€˜π‘ž))))
8786simprbda 497 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ π‘ž ∈ 𝐴) ∧ 𝑠 ∈ Word (SubGrpβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž)))) ∧ (𝐺 β†Ύs (π‘†β€˜π‘ž))dom DProd 𝑠) β†’ 𝐺dom DProd 𝑠)
8886simplbda 498 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ π‘ž ∈ 𝐴) ∧ 𝑠 ∈ Word (SubGrpβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž)))) ∧ (𝐺 β†Ύs (π‘†β€˜π‘ž))dom DProd 𝑠) β†’ ran 𝑠 βŠ† 𝒫 (π‘†β€˜π‘ž))
8950, 84, 87, 88subgdprd 19996 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ π‘ž ∈ 𝐴) ∧ 𝑠 ∈ Word (SubGrpβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž)))) ∧ (𝐺 β†Ύs (π‘†β€˜π‘ž))dom DProd 𝑠) β†’ ((𝐺 β†Ύs (π‘†β€˜π‘ž)) DProd 𝑠) = (𝐺 DProd 𝑠))
9055ad2antrr 724 . . . . . . . . . . . . . . . . 17 ((((πœ‘ ∧ π‘ž ∈ 𝐴) ∧ 𝑠 ∈ Word (SubGrpβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž)))) ∧ (𝐺 β†Ύs (π‘†β€˜π‘ž))dom DProd 𝑠) β†’ (π‘†β€˜π‘ž) = (Baseβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž))))
9190eqcomd 2731 . . . . . . . . . . . . . . . 16 ((((πœ‘ ∧ π‘ž ∈ 𝐴) ∧ 𝑠 ∈ Word (SubGrpβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž)))) ∧ (𝐺 β†Ύs (π‘†β€˜π‘ž))dom DProd 𝑠) β†’ (Baseβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž))) = (π‘†β€˜π‘ž))
9289, 91eqeq12d 2741 . . . . . . . . . . . . . . 15 ((((πœ‘ ∧ π‘ž ∈ 𝐴) ∧ 𝑠 ∈ Word (SubGrpβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž)))) ∧ (𝐺 β†Ύs (π‘†β€˜π‘ž))dom DProd 𝑠) β†’ (((𝐺 β†Ύs (π‘†β€˜π‘ž)) DProd 𝑠) = (Baseβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž))) ↔ (𝐺 DProd 𝑠) = (π‘†β€˜π‘ž)))
9392biimpd 228 . . . . . . . . . . . . . 14 ((((πœ‘ ∧ π‘ž ∈ 𝐴) ∧ 𝑠 ∈ Word (SubGrpβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž)))) ∧ (𝐺 β†Ύs (π‘†β€˜π‘ž))dom DProd 𝑠) β†’ (((𝐺 β†Ύs (π‘†β€˜π‘ž)) DProd 𝑠) = (Baseβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž))) β†’ (𝐺 DProd 𝑠) = (π‘†β€˜π‘ž)))
9493, 87jctild 524 . . . . . . . . . . . . 13 ((((πœ‘ ∧ π‘ž ∈ 𝐴) ∧ 𝑠 ∈ Word (SubGrpβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž)))) ∧ (𝐺 β†Ύs (π‘†β€˜π‘ž))dom DProd 𝑠) β†’ (((𝐺 β†Ύs (π‘†β€˜π‘ž)) DProd 𝑠) = (Baseβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž))) β†’ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (π‘†β€˜π‘ž))))
9594expimpd 452 . . . . . . . . . . . 12 (((πœ‘ ∧ π‘ž ∈ 𝐴) ∧ 𝑠 ∈ Word (SubGrpβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž)))) β†’ (((𝐺 β†Ύs (π‘†β€˜π‘ž))dom DProd 𝑠 ∧ ((𝐺 β†Ύs (π‘†β€˜π‘ž)) DProd 𝑠) = (Baseβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž)))) β†’ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (π‘†β€˜π‘ž))))
9682, 95sylan2 591 . . . . . . . . . . 11 (((πœ‘ ∧ π‘ž ∈ 𝐴) ∧ 𝑠 ∈ Word {π‘Ÿ ∈ (SubGrpβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž))) ∣ ((𝐺 β†Ύs (π‘†β€˜π‘ž)) β†Ύs π‘Ÿ) ∈ (CycGrp ∩ ran pGrp )}) β†’ (((𝐺 β†Ύs (π‘†β€˜π‘ž))dom DProd 𝑠 ∧ ((𝐺 β†Ύs (π‘†β€˜π‘ž)) DProd 𝑠) = (Baseβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž)))) β†’ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (π‘†β€˜π‘ž))))
97 oveq2 7424 . . . . . . . . . . . . . . . 16 (π‘Ÿ = 𝑦 β†’ ((𝐺 β†Ύs (π‘†β€˜π‘ž)) β†Ύs π‘Ÿ) = ((𝐺 β†Ύs (π‘†β€˜π‘ž)) β†Ύs 𝑦))
9897eleq1d 2810 . . . . . . . . . . . . . . 15 (π‘Ÿ = 𝑦 β†’ (((𝐺 β†Ύs (π‘†β€˜π‘ž)) β†Ύs π‘Ÿ) ∈ (CycGrp ∩ ran pGrp ) ↔ ((𝐺 β†Ύs (π‘†β€˜π‘ž)) β†Ύs 𝑦) ∈ (CycGrp ∩ ran pGrp )))
9998cbvrabv 3430 . . . . . . . . . . . . . 14 {π‘Ÿ ∈ (SubGrpβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž))) ∣ ((𝐺 β†Ύs (π‘†β€˜π‘ž)) β†Ύs π‘Ÿ) ∈ (CycGrp ∩ ran pGrp )} = {𝑦 ∈ (SubGrpβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž))) ∣ ((𝐺 β†Ύs (π‘†β€˜π‘ž)) β†Ύs 𝑦) ∈ (CycGrp ∩ ran pGrp )}
10050subsubg 19108 . . . . . . . . . . . . . . . . . . 19 ((π‘†β€˜π‘ž) ∈ (SubGrpβ€˜πΊ) β†’ (𝑦 ∈ (SubGrpβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž))) ↔ (𝑦 ∈ (SubGrpβ€˜πΊ) ∧ 𝑦 βŠ† (π‘†β€˜π‘ž))))
10137, 100syl 17 . . . . . . . . . . . . . . . . . 18 ((πœ‘ ∧ π‘ž ∈ 𝐴) β†’ (𝑦 ∈ (SubGrpβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž))) ↔ (𝑦 ∈ (SubGrpβ€˜πΊ) ∧ 𝑦 βŠ† (π‘†β€˜π‘ž))))
102101simprbda 497 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘ž ∈ 𝐴) ∧ 𝑦 ∈ (SubGrpβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž)))) β†’ 𝑦 ∈ (SubGrpβ€˜πΊ))
1031023adant3 1129 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘ž ∈ 𝐴) ∧ 𝑦 ∈ (SubGrpβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž))) ∧ ((𝐺 β†Ύs (π‘†β€˜π‘ž)) β†Ύs 𝑦) ∈ (CycGrp ∩ ran pGrp )) β†’ 𝑦 ∈ (SubGrpβ€˜πΊ))
104373ad2ant1 1130 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ π‘ž ∈ 𝐴) ∧ 𝑦 ∈ (SubGrpβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž))) ∧ ((𝐺 β†Ύs (π‘†β€˜π‘ž)) β†Ύs 𝑦) ∈ (CycGrp ∩ ran pGrp )) β†’ (π‘†β€˜π‘ž) ∈ (SubGrpβ€˜πΊ))
105101simplbda 498 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ π‘ž ∈ 𝐴) ∧ 𝑦 ∈ (SubGrpβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž)))) β†’ 𝑦 βŠ† (π‘†β€˜π‘ž))
1061053adant3 1129 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ π‘ž ∈ 𝐴) ∧ 𝑦 ∈ (SubGrpβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž))) ∧ ((𝐺 β†Ύs (π‘†β€˜π‘ž)) β†Ύs 𝑦) ∈ (CycGrp ∩ ran pGrp )) β†’ 𝑦 βŠ† (π‘†β€˜π‘ž))
107 ressabs 17229 . . . . . . . . . . . . . . . . . 18 (((π‘†β€˜π‘ž) ∈ (SubGrpβ€˜πΊ) ∧ 𝑦 βŠ† (π‘†β€˜π‘ž)) β†’ ((𝐺 β†Ύs (π‘†β€˜π‘ž)) β†Ύs 𝑦) = (𝐺 β†Ύs 𝑦))
108104, 106, 107syl2anc 582 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘ž ∈ 𝐴) ∧ 𝑦 ∈ (SubGrpβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž))) ∧ ((𝐺 β†Ύs (π‘†β€˜π‘ž)) β†Ύs 𝑦) ∈ (CycGrp ∩ ran pGrp )) β†’ ((𝐺 β†Ύs (π‘†β€˜π‘ž)) β†Ύs 𝑦) = (𝐺 β†Ύs 𝑦))
109 simp3 1135 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ π‘ž ∈ 𝐴) ∧ 𝑦 ∈ (SubGrpβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž))) ∧ ((𝐺 β†Ύs (π‘†β€˜π‘ž)) β†Ύs 𝑦) ∈ (CycGrp ∩ ran pGrp )) β†’ ((𝐺 β†Ύs (π‘†β€˜π‘ž)) β†Ύs 𝑦) ∈ (CycGrp ∩ ran pGrp ))
110108, 109eqeltrrd 2826 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ π‘ž ∈ 𝐴) ∧ 𝑦 ∈ (SubGrpβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž))) ∧ ((𝐺 β†Ύs (π‘†β€˜π‘ž)) β†Ύs 𝑦) ∈ (CycGrp ∩ ran pGrp )) β†’ (𝐺 β†Ύs 𝑦) ∈ (CycGrp ∩ ran pGrp ))
111 oveq2 7424 . . . . . . . . . . . . . . . . . 18 (π‘Ÿ = 𝑦 β†’ (𝐺 β†Ύs π‘Ÿ) = (𝐺 β†Ύs 𝑦))
112111eleq1d 2810 . . . . . . . . . . . . . . . . 17 (π‘Ÿ = 𝑦 β†’ ((𝐺 β†Ύs π‘Ÿ) ∈ (CycGrp ∩ ran pGrp ) ↔ (𝐺 β†Ύs 𝑦) ∈ (CycGrp ∩ ran pGrp )))
113112, 38elrab2 3677 . . . . . . . . . . . . . . . 16 (𝑦 ∈ 𝐢 ↔ (𝑦 ∈ (SubGrpβ€˜πΊ) ∧ (𝐺 β†Ύs 𝑦) ∈ (CycGrp ∩ ran pGrp )))
114103, 110, 113sylanbrc 581 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ π‘ž ∈ 𝐴) ∧ 𝑦 ∈ (SubGrpβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž))) ∧ ((𝐺 β†Ύs (π‘†β€˜π‘ž)) β†Ύs 𝑦) ∈ (CycGrp ∩ ran pGrp )) β†’ 𝑦 ∈ 𝐢)
115114rabssdv 4064 . . . . . . . . . . . . . 14 ((πœ‘ ∧ π‘ž ∈ 𝐴) β†’ {𝑦 ∈ (SubGrpβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž))) ∣ ((𝐺 β†Ύs (π‘†β€˜π‘ž)) β†Ύs 𝑦) ∈ (CycGrp ∩ ran pGrp )} βŠ† 𝐢)
11699, 115eqsstrid 4021 . . . . . . . . . . . . 13 ((πœ‘ ∧ π‘ž ∈ 𝐴) β†’ {π‘Ÿ ∈ (SubGrpβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž))) ∣ ((𝐺 β†Ύs (π‘†β€˜π‘ž)) β†Ύs π‘Ÿ) ∈ (CycGrp ∩ ran pGrp )} βŠ† 𝐢)
117 sswrd 14504 . . . . . . . . . . . . 13 ({π‘Ÿ ∈ (SubGrpβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž))) ∣ ((𝐺 β†Ύs (π‘†β€˜π‘ž)) β†Ύs π‘Ÿ) ∈ (CycGrp ∩ ran pGrp )} βŠ† 𝐢 β†’ Word {π‘Ÿ ∈ (SubGrpβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž))) ∣ ((𝐺 β†Ύs (π‘†β€˜π‘ž)) β†Ύs π‘Ÿ) ∈ (CycGrp ∩ ran pGrp )} βŠ† Word 𝐢)
118116, 117syl 17 . . . . . . . . . . . 12 ((πœ‘ ∧ π‘ž ∈ 𝐴) β†’ Word {π‘Ÿ ∈ (SubGrpβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž))) ∣ ((𝐺 β†Ύs (π‘†β€˜π‘ž)) β†Ύs π‘Ÿ) ∈ (CycGrp ∩ ran pGrp )} βŠ† Word 𝐢)
119118sselda 3972 . . . . . . . . . . 11 (((πœ‘ ∧ π‘ž ∈ 𝐴) ∧ 𝑠 ∈ Word {π‘Ÿ ∈ (SubGrpβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž))) ∣ ((𝐺 β†Ύs (π‘†β€˜π‘ž)) β†Ύs π‘Ÿ) ∈ (CycGrp ∩ ran pGrp )}) β†’ 𝑠 ∈ Word 𝐢)
12096, 119jctild 524 . . . . . . . . . 10 (((πœ‘ ∧ π‘ž ∈ 𝐴) ∧ 𝑠 ∈ Word {π‘Ÿ ∈ (SubGrpβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž))) ∣ ((𝐺 β†Ύs (π‘†β€˜π‘ž)) β†Ύs π‘Ÿ) ∈ (CycGrp ∩ ran pGrp )}) β†’ (((𝐺 β†Ύs (π‘†β€˜π‘ž))dom DProd 𝑠 ∧ ((𝐺 β†Ύs (π‘†β€˜π‘ž)) DProd 𝑠) = (Baseβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž)))) β†’ (𝑠 ∈ Word 𝐢 ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (π‘†β€˜π‘ž)))))
121120expimpd 452 . . . . . . . . 9 ((πœ‘ ∧ π‘ž ∈ 𝐴) β†’ ((𝑠 ∈ Word {π‘Ÿ ∈ (SubGrpβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž))) ∣ ((𝐺 β†Ύs (π‘†β€˜π‘ž)) β†Ύs π‘Ÿ) ∈ (CycGrp ∩ ran pGrp )} ∧ ((𝐺 β†Ύs (π‘†β€˜π‘ž))dom DProd 𝑠 ∧ ((𝐺 β†Ύs (π‘†β€˜π‘ž)) DProd 𝑠) = (Baseβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž))))) β†’ (𝑠 ∈ Word 𝐢 ∧ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (π‘†β€˜π‘ž)))))
122121reximdv2 3154 . . . . . . . 8 ((πœ‘ ∧ π‘ž ∈ 𝐴) β†’ (βˆƒπ‘  ∈ Word {π‘Ÿ ∈ (SubGrpβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž))) ∣ ((𝐺 β†Ύs (π‘†β€˜π‘ž)) β†Ύs π‘Ÿ) ∈ (CycGrp ∩ ran pGrp )} ((𝐺 β†Ύs (π‘†β€˜π‘ž))dom DProd 𝑠 ∧ ((𝐺 β†Ύs (π‘†β€˜π‘ž)) DProd 𝑠) = (Baseβ€˜(𝐺 β†Ύs (π‘†β€˜π‘ž)))) β†’ βˆƒπ‘  ∈ Word 𝐢(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (π‘†β€˜π‘ž))))
12378, 122mpd 15 . . . . . . 7 ((πœ‘ ∧ π‘ž ∈ 𝐴) β†’ βˆƒπ‘  ∈ Word 𝐢(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (π‘†β€˜π‘ž)))
124 rabn0 4381 . . . . . . 7 ({𝑠 ∈ Word 𝐢 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (π‘†β€˜π‘ž))} β‰  βˆ… ↔ βˆƒπ‘  ∈ Word 𝐢(𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (π‘†β€˜π‘ž)))
125123, 124sylibr 233 . . . . . 6 ((πœ‘ ∧ π‘ž ∈ 𝐴) β†’ {𝑠 ∈ Word 𝐢 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = (π‘†β€˜π‘ž))} β‰  βˆ…)
12647, 125eqnetrd 2998 . . . . 5 ((πœ‘ ∧ π‘ž ∈ 𝐴) β†’ {𝑦 ∈ Word 𝐢 ∣ 𝑦 ∈ (π‘Šβ€˜(π‘†β€˜π‘ž))} β‰  βˆ…)
127 rabn0 4381 . . . . 5 ({𝑦 ∈ Word 𝐢 ∣ 𝑦 ∈ (π‘Šβ€˜(π‘†β€˜π‘ž))} β‰  βˆ… ↔ βˆƒπ‘¦ ∈ Word 𝐢𝑦 ∈ (π‘Šβ€˜(π‘†β€˜π‘ž)))
128126, 127sylib 217 . . . 4 ((πœ‘ ∧ π‘ž ∈ 𝐴) β†’ βˆƒπ‘¦ ∈ Word 𝐢𝑦 ∈ (π‘Šβ€˜(π‘†β€˜π‘ž)))
129128ralrimiva 3136 . . 3 (πœ‘ β†’ βˆ€π‘ž ∈ 𝐴 βˆƒπ‘¦ ∈ Word 𝐢𝑦 ∈ (π‘Šβ€˜(π‘†β€˜π‘ž)))
130 eleq1 2813 . . . 4 (𝑦 = (π‘“β€˜π‘ž) β†’ (𝑦 ∈ (π‘Šβ€˜(π‘†β€˜π‘ž)) ↔ (π‘“β€˜π‘ž) ∈ (π‘Šβ€˜(π‘†β€˜π‘ž))))
131130ac6sfi 9310 . . 3 ((𝐴 ∈ Fin ∧ βˆ€π‘ž ∈ 𝐴 βˆƒπ‘¦ ∈ Word 𝐢𝑦 ∈ (π‘Šβ€˜(π‘†β€˜π‘ž))) β†’ βˆƒπ‘“(𝑓:𝐴⟢Word 𝐢 ∧ βˆ€π‘ž ∈ 𝐴 (π‘“β€˜π‘ž) ∈ (π‘Šβ€˜(π‘†β€˜π‘ž))))
13225, 129, 131syl2anc 582 . 2 (πœ‘ β†’ βˆƒπ‘“(𝑓:𝐴⟢Word 𝐢 ∧ βˆ€π‘ž ∈ 𝐴 (π‘“β€˜π‘ž) ∈ (π‘Šβ€˜(π‘†β€˜π‘ž))))
133 sneq 4634 . . . . . . . . 9 (π‘ž = 𝑦 β†’ {π‘ž} = {𝑦})
134 fveq2 6892 . . . . . . . . . 10 (π‘ž = 𝑦 β†’ (π‘“β€˜π‘ž) = (π‘“β€˜π‘¦))
135134dmeqd 5902 . . . . . . . . 9 (π‘ž = 𝑦 β†’ dom (π‘“β€˜π‘ž) = dom (π‘“β€˜π‘¦))
136133, 135xpeq12d 5703 . . . . . . . 8 (π‘ž = 𝑦 β†’ ({π‘ž} Γ— dom (π‘“β€˜π‘ž)) = ({𝑦} Γ— dom (π‘“β€˜π‘¦)))
137136cbviunv 5038 . . . . . . 7 βˆͺ π‘ž ∈ 𝐴 ({π‘ž} Γ— dom (π‘“β€˜π‘ž)) = βˆͺ 𝑦 ∈ 𝐴 ({𝑦} Γ— dom (π‘“β€˜π‘¦))
138 snfi 9067 . . . . . . . . . 10 {𝑦} ∈ Fin
139 simprl 769 . . . . . . . . . . . . 13 ((πœ‘ ∧ (𝑓:𝐴⟢Word 𝐢 ∧ βˆ€π‘ž ∈ 𝐴 (π‘“β€˜π‘ž) ∈ (π‘Šβ€˜(π‘†β€˜π‘ž)))) β†’ 𝑓:𝐴⟢Word 𝐢)
140139ffvelcdmda 7089 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑓:𝐴⟢Word 𝐢 ∧ βˆ€π‘ž ∈ 𝐴 (π‘“β€˜π‘ž) ∈ (π‘Šβ€˜(π‘†β€˜π‘ž)))) ∧ 𝑦 ∈ 𝐴) β†’ (π‘“β€˜π‘¦) ∈ Word 𝐢)
141 wrdf 14501 . . . . . . . . . . . 12 ((π‘“β€˜π‘¦) ∈ Word 𝐢 β†’ (π‘“β€˜π‘¦):(0..^(β™―β€˜(π‘“β€˜π‘¦)))⟢𝐢)
142 fdm 6726 . . . . . . . . . . . 12 ((π‘“β€˜π‘¦):(0..^(β™―β€˜(π‘“β€˜π‘¦)))⟢𝐢 β†’ dom (π‘“β€˜π‘¦) = (0..^(β™―β€˜(π‘“β€˜π‘¦))))
143140, 141, 1423syl 18 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑓:𝐴⟢Word 𝐢 ∧ βˆ€π‘ž ∈ 𝐴 (π‘“β€˜π‘ž) ∈ (π‘Šβ€˜(π‘†β€˜π‘ž)))) ∧ 𝑦 ∈ 𝐴) β†’ dom (π‘“β€˜π‘¦) = (0..^(β™―β€˜(π‘“β€˜π‘¦))))
144 fzofi 13971 . . . . . . . . . . 11 (0..^(β™―β€˜(π‘“β€˜π‘¦))) ∈ Fin
145143, 144eqeltrdi 2833 . . . . . . . . . 10 (((πœ‘ ∧ (𝑓:𝐴⟢Word 𝐢 ∧ βˆ€π‘ž ∈ 𝐴 (π‘“β€˜π‘ž) ∈ (π‘Šβ€˜(π‘†β€˜π‘ž)))) ∧ 𝑦 ∈ 𝐴) β†’ dom (π‘“β€˜π‘¦) ∈ Fin)
146 xpfi 9341 . . . . . . . . . 10 (({𝑦} ∈ Fin ∧ dom (π‘“β€˜π‘¦) ∈ Fin) β†’ ({𝑦} Γ— dom (π‘“β€˜π‘¦)) ∈ Fin)
147138, 145, 146sylancr 585 . . . . . . . . 9 (((πœ‘ ∧ (𝑓:𝐴⟢Word 𝐢 ∧ βˆ€π‘ž ∈ 𝐴 (π‘“β€˜π‘ž) ∈ (π‘Šβ€˜(π‘†β€˜π‘ž)))) ∧ 𝑦 ∈ 𝐴) β†’ ({𝑦} Γ— dom (π‘“β€˜π‘¦)) ∈ Fin)
148147ralrimiva 3136 . . . . . . . 8 ((πœ‘ ∧ (𝑓:𝐴⟢Word 𝐢 ∧ βˆ€π‘ž ∈ 𝐴 (π‘“β€˜π‘ž) ∈ (π‘Šβ€˜(π‘†β€˜π‘ž)))) β†’ βˆ€π‘¦ ∈ 𝐴 ({𝑦} Γ— dom (π‘“β€˜π‘¦)) ∈ Fin)
149 iunfi 9364 . . . . . . . 8 ((𝐴 ∈ Fin ∧ βˆ€π‘¦ ∈ 𝐴 ({𝑦} Γ— dom (π‘“β€˜π‘¦)) ∈ Fin) β†’ βˆͺ 𝑦 ∈ 𝐴 ({𝑦} Γ— dom (π‘“β€˜π‘¦)) ∈ Fin)
15025, 148, 149syl2an2r 683 . . . . . . 7 ((πœ‘ ∧ (𝑓:𝐴⟢Word 𝐢 ∧ βˆ€π‘ž ∈ 𝐴 (π‘“β€˜π‘ž) ∈ (π‘Šβ€˜(π‘†β€˜π‘ž)))) β†’ βˆͺ 𝑦 ∈ 𝐴 ({𝑦} Γ— dom (π‘“β€˜π‘¦)) ∈ Fin)
151137, 150eqeltrid 2829 . . . . . 6 ((πœ‘ ∧ (𝑓:𝐴⟢Word 𝐢 ∧ βˆ€π‘ž ∈ 𝐴 (π‘“β€˜π‘ž) ∈ (π‘Šβ€˜(π‘†β€˜π‘ž)))) β†’ βˆͺ π‘ž ∈ 𝐴 ({π‘ž} Γ— dom (π‘“β€˜π‘ž)) ∈ Fin)
152 hashcl 14347 . . . . . 6 (βˆͺ π‘ž ∈ 𝐴 ({π‘ž} Γ— dom (π‘“β€˜π‘ž)) ∈ Fin β†’ (β™―β€˜βˆͺ π‘ž ∈ 𝐴 ({π‘ž} Γ— dom (π‘“β€˜π‘ž))) ∈ β„•0)
153 hashfzo0 14421 . . . . . 6 ((β™―β€˜βˆͺ π‘ž ∈ 𝐴 ({π‘ž} Γ— dom (π‘“β€˜π‘ž))) ∈ β„•0 β†’ (β™―β€˜(0..^(β™―β€˜βˆͺ π‘ž ∈ 𝐴 ({π‘ž} Γ— dom (π‘“β€˜π‘ž))))) = (β™―β€˜βˆͺ π‘ž ∈ 𝐴 ({π‘ž} Γ— dom (π‘“β€˜π‘ž))))
154151, 152, 1533syl 18 . . . . 5 ((πœ‘ ∧ (𝑓:𝐴⟢Word 𝐢 ∧ βˆ€π‘ž ∈ 𝐴 (π‘“β€˜π‘ž) ∈ (π‘Šβ€˜(π‘†β€˜π‘ž)))) β†’ (β™―β€˜(0..^(β™―β€˜βˆͺ π‘ž ∈ 𝐴 ({π‘ž} Γ— dom (π‘“β€˜π‘ž))))) = (β™―β€˜βˆͺ π‘ž ∈ 𝐴 ({π‘ž} Γ— dom (π‘“β€˜π‘ž))))
155 fzofi 13971 . . . . . 6 (0..^(β™―β€˜βˆͺ π‘ž ∈ 𝐴 ({π‘ž} Γ— dom (π‘“β€˜π‘ž)))) ∈ Fin
156 hashen 14338 . . . . . 6 (((0..^(β™―β€˜βˆͺ π‘ž ∈ 𝐴 ({π‘ž} Γ— dom (π‘“β€˜π‘ž)))) ∈ Fin ∧ βˆͺ π‘ž ∈ 𝐴 ({π‘ž} Γ— dom (π‘“β€˜π‘ž)) ∈ Fin) β†’ ((β™―β€˜(0..^(β™―β€˜βˆͺ π‘ž ∈ 𝐴 ({π‘ž} Γ— dom (π‘“β€˜π‘ž))))) = (β™―β€˜βˆͺ π‘ž ∈ 𝐴 ({π‘ž} Γ— dom (π‘“β€˜π‘ž))) ↔ (0..^(β™―β€˜βˆͺ π‘ž ∈ 𝐴 ({π‘ž} Γ— dom (π‘“β€˜π‘ž)))) β‰ˆ βˆͺ π‘ž ∈ 𝐴 ({π‘ž} Γ— dom (π‘“β€˜π‘ž))))
157155, 151, 156sylancr 585 . . . . 5 ((πœ‘ ∧ (𝑓:𝐴⟢Word 𝐢 ∧ βˆ€π‘ž ∈ 𝐴 (π‘“β€˜π‘ž) ∈ (π‘Šβ€˜(π‘†β€˜π‘ž)))) β†’ ((β™―β€˜(0..^(β™―β€˜βˆͺ π‘ž ∈ 𝐴 ({π‘ž} Γ— dom (π‘“β€˜π‘ž))))) = (β™―β€˜βˆͺ π‘ž ∈ 𝐴 ({π‘ž} Γ— dom (π‘“β€˜π‘ž))) ↔ (0..^(β™―β€˜βˆͺ π‘ž ∈ 𝐴 ({π‘ž} Γ— dom (π‘“β€˜π‘ž)))) β‰ˆ βˆͺ π‘ž ∈ 𝐴 ({π‘ž} Γ— dom (π‘“β€˜π‘ž))))
158154, 157mpbid 231 . . . 4 ((πœ‘ ∧ (𝑓:𝐴⟢Word 𝐢 ∧ βˆ€π‘ž ∈ 𝐴 (π‘“β€˜π‘ž) ∈ (π‘Šβ€˜(π‘†β€˜π‘ž)))) β†’ (0..^(β™―β€˜βˆͺ π‘ž ∈ 𝐴 ({π‘ž} Γ— dom (π‘“β€˜π‘ž)))) β‰ˆ βˆͺ π‘ž ∈ 𝐴 ({π‘ž} Γ— dom (π‘“β€˜π‘ž)))
159 bren 8972 . . . 4 ((0..^(β™―β€˜βˆͺ π‘ž ∈ 𝐴 ({π‘ž} Γ— dom (π‘“β€˜π‘ž)))) β‰ˆ βˆͺ π‘ž ∈ 𝐴 ({π‘ž} Γ— dom (π‘“β€˜π‘ž)) ↔ βˆƒβ„Ž β„Ž:(0..^(β™―β€˜βˆͺ π‘ž ∈ 𝐴 ({π‘ž} Γ— dom (π‘“β€˜π‘ž))))–1-1-ontoβ†’βˆͺ π‘ž ∈ 𝐴 ({π‘ž} Γ— dom (π‘“β€˜π‘ž)))
160158, 159sylib 217 . . 3 ((πœ‘ ∧ (𝑓:𝐴⟢Word 𝐢 ∧ βˆ€π‘ž ∈ 𝐴 (π‘“β€˜π‘ž) ∈ (π‘Šβ€˜(π‘†β€˜π‘ž)))) β†’ βˆƒβ„Ž β„Ž:(0..^(β™―β€˜βˆͺ π‘ž ∈ 𝐴 ({π‘ž} Γ— dom (π‘“β€˜π‘ž))))–1-1-ontoβ†’βˆͺ π‘ž ∈ 𝐴 ({π‘ž} Γ— dom (π‘“β€˜π‘ž)))
1616adantr 479 . . . . . 6 ((πœ‘ ∧ ((𝑓:𝐴⟢Word 𝐢 ∧ βˆ€π‘ž ∈ 𝐴 (π‘“β€˜π‘ž) ∈ (π‘Šβ€˜(π‘†β€˜π‘ž))) ∧ β„Ž:(0..^(β™―β€˜βˆͺ π‘ž ∈ 𝐴 ({π‘ž} Γ— dom (π‘“β€˜π‘ž))))–1-1-ontoβ†’βˆͺ π‘ž ∈ 𝐴 ({π‘ž} Γ— dom (π‘“β€˜π‘ž)))) β†’ 𝐺 ∈ Abel)
16211adantr 479 . . . . . 6 ((πœ‘ ∧ ((𝑓:𝐴⟢Word 𝐢 ∧ βˆ€π‘ž ∈ 𝐴 (π‘“β€˜π‘ž) ∈ (π‘Šβ€˜(π‘†β€˜π‘ž))) ∧ β„Ž:(0..^(β™―β€˜βˆͺ π‘ž ∈ 𝐴 ({π‘ž} Γ— dom (π‘“β€˜π‘ž))))–1-1-ontoβ†’βˆͺ π‘ž ∈ 𝐴 ({π‘ž} Γ— dom (π‘“β€˜π‘ž)))) β†’ 𝐡 ∈ Fin)
163 breq1 5146 . . . . . . . 8 (𝑀 = π‘Ž β†’ (𝑀 βˆ₯ (β™―β€˜π΅) ↔ π‘Ž βˆ₯ (β™―β€˜π΅)))
164163cbvrabv 3430 . . . . . . 7 {𝑀 ∈ β„™ ∣ 𝑀 βˆ₯ (β™―β€˜π΅)} = {π‘Ž ∈ β„™ ∣ π‘Ž βˆ₯ (β™―β€˜π΅)}
1652, 164eqtri 2753 . . . . . 6 𝐴 = {π‘Ž ∈ β„™ ∣ π‘Ž βˆ₯ (β™―β€˜π΅)}
166 fveq2 6892 . . . . . . . . . . 11 (π‘₯ = 𝑐 β†’ (π‘‚β€˜π‘₯) = (π‘‚β€˜π‘))
167166breq1d 5153 . . . . . . . . . 10 (π‘₯ = 𝑐 β†’ ((π‘‚β€˜π‘₯) βˆ₯ (𝑝↑(𝑝 pCnt (β™―β€˜π΅))) ↔ (π‘‚β€˜π‘) βˆ₯ (𝑝↑(𝑝 pCnt (β™―β€˜π΅)))))
168167cbvrabv 3430 . . . . . . . . 9 {π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ (𝑝↑(𝑝 pCnt (β™―β€˜π΅)))} = {𝑐 ∈ 𝐡 ∣ (π‘‚β€˜π‘) βˆ₯ (𝑝↑(𝑝 pCnt (β™―β€˜π΅)))}
169 id 22 . . . . . . . . . . . 12 (𝑝 = 𝑏 β†’ 𝑝 = 𝑏)
170 oveq1 7423 . . . . . . . . . . . 12 (𝑝 = 𝑏 β†’ (𝑝 pCnt (β™―β€˜π΅)) = (𝑏 pCnt (β™―β€˜π΅)))
171169, 170oveq12d 7434 . . . . . . . . . . 11 (𝑝 = 𝑏 β†’ (𝑝↑(𝑝 pCnt (β™―β€˜π΅))) = (𝑏↑(𝑏 pCnt (β™―β€˜π΅))))
172171breq2d 5155 . . . . . . . . . 10 (𝑝 = 𝑏 β†’ ((π‘‚β€˜π‘) βˆ₯ (𝑝↑(𝑝 pCnt (β™―β€˜π΅))) ↔ (π‘‚β€˜π‘) βˆ₯ (𝑏↑(𝑏 pCnt (β™―β€˜π΅)))))
173172rabbidv 3427 . . . . . . . . 9 (𝑝 = 𝑏 β†’ {𝑐 ∈ 𝐡 ∣ (π‘‚β€˜π‘) βˆ₯ (𝑝↑(𝑝 pCnt (β™―β€˜π΅)))} = {𝑐 ∈ 𝐡 ∣ (π‘‚β€˜π‘) βˆ₯ (𝑏↑(𝑏 pCnt (β™―β€˜π΅)))})
174168, 173eqtrid 2777 . . . . . . . 8 (𝑝 = 𝑏 β†’ {π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ (𝑝↑(𝑝 pCnt (β™―β€˜π΅)))} = {𝑐 ∈ 𝐡 ∣ (π‘‚β€˜π‘) βˆ₯ (𝑏↑(𝑏 pCnt (β™―β€˜π΅)))})
175174cbvmptv 5256 . . . . . . 7 (𝑝 ∈ 𝐴 ↦ {π‘₯ ∈ 𝐡 ∣ (π‘‚β€˜π‘₯) βˆ₯ (𝑝↑(𝑝 pCnt (β™―β€˜π΅)))}) = (𝑏 ∈ 𝐴 ↦ {𝑐 ∈ 𝐡 ∣ (π‘‚β€˜π‘) βˆ₯ (𝑏↑(𝑏 pCnt (β™―β€˜π΅)))})
17628, 175eqtri 2753 . . . . . 6 𝑆 = (𝑏 ∈ 𝐴 ↦ {𝑐 ∈ 𝐡 ∣ (π‘‚β€˜π‘) βˆ₯ (𝑏↑(𝑏 pCnt (β™―β€˜π΅)))})
177 breq2 5147 . . . . . . . . . 10 (𝑠 = 𝑑 β†’ (𝐺dom DProd 𝑠 ↔ 𝐺dom DProd 𝑑))
178 oveq2 7424 . . . . . . . . . . 11 (𝑠 = 𝑑 β†’ (𝐺 DProd 𝑠) = (𝐺 DProd 𝑑))
179178eqeq1d 2727 . . . . . . . . . 10 (𝑠 = 𝑑 β†’ ((𝐺 DProd 𝑠) = 𝑔 ↔ (𝐺 DProd 𝑑) = 𝑔))
180177, 179anbi12d 630 . . . . . . . . 9 (𝑠 = 𝑑 β†’ ((𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑔) ↔ (𝐺dom DProd 𝑑 ∧ (𝐺 DProd 𝑑) = 𝑔)))
181180cbvrabv 3430 . . . . . . . 8 {𝑠 ∈ Word 𝐢 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑔)} = {𝑑 ∈ Word 𝐢 ∣ (𝐺dom DProd 𝑑 ∧ (𝐺 DProd 𝑑) = 𝑔)}
182181mpteq2i 5248 . . . . . . 7 (𝑔 ∈ (SubGrpβ€˜πΊ) ↦ {𝑠 ∈ Word 𝐢 ∣ (𝐺dom DProd 𝑠 ∧ (𝐺 DProd 𝑠) = 𝑔)}) = (𝑔 ∈ (SubGrpβ€˜πΊ) ↦ {𝑑 ∈ Word 𝐢 ∣ (𝐺dom DProd 𝑑 ∧ (𝐺 DProd 𝑑) = 𝑔)})
18339, 182eqtri 2753 . . . . . 6 π‘Š = (𝑔 ∈ (SubGrpβ€˜πΊ) ↦ {𝑑 ∈ Word 𝐢 ∣ (𝐺dom DProd 𝑑 ∧ (𝐺 DProd 𝑑) = 𝑔)})
184 simprll 777 . . . . . 6 ((πœ‘ ∧ ((𝑓:𝐴⟢Word 𝐢 ∧ βˆ€π‘ž ∈ 𝐴 (π‘“β€˜π‘ž) ∈ (π‘Šβ€˜(π‘†β€˜π‘ž))) ∧ β„Ž:(0..^(β™―β€˜βˆͺ π‘ž ∈ 𝐴 ({π‘ž} Γ— dom (π‘“β€˜π‘ž))))–1-1-ontoβ†’βˆͺ π‘ž ∈ 𝐴 ({π‘ž} Γ— dom (π‘“β€˜π‘ž)))) β†’ 𝑓:𝐴⟢Word 𝐢)
185 simprlr 778 . . . . . . 7 ((πœ‘ ∧ ((𝑓:𝐴⟢Word 𝐢 ∧ βˆ€π‘ž ∈ 𝐴 (π‘“β€˜π‘ž) ∈ (π‘Šβ€˜(π‘†β€˜π‘ž))) ∧ β„Ž:(0..^(β™―β€˜βˆͺ π‘ž ∈ 𝐴 ({π‘ž} Γ— dom (π‘“β€˜π‘ž))))–1-1-ontoβ†’βˆͺ π‘ž ∈ 𝐴 ({π‘ž} Γ— dom (π‘“β€˜π‘ž)))) β†’ βˆ€π‘ž ∈ 𝐴 (π‘“β€˜π‘ž) ∈ (π‘Šβ€˜(π‘†β€˜π‘ž)))
186 2fveq3 6897 . . . . . . . . 9 (π‘ž = 𝑦 β†’ (π‘Šβ€˜(π‘†β€˜π‘ž)) = (π‘Šβ€˜(π‘†β€˜π‘¦)))
187134, 186eleq12d 2819 . . . . . . . 8 (π‘ž = 𝑦 β†’ ((π‘“β€˜π‘ž) ∈ (π‘Šβ€˜(π‘†β€˜π‘ž)) ↔ (π‘“β€˜π‘¦) ∈ (π‘Šβ€˜(π‘†β€˜π‘¦))))
188187cbvralvw 3225 . . . . . . 7 (βˆ€π‘ž ∈ 𝐴 (π‘“β€˜π‘ž) ∈ (π‘Šβ€˜(π‘†β€˜π‘ž)) ↔ βˆ€π‘¦ ∈ 𝐴 (π‘“β€˜π‘¦) ∈ (π‘Šβ€˜(π‘†β€˜π‘¦)))
189185, 188sylib 217 . . . . . 6 ((πœ‘ ∧ ((𝑓:𝐴⟢Word 𝐢 ∧ βˆ€π‘ž ∈ 𝐴 (π‘“β€˜π‘ž) ∈ (π‘Šβ€˜(π‘†β€˜π‘ž))) ∧ β„Ž:(0..^(β™―β€˜βˆͺ π‘ž ∈ 𝐴 ({π‘ž} Γ— dom (π‘“β€˜π‘ž))))–1-1-ontoβ†’βˆͺ π‘ž ∈ 𝐴 ({π‘ž} Γ— dom (π‘“β€˜π‘ž)))) β†’ βˆ€π‘¦ ∈ 𝐴 (π‘“β€˜π‘¦) ∈ (π‘Šβ€˜(π‘†β€˜π‘¦)))
190 simprr 771 . . . . . 6 ((πœ‘ ∧ ((𝑓:𝐴⟢Word 𝐢 ∧ βˆ€π‘ž ∈ 𝐴 (π‘“β€˜π‘ž) ∈ (π‘Šβ€˜(π‘†β€˜π‘ž))) ∧ β„Ž:(0..^(β™―β€˜βˆͺ π‘ž ∈ 𝐴 ({π‘ž} Γ— dom (π‘“β€˜π‘ž))))–1-1-ontoβ†’βˆͺ π‘ž ∈ 𝐴 ({π‘ž} Γ— dom (π‘“β€˜π‘ž)))) β†’ β„Ž:(0..^(β™―β€˜βˆͺ π‘ž ∈ 𝐴 ({π‘ž} Γ— dom (π‘“β€˜π‘ž))))–1-1-ontoβ†’βˆͺ π‘ž ∈ 𝐴 ({π‘ž} Γ— dom (π‘“β€˜π‘ž)))
1918, 38, 161, 162, 27, 165, 176, 183, 184, 189, 137, 190ablfaclem2 20047 . . . . 5 ((πœ‘ ∧ ((𝑓:𝐴⟢Word 𝐢 ∧ βˆ€π‘ž ∈ 𝐴 (π‘“β€˜π‘ž) ∈ (π‘Šβ€˜(π‘†β€˜π‘ž))) ∧ β„Ž:(0..^(β™―β€˜βˆͺ π‘ž ∈ 𝐴 ({π‘ž} Γ— dom (π‘“β€˜π‘ž))))–1-1-ontoβ†’βˆͺ π‘ž ∈ 𝐴 ({π‘ž} Γ— dom (π‘“β€˜π‘ž)))) β†’ (π‘Šβ€˜π΅) β‰  βˆ…)
192191expr 455 . . . 4 ((πœ‘ ∧ (𝑓:𝐴⟢Word 𝐢 ∧ βˆ€π‘ž ∈ 𝐴 (π‘“β€˜π‘ž) ∈ (π‘Šβ€˜(π‘†β€˜π‘ž)))) β†’ (β„Ž:(0..^(β™―β€˜βˆͺ π‘ž ∈ 𝐴 ({π‘ž} Γ— dom (π‘“β€˜π‘ž))))–1-1-ontoβ†’βˆͺ π‘ž ∈ 𝐴 ({π‘ž} Γ— dom (π‘“β€˜π‘ž)) β†’ (π‘Šβ€˜π΅) β‰  βˆ…))
193192exlimdv 1928 . . 3 ((πœ‘ ∧ (𝑓:𝐴⟢Word 𝐢 ∧ βˆ€π‘ž ∈ 𝐴 (π‘“β€˜π‘ž) ∈ (π‘Šβ€˜(π‘†β€˜π‘ž)))) β†’ (βˆƒβ„Ž β„Ž:(0..^(β™―β€˜βˆͺ π‘ž ∈ 𝐴 ({π‘ž} Γ— dom (π‘“β€˜π‘ž))))–1-1-ontoβ†’βˆͺ π‘ž ∈ 𝐴 ({π‘ž} Γ— dom (π‘“β€˜π‘ž)) β†’ (π‘Šβ€˜π΅) β‰  βˆ…))
194160, 193mpd 15 . 2 ((πœ‘ ∧ (𝑓:𝐴⟢Word 𝐢 ∧ βˆ€π‘ž ∈ 𝐴 (π‘“β€˜π‘ž) ∈ (π‘Šβ€˜(π‘†β€˜π‘ž)))) β†’ (π‘Šβ€˜π΅) β‰  βˆ…)
195132, 194exlimddv 1930 1 (πœ‘ β†’ (π‘Šβ€˜π΅) β‰  βˆ…)
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1084   = wceq 1533  βˆƒwex 1773   ∈ wcel 2098   β‰  wne 2930  βˆ€wral 3051  βˆƒwrex 3060  {crab 3419   ∩ cin 3938   βŠ† wss 3939  βˆ…c0 4318  π’« cpw 4598  {csn 4624  βˆͺ ciun 4991   class class class wbr 5143   ↦ cmpt 5226   Γ— cxp 5670  dom cdm 5672  ran crn 5673  βŸΆwf 6539  β€“1-1-ontoβ†’wf1o 6542  β€˜cfv 6543  (class class class)co 7416   β‰ˆ cen 8959  Fincfn 8962  0cc0 11138  1c1 11139   ≀ cle 11279  β„•cn 12242  β„•0cn0 12502  β„€cz 12588  ...cfz 13516  ..^cfzo 13659  β†‘cexp 14058  β™―chash 14321  Word cword 14496   βˆ₯ cdvds 16230  β„™cprime 16641   pCnt cpc 16804  Basecbs 17179   β†Ύs cress 17208  Grpcgrp 18894  SubGrpcsubg 19079  odcod 19483   pGrp cpgp 19485  Abelcabl 19740  CycGrpccyg 19836   DProd cdprd 19954
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5280  ax-sep 5294  ax-nul 5301  ax-pow 5359  ax-pr 5423  ax-un 7738  ax-inf2 9664  ax-cnex 11194  ax-resscn 11195  ax-1cn 11196  ax-icn 11197  ax-addcl 11198  ax-addrcl 11199  ax-mulcl 11200  ax-mulrcl 11201  ax-mulcom 11202  ax-addass 11203  ax-mulass 11204  ax-distr 11205  ax-i2m1 11206  ax-1ne0 11207  ax-1rid 11208  ax-rnegex 11209  ax-rrecex 11210  ax-cnre 11211  ax-pre-lttri 11212  ax-pre-lttrn 11213  ax-pre-ltadd 11214  ax-pre-mulgt0 11215  ax-pre-sup 11216
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2931  df-nel 3037  df-ral 3052  df-rex 3061  df-rmo 3364  df-reu 3365  df-rab 3420  df-v 3465  df-sbc 3769  df-csb 3885  df-dif 3942  df-un 3944  df-in 3946  df-ss 3956  df-pss 3959  df-nul 4319  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4904  df-int 4945  df-iun 4993  df-iin 4994  df-disj 5109  df-br 5144  df-opab 5206  df-mpt 5227  df-tr 5261  df-id 5570  df-eprel 5576  df-po 5584  df-so 5585  df-fr 5627  df-se 5628  df-we 5629  df-xp 5678  df-rel 5679  df-cnv 5680  df-co 5681  df-dm 5682  df-rn 5683  df-res 5684  df-ima 5685  df-pred 6300  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-isom 6552  df-riota 7372  df-ov 7419  df-oprab 7420  df-mpo 7421  df-of 7682  df-rpss 7726  df-om 7869  df-1st 7991  df-2nd 7992  df-supp 8164  df-tpos 8230  df-frecs 8285  df-wrecs 8316  df-recs 8390  df-rdg 8429  df-1o 8485  df-2o 8486  df-oadd 8489  df-omul 8490  df-er 8723  df-ec 8725  df-qs 8729  df-map 8845  df-ixp 8915  df-en 8963  df-dom 8964  df-sdom 8965  df-fin 8966  df-fsupp 9386  df-sup 9465  df-inf 9466  df-oi 9533  df-dju 9924  df-card 9962  df-acn 9965  df-pnf 11280  df-mnf 11281  df-xr 11282  df-ltxr 11283  df-le 11284  df-sub 11476  df-neg 11477  df-div 11902  df-nn 12243  df-2 12305  df-3 12306  df-n0 12503  df-xnn0 12575  df-z 12589  df-uz 12853  df-q 12963  df-rp 13007  df-fz 13517  df-fzo 13660  df-fl 13789  df-mod 13867  df-seq 13999  df-exp 14059  df-fac 14265  df-bc 14294  df-hash 14322  df-word 14497  df-concat 14553  df-s1 14578  df-cj 15078  df-re 15079  df-im 15080  df-sqrt 15214  df-abs 15215  df-clim 15464  df-sum 15665  df-dvds 16231  df-gcd 16469  df-prm 16642  df-pc 16805  df-sets 17132  df-slot 17150  df-ndx 17162  df-base 17180  df-ress 17209  df-plusg 17245  df-0g 17422  df-gsum 17423  df-mre 17565  df-mrc 17566  df-acs 17568  df-mgm 18599  df-sgrp 18678  df-mnd 18694  df-mhm 18739  df-submnd 18740  df-grp 18897  df-minusg 18898  df-sbg 18899  df-mulg 19028  df-subg 19082  df-eqg 19084  df-ghm 19172  df-gim 19217  df-ga 19245  df-cntz 19272  df-oppg 19301  df-od 19487  df-gex 19488  df-pgp 19489  df-lsm 19595  df-pj1 19596  df-cmn 19741  df-abl 19742  df-cyg 19837  df-dprd 19956
This theorem is referenced by:  ablfac  20049
  Copyright terms: Public domain W3C validator