Metamath Proof Explorer

Theorem ablfaclem2

Description: Lemma for ablfac . (Contributed by Mario Carneiro, 27-Apr-2016) (Proof shortened by Mario Carneiro, 3-May-2016)

Ref Expression
Hypotheses 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 𝑠 ) = 𝑔 ) } )
ablfaclem2.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ Word 𝐶 )
ablfaclem2.q ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) ∈ ( 𝑊 ‘ ( 𝑆 ‘ 𝑦 ) ) )
ablfaclem2.l ⊢ 𝐿 = ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × dom ( 𝐹 ‘ 𝑦 ) )
ablfaclem2.g ⊢ ( 𝜑 → 𝐻 : ( 0 ..^ ( ♯ ‘ 𝐿 ) ) –1-1-onto→ 𝐿 )
Assertion ablfaclem2 ( 𝜑 → ( 𝑊 ‘ 𝐵 ) ≠ ∅ )

Proof

Step Hyp Ref Expression
1 ablfac.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 ablfac.c ⊢ 𝐶 = { 𝑟 ∈ ( SubGrp ‘ 𝐺 ) ∣ ( 𝐺 ↾s 𝑟 ) ∈ ( CycGrp ∩ ran pGrp ) }
3 ablfac.1 ⊢ ( 𝜑 → 𝐺 ∈ Abel )
4 ablfac.2 ⊢ ( 𝜑 → 𝐵 ∈ Fin )
5 ablfac.o ⊢ 𝑂 = ( od ‘ 𝐺 )
6 ablfac.a ⊢ 𝐴 = { 𝑤 ∈ ℙ ∣ 𝑤 ∥ ( ♯ ‘ 𝐵 ) }
7 ablfac.s ⊢ 𝑆 = ( 𝑝 ∈ 𝐴 ↦ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) } )
8 ablfac.w ⊢ 𝑊 = ( 𝑔 ∈ ( SubGrp ‘ 𝐺 ) ↦ { 𝑠 ∈ Word 𝐶 ∣ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝑔 ) } )
9 ablfaclem2.f ⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ Word 𝐶 )
10 ablfaclem2.q ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐴 ( 𝐹 ‘ 𝑦 ) ∈ ( 𝑊 ‘ ( 𝑆 ‘ 𝑦 ) ) )
11 ablfaclem2.l ⊢ 𝐿 = ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × dom ( 𝐹 ‘ 𝑦 ) )
12 ablfaclem2.g ⊢ ( 𝜑 → 𝐻 : ( 0 ..^ ( ♯ ‘ 𝐿 ) ) –1-1-onto→ 𝐿 )
13 ablgrp ⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )
14 1 subgid ⊢ ( 𝐺 ∈ Grp → 𝐵 ∈ ( SubGrp ‘ 𝐺 ) )
15 1 2 3 4 5 6 7 8 ablfaclem1 ⊢ ( 𝐵 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑊 ‘ 𝐵 ) = { 𝑠 ∈ Word 𝐶 ∣ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) } )
16 3 13 14 15 4syl ⊢ ( 𝜑 → ( 𝑊 ‘ 𝐵 ) = { 𝑠 ∈ Word 𝐶 ∣ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) } )
17 9 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑦 ) ∈ Word 𝐶 )
18 wrdf ⊢ ( ( 𝐹 ‘ 𝑦 ) ∈ Word 𝐶 → ( 𝐹 ‘ 𝑦 ) : ( 0 ..^ ( ♯ ‘ ( 𝐹 ‘ 𝑦 ) ) ) ⟶ 𝐶 )
19 17 18 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑦 ) : ( 0 ..^ ( ♯ ‘ ( 𝐹 ‘ 𝑦 ) ) ) ⟶ 𝐶 )
20 19 ffdmd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑦 ) : dom ( 𝐹 ‘ 𝑦 ) ⟶ 𝐶 )
21 20 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ dom ( 𝐹 ‘ 𝑦 ) ) → ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑧 ) ∈ 𝐶 )
22 21 anasss ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ dom ( 𝐹 ‘ 𝑦 ) ) ) → ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑧 ) ∈ 𝐶 )
23 22 ralrimivva ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ dom ( 𝐹 ‘ 𝑦 ) ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑧 ) ∈ 𝐶 )
24 eqid ⊢ ( 𝑦 ∈ 𝐴 , 𝑧 ∈ dom ( 𝐹 ‘ 𝑦 ) ↦ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑧 ) ) = ( 𝑦 ∈ 𝐴 , 𝑧 ∈ dom ( 𝐹 ‘ 𝑦 ) ↦ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑧 ) )
25 24 fmpox ⊢ ( ∀ 𝑦 ∈ 𝐴 ∀ 𝑧 ∈ dom ( 𝐹 ‘ 𝑦 ) ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑧 ) ∈ 𝐶 ↔ ( 𝑦 ∈ 𝐴 , 𝑧 ∈ dom ( 𝐹 ‘ 𝑦 ) ↦ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑧 ) ) : ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × dom ( 𝐹 ‘ 𝑦 ) ) ⟶ 𝐶 )
26 23 25 sylib ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐴 , 𝑧 ∈ dom ( 𝐹 ‘ 𝑦 ) ↦ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑧 ) ) : ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × dom ( 𝐹 ‘ 𝑦 ) ) ⟶ 𝐶 )
27 11 feq2i ⊢ ( ( 𝑦 ∈ 𝐴 , 𝑧 ∈ dom ( 𝐹 ‘ 𝑦 ) ↦ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑧 ) ) : 𝐿 ⟶ 𝐶 ↔ ( 𝑦 ∈ 𝐴 , 𝑧 ∈ dom ( 𝐹 ‘ 𝑦 ) ↦ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑧 ) ) : ∪ 𝑦 ∈ 𝐴 ( { 𝑦 } × dom ( 𝐹 ‘ 𝑦 ) ) ⟶ 𝐶 )
28 26 27 sylibr ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐴 , 𝑧 ∈ dom ( 𝐹 ‘ 𝑦 ) ↦ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑧 ) ) : 𝐿 ⟶ 𝐶 )
29 f1of ⊢ ( 𝐻 : ( 0 ..^ ( ♯ ‘ 𝐿 ) ) –1-1-onto→ 𝐿 → 𝐻 : ( 0 ..^ ( ♯ ‘ 𝐿 ) ) ⟶ 𝐿 )
30 12 29 syl ⊢ ( 𝜑 → 𝐻 : ( 0 ..^ ( ♯ ‘ 𝐿 ) ) ⟶ 𝐿 )
31 fco ⊢ ( ( ( 𝑦 ∈ 𝐴 , 𝑧 ∈ dom ( 𝐹 ‘ 𝑦 ) ↦ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑧 ) ) : 𝐿 ⟶ 𝐶 ∧ 𝐻 : ( 0 ..^ ( ♯ ‘ 𝐿 ) ) ⟶ 𝐿 ) → ( ( 𝑦 ∈ 𝐴 , 𝑧 ∈ dom ( 𝐹 ‘ 𝑦 ) ↦ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑧 ) ) ∘ 𝐻 ) : ( 0 ..^ ( ♯ ‘ 𝐿 ) ) ⟶ 𝐶 )
32 28 30 31 syl2anc ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐴 , 𝑧 ∈ dom ( 𝐹 ‘ 𝑦 ) ↦ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑧 ) ) ∘ 𝐻 ) : ( 0 ..^ ( ♯ ‘ 𝐿 ) ) ⟶ 𝐶 )
33 iswrdi ⊢ ( ( ( 𝑦 ∈ 𝐴 , 𝑧 ∈ dom ( 𝐹 ‘ 𝑦 ) ↦ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑧 ) ) ∘ 𝐻 ) : ( 0 ..^ ( ♯ ‘ 𝐿 ) ) ⟶ 𝐶 → ( ( 𝑦 ∈ 𝐴 , 𝑧 ∈ dom ( 𝐹 ‘ 𝑦 ) ↦ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑧 ) ) ∘ 𝐻 ) ∈ Word 𝐶 )
34 32 33 syl ⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐴 , 𝑧 ∈ dom ( 𝐹 ‘ 𝑦 ) ↦ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑧 ) ) ∘ 𝐻 ) ∈ Word 𝐶 )
35 10 r19.21bi ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑦 ) ∈ ( 𝑊 ‘ ( 𝑆 ‘ 𝑦 ) ) )
36 6 ssrab3 ⊢ 𝐴 ⊆ ℙ
37 36 a1i ⊢ ( 𝜑 → 𝐴 ⊆ ℙ )
38 1 5 7 3 4 37 ablfac1b ⊢ ( 𝜑 → 𝐺 dom DProd 𝑆 )
39 1 fvexi ⊢ 𝐵 ∈ V
40 39 rabex ⊢ { 𝑥 ∈ 𝐵 ∣ ( 𝑂 ‘ 𝑥 ) ∥ ( 𝑝 ↑ ( 𝑝 pCnt ( ♯ ‘ 𝐵 ) ) ) } ∈ V
41 40 7 dmmpti ⊢ dom 𝑆 = 𝐴
42 41 a1i ⊢ ( 𝜑 → dom 𝑆 = 𝐴 )
43 38 42 dprdf2 ⊢ ( 𝜑 → 𝑆 : 𝐴 ⟶ ( SubGrp ‘ 𝐺 ) )
44 43 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑆 ‘ 𝑦 ) ∈ ( SubGrp ‘ 𝐺 ) )
45 1 2 3 4 5 6 7 8 ablfaclem1 ⊢ ( ( 𝑆 ‘ 𝑦 ) ∈ ( SubGrp ‘ 𝐺 ) → ( 𝑊 ‘ ( 𝑆 ‘ 𝑦 ) ) = { 𝑠 ∈ Word 𝐶 ∣ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = ( 𝑆 ‘ 𝑦 ) ) } )
46 44 45 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝑊 ‘ ( 𝑆 ‘ 𝑦 ) ) = { 𝑠 ∈ Word 𝐶 ∣ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = ( 𝑆 ‘ 𝑦 ) ) } )
47 35 46 eleqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑦 ) ∈ { 𝑠 ∈ Word 𝐶 ∣ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = ( 𝑆 ‘ 𝑦 ) ) } )
48 breq2 ⊢ ( 𝑠 = ( 𝐹 ‘ 𝑦 ) → ( 𝐺 dom DProd 𝑠 ↔ 𝐺 dom DProd ( 𝐹 ‘ 𝑦 ) ) )
49 oveq2 ⊢ ( 𝑠 = ( 𝐹 ‘ 𝑦 ) → ( 𝐺 DProd 𝑠 ) = ( 𝐺 DProd ( 𝐹 ‘ 𝑦 ) ) )
50 49 eqeq1d ⊢ ( 𝑠 = ( 𝐹 ‘ 𝑦 ) → ( ( 𝐺 DProd 𝑠 ) = ( 𝑆 ‘ 𝑦 ) ↔ ( 𝐺 DProd ( 𝐹 ‘ 𝑦 ) ) = ( 𝑆 ‘ 𝑦 ) ) )
51 48 50 anbi12d ⊢ ( 𝑠 = ( 𝐹 ‘ 𝑦 ) → ( ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = ( 𝑆 ‘ 𝑦 ) ) ↔ ( 𝐺 dom DProd ( 𝐹 ‘ 𝑦 ) ∧ ( 𝐺 DProd ( 𝐹 ‘ 𝑦 ) ) = ( 𝑆 ‘ 𝑦 ) ) ) )
52 51 elrab ⊢ ( ( 𝐹 ‘ 𝑦 ) ∈ { 𝑠 ∈ Word 𝐶 ∣ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = ( 𝑆 ‘ 𝑦 ) ) } ↔ ( ( 𝐹 ‘ 𝑦 ) ∈ Word 𝐶 ∧ ( 𝐺 dom DProd ( 𝐹 ‘ 𝑦 ) ∧ ( 𝐺 DProd ( 𝐹 ‘ 𝑦 ) ) = ( 𝑆 ‘ 𝑦 ) ) ) )
53 52 simprbi ⊢ ( ( 𝐹 ‘ 𝑦 ) ∈ { 𝑠 ∈ Word 𝐶 ∣ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = ( 𝑆 ‘ 𝑦 ) ) } → ( 𝐺 dom DProd ( 𝐹 ‘ 𝑦 ) ∧ ( 𝐺 DProd ( 𝐹 ‘ 𝑦 ) ) = ( 𝑆 ‘ 𝑦 ) ) )
54 47 53 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐺 dom DProd ( 𝐹 ‘ 𝑦 ) ∧ ( 𝐺 DProd ( 𝐹 ‘ 𝑦 ) ) = ( 𝑆 ‘ 𝑦 ) ) )
55 54 simpld ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → 𝐺 dom DProd ( 𝐹 ‘ 𝑦 ) )
56 dprdf ⊢ ( 𝐺 dom DProd ( 𝐹 ‘ 𝑦 ) → ( 𝐹 ‘ 𝑦 ) : dom ( 𝐹 ‘ 𝑦 ) ⟶ ( SubGrp ‘ 𝐺 ) )
57 55 56 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑦 ) : dom ( 𝐹 ‘ 𝑦 ) ⟶ ( SubGrp ‘ 𝐺 ) )
58 57 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑧 ∈ dom ( 𝐹 ‘ 𝑦 ) ) → ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑧 ) ∈ ( SubGrp ‘ 𝐺 ) )
59 58 anasss ⊢ ( ( 𝜑 ∧ ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ dom ( 𝐹 ‘ 𝑦 ) ) ) → ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑧 ) ∈ ( SubGrp ‘ 𝐺 ) )
60 57 feqmptd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑦 ) = ( 𝑧 ∈ dom ( 𝐹 ‘ 𝑦 ) ↦ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑧 ) ) )
61 55 60 breqtrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → 𝐺 dom DProd ( 𝑧 ∈ dom ( 𝐹 ‘ 𝑦 ) ↦ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑧 ) ) )
62 43 feqmptd ⊢ ( 𝜑 → 𝑆 = ( 𝑦 ∈ 𝐴 ↦ ( 𝑆 ‘ 𝑦 ) ) )
63 60 oveq2d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐺 DProd ( 𝐹 ‘ 𝑦 ) ) = ( 𝐺 DProd ( 𝑧 ∈ dom ( 𝐹 ‘ 𝑦 ) ↦ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑧 ) ) ) )
64 54 simprd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐺 DProd ( 𝐹 ‘ 𝑦 ) ) = ( 𝑆 ‘ 𝑦 ) )
65 63 64 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐺 DProd ( 𝑧 ∈ dom ( 𝐹 ‘ 𝑦 ) ↦ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑧 ) ) ) = ( 𝑆 ‘ 𝑦 ) )
66 65 mpteq2dva ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐴 ↦ ( 𝐺 DProd ( 𝑧 ∈ dom ( 𝐹 ‘ 𝑦 ) ↦ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑧 ) ) ) ) = ( 𝑦 ∈ 𝐴 ↦ ( 𝑆 ‘ 𝑦 ) ) )
67 62 66 eqtr4d ⊢ ( 𝜑 → 𝑆 = ( 𝑦 ∈ 𝐴 ↦ ( 𝐺 DProd ( 𝑧 ∈ dom ( 𝐹 ‘ 𝑦 ) ↦ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑧 ) ) ) ) )
68 38 67 breqtrd ⊢ ( 𝜑 → 𝐺 dom DProd ( 𝑦 ∈ 𝐴 ↦ ( 𝐺 DProd ( 𝑧 ∈ dom ( 𝐹 ‘ 𝑦 ) ↦ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑧 ) ) ) ) )
69 59 61 68 dprd2d2 ⊢ ( 𝜑 → ( 𝐺 dom DProd ( 𝑦 ∈ 𝐴 , 𝑧 ∈ dom ( 𝐹 ‘ 𝑦 ) ↦ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑧 ) ) ∧ ( 𝐺 DProd ( 𝑦 ∈ 𝐴 , 𝑧 ∈ dom ( 𝐹 ‘ 𝑦 ) ↦ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑧 ) ) ) = ( 𝐺 DProd ( 𝑦 ∈ 𝐴 ↦ ( 𝐺 DProd ( 𝑧 ∈ dom ( 𝐹 ‘ 𝑦 ) ↦ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑧 ) ) ) ) ) ) )
70 69 simpld ⊢ ( 𝜑 → 𝐺 dom DProd ( 𝑦 ∈ 𝐴 , 𝑧 ∈ dom ( 𝐹 ‘ 𝑦 ) ↦ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑧 ) ) )
71 28 fdmd ⊢ ( 𝜑 → dom ( 𝑦 ∈ 𝐴 , 𝑧 ∈ dom ( 𝐹 ‘ 𝑦 ) ↦ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑧 ) ) = 𝐿 )
72 70 71 12 dprdf1o ⊢ ( 𝜑 → ( 𝐺 dom DProd ( ( 𝑦 ∈ 𝐴 , 𝑧 ∈ dom ( 𝐹 ‘ 𝑦 ) ↦ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑧 ) ) ∘ 𝐻 ) ∧ ( 𝐺 DProd ( ( 𝑦 ∈ 𝐴 , 𝑧 ∈ dom ( 𝐹 ‘ 𝑦 ) ↦ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑧 ) ) ∘ 𝐻 ) ) = ( 𝐺 DProd ( 𝑦 ∈ 𝐴 , 𝑧 ∈ dom ( 𝐹 ‘ 𝑦 ) ↦ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑧 ) ) ) ) )
73 72 simpld ⊢ ( 𝜑 → 𝐺 dom DProd ( ( 𝑦 ∈ 𝐴 , 𝑧 ∈ dom ( 𝐹 ‘ 𝑦 ) ↦ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑧 ) ) ∘ 𝐻 ) )
74 72 simprd ⊢ ( 𝜑 → ( 𝐺 DProd ( ( 𝑦 ∈ 𝐴 , 𝑧 ∈ dom ( 𝐹 ‘ 𝑦 ) ↦ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑧 ) ) ∘ 𝐻 ) ) = ( 𝐺 DProd ( 𝑦 ∈ 𝐴 , 𝑧 ∈ dom ( 𝐹 ‘ 𝑦 ) ↦ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑧 ) ) ) )
75 69 simprd ⊢ ( 𝜑 → ( 𝐺 DProd ( 𝑦 ∈ 𝐴 , 𝑧 ∈ dom ( 𝐹 ‘ 𝑦 ) ↦ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑧 ) ) ) = ( 𝐺 DProd ( 𝑦 ∈ 𝐴 ↦ ( 𝐺 DProd ( 𝑧 ∈ dom ( 𝐹 ‘ 𝑦 ) ↦ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑧 ) ) ) ) ) )
76 67 oveq2d ⊢ ( 𝜑 → ( 𝐺 DProd 𝑆 ) = ( 𝐺 DProd ( 𝑦 ∈ 𝐴 ↦ ( 𝐺 DProd ( 𝑧 ∈ dom ( 𝐹 ‘ 𝑦 ) ↦ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑧 ) ) ) ) ) )
77 ssidd ⊢ ( 𝜑 → 𝐴 ⊆ 𝐴 )
78 1 5 7 3 4 37 6 77 ablfac1c ⊢ ( 𝜑 → ( 𝐺 DProd 𝑆 ) = 𝐵 )
79 76 78 eqtr3d ⊢ ( 𝜑 → ( 𝐺 DProd ( 𝑦 ∈ 𝐴 ↦ ( 𝐺 DProd ( 𝑧 ∈ dom ( 𝐹 ‘ 𝑦 ) ↦ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑧 ) ) ) ) ) = 𝐵 )
80 74 75 79 3eqtrd ⊢ ( 𝜑 → ( 𝐺 DProd ( ( 𝑦 ∈ 𝐴 , 𝑧 ∈ dom ( 𝐹 ‘ 𝑦 ) ↦ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑧 ) ) ∘ 𝐻 ) ) = 𝐵 )
81 breq2 ⊢ ( 𝑠 = ( ( 𝑦 ∈ 𝐴 , 𝑧 ∈ dom ( 𝐹 ‘ 𝑦 ) ↦ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑧 ) ) ∘ 𝐻 ) → ( 𝐺 dom DProd 𝑠 ↔ 𝐺 dom DProd ( ( 𝑦 ∈ 𝐴 , 𝑧 ∈ dom ( 𝐹 ‘ 𝑦 ) ↦ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑧 ) ) ∘ 𝐻 ) ) )
82 oveq2 ⊢ ( 𝑠 = ( ( 𝑦 ∈ 𝐴 , 𝑧 ∈ dom ( 𝐹 ‘ 𝑦 ) ↦ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑧 ) ) ∘ 𝐻 ) → ( 𝐺 DProd 𝑠 ) = ( 𝐺 DProd ( ( 𝑦 ∈ 𝐴 , 𝑧 ∈ dom ( 𝐹 ‘ 𝑦 ) ↦ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑧 ) ) ∘ 𝐻 ) ) )
83 82 eqeq1d ⊢ ( 𝑠 = ( ( 𝑦 ∈ 𝐴 , 𝑧 ∈ dom ( 𝐹 ‘ 𝑦 ) ↦ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑧 ) ) ∘ 𝐻 ) → ( ( 𝐺 DProd 𝑠 ) = 𝐵 ↔ ( 𝐺 DProd ( ( 𝑦 ∈ 𝐴 , 𝑧 ∈ dom ( 𝐹 ‘ 𝑦 ) ↦ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑧 ) ) ∘ 𝐻 ) ) = 𝐵 ) )
84 81 83 anbi12d ⊢ ( 𝑠 = ( ( 𝑦 ∈ 𝐴 , 𝑧 ∈ dom ( 𝐹 ‘ 𝑦 ) ↦ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑧 ) ) ∘ 𝐻 ) → ( ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) ↔ ( 𝐺 dom DProd ( ( 𝑦 ∈ 𝐴 , 𝑧 ∈ dom ( 𝐹 ‘ 𝑦 ) ↦ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑧 ) ) ∘ 𝐻 ) ∧ ( 𝐺 DProd ( ( 𝑦 ∈ 𝐴 , 𝑧 ∈ dom ( 𝐹 ‘ 𝑦 ) ↦ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑧 ) ) ∘ 𝐻 ) ) = 𝐵 ) ) )
85 84 rspcev ⊢ ( ( ( ( 𝑦 ∈ 𝐴 , 𝑧 ∈ dom ( 𝐹 ‘ 𝑦 ) ↦ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑧 ) ) ∘ 𝐻 ) ∈ Word 𝐶 ∧ ( 𝐺 dom DProd ( ( 𝑦 ∈ 𝐴 , 𝑧 ∈ dom ( 𝐹 ‘ 𝑦 ) ↦ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑧 ) ) ∘ 𝐻 ) ∧ ( 𝐺 DProd ( ( 𝑦 ∈ 𝐴 , 𝑧 ∈ dom ( 𝐹 ‘ 𝑦 ) ↦ ( ( 𝐹 ‘ 𝑦 ) ‘ 𝑧 ) ) ∘ 𝐻 ) ) = 𝐵 ) ) → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) )
86 34 73 80 85 syl12anc ⊢ ( 𝜑 → ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) )
87 rabn0 ⊢ ( { 𝑠 ∈ Word 𝐶 ∣ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) } ≠ ∅ ↔ ∃ 𝑠 ∈ Word 𝐶 ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) )
88 86 87 sylibr ⊢ ( 𝜑 → { 𝑠 ∈ Word 𝐶 ∣ ( 𝐺 dom DProd 𝑠 ∧ ( 𝐺 DProd 𝑠 ) = 𝐵 ) } ≠ ∅ )
89 16 88 eqnetrd ⊢ ( 𝜑 → ( 𝑊 ‘ 𝐵 ) ≠ ∅ )