ablfac2

Description: Choose generators for each cyclic group in ablfac . (Contributed by Mario Carneiro, 28-Apr-2016)

	Ref	Expression
Hypotheses	ablfac.b	$⊢ B = {Base}_{G}$
	ablfac.c	$⊢ C = \{r \in SubGrp (G) \| G ↾_{𝑠} r \in (CycGrp \cap ran pGrp)\}$
	ablfac.1	$⊢ φ \to G \in Abel$
	ablfac.2	$⊢ φ \to B \in Fin$
	ablfac2.m	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
	ablfac2.s	$⊢ S = (k \in dom w ⟼ ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (k)))$
Assertion	ablfac2	$⊢ φ \to \exists w \in Word B (S : dom w ⟶ C \land G dom DProd S \land G DProd S = B)$

Proof

Step	Hyp	Ref	Expression
1		ablfac.b	$⊢ B = {Base}_{G}$
2		ablfac.c	$⊢ C = \{r \in SubGrp (G) \| G ↾_{𝑠} r \in (CycGrp \cap ran pGrp)\}$
3		ablfac.1	$⊢ φ \to G \in Abel$
4		ablfac.2	$⊢ φ \to B \in Fin$
5		ablfac2.m	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
6		ablfac2.s	$⊢ S = (k \in dom w ⟼ ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (k)))$
7		wrdf	$⊢ s \in Word C \to s : (0 ..^\|s\|) ⟶ C$
8	7	ad2antlr	$⊢ ((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \to s : (0 ..^\|s\|) ⟶ C$
9	8	fdmd	$⊢ ((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \to dom s = (0 ..^\|s\|)$
10		fzofi	$⊢ (0 ..^\|s\|) \in Fin$
11	9 10	eqeltrdi	$⊢ ((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \to dom s \in Fin$
12	8	ffdmd	$⊢ ((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \to s : dom s ⟶ C$
13	12	ffvelcdmda	$⊢ (((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \land k \in dom s) \to s (k) \in C$
14		oveq2	$⊢ r = s (k) \to G ↾_{𝑠} r = G ↾_{𝑠} s (k)$
15	14	eleq1d	$⊢ r = s (k) \to (G ↾_{𝑠} r \in (CycGrp \cap ran pGrp) \leftrightarrow G ↾_{𝑠} s (k) \in (CycGrp \cap ran pGrp))$
16	15 2	elrab2	$⊢ s (k) \in C \leftrightarrow (s (k) \in SubGrp (G) \land G ↾_{𝑠} s (k) \in (CycGrp \cap ran pGrp))$
17	16	simplbi	$⊢ s (k) \in C \to s (k) \in SubGrp (G)$
18	13 17	syl	$⊢ (((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \land k \in dom s) \to s (k) \in SubGrp (G)$
19	1	subgss	$⊢ s (k) \in SubGrp (G) \to s (k) \subseteq B$
20	18 19	syl	$⊢ (((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \land k \in dom s) \to s (k) \subseteq B$
21	16	simprbi	$⊢ s (k) \in C \to G ↾_{𝑠} s (k) \in (CycGrp \cap ran pGrp)$
22	13 21	syl	$⊢ (((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \land k \in dom s) \to G ↾_{𝑠} s (k) \in (CycGrp \cap ran pGrp)$
23	22	elin1d	$⊢ (((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \land k \in dom s) \to G ↾_{𝑠} s (k) \in CycGrp$
24		eqid	$⊢ {Base}_{(G ↾_{𝑠} s (k))} = {Base}_{(G ↾_{𝑠} s (k))}$
25		eqid	$⊢ \cdot_{(G ↾_{𝑠} s (k))} = \cdot_{(G ↾_{𝑠} s (k))}$
26	24 25	iscyg	$⊢ G ↾_{𝑠} s (k) \in CycGrp \leftrightarrow (G ↾_{𝑠} s (k) \in Grp \land \exists x \in {Base}_{(G ↾_{𝑠} s (k))} ran (n \in ℤ ⟼ n \cdot_{(G ↾_{𝑠} s (k))} x) = {Base}_{(G ↾_{𝑠} s (k))})$
27	26	simprbi	$⊢ G ↾_{𝑠} s (k) \in CycGrp \to \exists x \in {Base}_{(G ↾_{𝑠} s (k))} ran (n \in ℤ ⟼ n \cdot_{(G ↾_{𝑠} s (k))} x) = {Base}_{(G ↾_{𝑠} s (k))}$
28	23 27	syl	$⊢ (((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \land k \in dom s) \to \exists x \in {Base}_{(G ↾_{𝑠} s (k))} ran (n \in ℤ ⟼ n \cdot_{(G ↾_{𝑠} s (k))} x) = {Base}_{(G ↾_{𝑠} s (k))}$
29		eqid	$⊢ G ↾_{𝑠} s (k) = G ↾_{𝑠} s (k)$
30	29	subgbas	$⊢ s (k) \in SubGrp (G) \to s (k) = {Base}_{(G ↾_{𝑠} s (k))}$
31	18 30	syl	$⊢ (((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \land k \in dom s) \to s (k) = {Base}_{(G ↾_{𝑠} s (k))}$
32	28 31	rexeqtrrdv	$⊢ (((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \land k \in dom s) \to \exists x \in s (k) ran (n \in ℤ ⟼ n \cdot_{(G ↾_{𝑠} s (k))} x) = {Base}_{(G ↾_{𝑠} s (k))}$
33	18	ad2antrr	$⊢ (((((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \land k \in dom s) \land x \in s (k)) \land n \in ℤ) \to s (k) \in SubGrp (G)$
34		simpr	$⊢ (((((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \land k \in dom s) \land x \in s (k)) \land n \in ℤ) \to n \in ℤ$
35		simplr	$⊢ (((((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \land k \in dom s) \land x \in s (k)) \land n \in ℤ) \to x \in s (k)$
36	5 29 25	subgmulg	$⊢ (s (k) \in SubGrp (G) \land n \in ℤ \land x \in s (k)) \to n \underset{˙}{\cdot} x = n \cdot_{(G ↾_{𝑠} s (k))} x$
37	33 34 35 36	syl3anc	$⊢ (((((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \land k \in dom s) \land x \in s (k)) \land n \in ℤ) \to n \underset{˙}{\cdot} x = n \cdot_{(G ↾_{𝑠} s (k))} x$
38	37	mpteq2dva	$⊢ ((((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \land k \in dom s) \land x \in s (k)) \to (n \in ℤ ⟼ n \underset{˙}{\cdot} x) = (n \in ℤ ⟼ n \cdot_{(G ↾_{𝑠} s (k))} x)$
39	38	rneqd	$⊢ ((((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \land k \in dom s) \land x \in s (k)) \to ran (n \in ℤ ⟼ n \underset{˙}{\cdot} x) = ran (n \in ℤ ⟼ n \cdot_{(G ↾_{𝑠} s (k))} x)$
40	31	adantr	$⊢ ((((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \land k \in dom s) \land x \in s (k)) \to s (k) = {Base}_{(G ↾_{𝑠} s (k))}$
41	39 40	eqeq12d	$⊢ ((((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \land k \in dom s) \land x \in s (k)) \to (ran (n \in ℤ ⟼ n \underset{˙}{\cdot} x) = s (k) \leftrightarrow ran (n \in ℤ ⟼ n \cdot_{(G ↾_{𝑠} s (k))} x) = {Base}_{(G ↾_{𝑠} s (k))})$
42	41	rexbidva	$⊢ (((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \land k \in dom s) \to (\exists x \in s (k) ran (n \in ℤ ⟼ n \underset{˙}{\cdot} x) = s (k) \leftrightarrow \exists x \in s (k) ran (n \in ℤ ⟼ n \cdot_{(G ↾_{𝑠} s (k))} x) = {Base}_{(G ↾_{𝑠} s (k))})$
43	32 42	mpbird	$⊢ (((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \land k \in dom s) \to \exists x \in s (k) ran (n \in ℤ ⟼ n \underset{˙}{\cdot} x) = s (k)$
44		ssrexv	$⊢ s (k) \subseteq B \to (\exists x \in s (k) ran (n \in ℤ ⟼ n \underset{˙}{\cdot} x) = s (k) \to \exists x \in B ran (n \in ℤ ⟼ n \underset{˙}{\cdot} x) = s (k))$
45	20 43 44	sylc	$⊢ (((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \land k \in dom s) \to \exists x \in B ran (n \in ℤ ⟼ n \underset{˙}{\cdot} x) = s (k)$
46	45	ralrimiva	$⊢ ((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \to \forall k \in dom s \exists x \in B ran (n \in ℤ ⟼ n \underset{˙}{\cdot} x) = s (k)$
47		oveq2	$⊢ x = w (k) \to n \underset{˙}{\cdot} x = n \underset{˙}{\cdot} w (k)$
48	47	mpteq2dv	$⊢ x = w (k) \to (n \in ℤ ⟼ n \underset{˙}{\cdot} x) = (n \in ℤ ⟼ n \underset{˙}{\cdot} w (k))$
49	48	rneqd	$⊢ x = w (k) \to ran (n \in ℤ ⟼ n \underset{˙}{\cdot} x) = ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (k))$
50	49	eqeq1d	$⊢ x = w (k) \to (ran (n \in ℤ ⟼ n \underset{˙}{\cdot} x) = s (k) \leftrightarrow ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (k)) = s (k))$
51	50	ac6sfi	$⊢ (dom s \in Fin \land \forall k \in dom s \exists x \in B ran (n \in ℤ ⟼ n \underset{˙}{\cdot} x) = s (k)) \to \exists w (w : dom s ⟶ B \land \forall k \in dom s ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (k)) = s (k))$
52	11 46 51	syl2anc	$⊢ ((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \to \exists w (w : dom s ⟶ B \land \forall k \in dom s ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (k)) = s (k))$
53		simprl	$⊢ (((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \land (w : dom s ⟶ B \land \forall k \in dom s ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (k)) = s (k))) \to w : dom s ⟶ B$
54	9	adantr	$⊢ (((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \land (w : dom s ⟶ B \land \forall k \in dom s ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (k)) = s (k))) \to dom s = (0 ..^\|s\|)$
55	54	feq2d	$⊢ (((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \land (w : dom s ⟶ B \land \forall k \in dom s ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (k)) = s (k))) \to (w : dom s ⟶ B \leftrightarrow w : (0 ..^\|s\|) ⟶ B)$
56	53 55	mpbid	$⊢ (((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \land (w : dom s ⟶ B \land \forall k \in dom s ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (k)) = s (k))) \to w : (0 ..^\|s\|) ⟶ B$
57		iswrdi	$⊢ w : (0 ..^\|s\|) ⟶ B \to w \in Word B$
58	56 57	syl	$⊢ (((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \land (w : dom s ⟶ B \land \forall k \in dom s ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (k)) = s (k))) \to w \in Word B$
59	53	fdmd	$⊢ (((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \land (w : dom s ⟶ B \land \forall k \in dom s ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (k)) = s (k))) \to dom w = dom s$
60	59	eleq2d	$⊢ (((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \land (w : dom s ⟶ B \land \forall k \in dom s ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (k)) = s (k))) \to (j \in dom w \leftrightarrow j \in dom s)$
61	60	biimpa	$⊢ ((((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \land (w : dom s ⟶ B \land \forall k \in dom s ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (k)) = s (k))) \land j \in dom w) \to j \in dom s$
62		simprr	$⊢ (((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \land (w : dom s ⟶ B \land \forall k \in dom s ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (k)) = s (k))) \to \forall k \in dom s ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (k)) = s (k)$
63		simpl	$⊢ (k = j \land n \in ℤ) \to k = j$
64	63	fveq2d	$⊢ (k = j \land n \in ℤ) \to w (k) = w (j)$
65	64	oveq2d	$⊢ (k = j \land n \in ℤ) \to n \underset{˙}{\cdot} w (k) = n \underset{˙}{\cdot} w (j)$
66	65	mpteq2dva	$⊢ k = j \to (n \in ℤ ⟼ n \underset{˙}{\cdot} w (k)) = (n \in ℤ ⟼ n \underset{˙}{\cdot} w (j))$
67	66	rneqd	$⊢ k = j \to ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (k)) = ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (j))$
68		fveq2	$⊢ k = j \to s (k) = s (j)$
69	67 68	eqeq12d	$⊢ k = j \to (ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (k)) = s (k) \leftrightarrow ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (j)) = s (j))$
70	69	rspccva	$⊢ (\forall k \in dom s ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (k)) = s (k) \land j \in dom s) \to ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (j)) = s (j)$
71	62 70	sylan	$⊢ ((((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \land (w : dom s ⟶ B \land \forall k \in dom s ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (k)) = s (k))) \land j \in dom s) \to ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (j)) = s (j)$
72	12	adantr	$⊢ (((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \land (w : dom s ⟶ B \land \forall k \in dom s ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (k)) = s (k))) \to s : dom s ⟶ C$
73	72	ffvelcdmda	$⊢ ((((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \land (w : dom s ⟶ B \land \forall k \in dom s ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (k)) = s (k))) \land j \in dom s) \to s (j) \in C$
74	71 73	eqeltrd	$⊢ ((((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \land (w : dom s ⟶ B \land \forall k \in dom s ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (k)) = s (k))) \land j \in dom s) \to ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (j)) \in C$
75	61 74	syldan	$⊢ ((((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \land (w : dom s ⟶ B \land \forall k \in dom s ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (k)) = s (k))) \land j \in dom w) \to ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (j)) \in C$
76		fveq2	$⊢ k = j \to w (k) = w (j)$
77	76	oveq2d	$⊢ k = j \to n \underset{˙}{\cdot} w (k) = n \underset{˙}{\cdot} w (j)$
78	77	mpteq2dv	$⊢ k = j \to (n \in ℤ ⟼ n \underset{˙}{\cdot} w (k)) = (n \in ℤ ⟼ n \underset{˙}{\cdot} w (j))$
79	78	rneqd	$⊢ k = j \to ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (k)) = ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (j))$
80	79	cbvmptv	$⊢ (k \in dom w ⟼ ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (k))) = (j \in dom w ⟼ ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (j)))$
81	6 80	eqtri	$⊢ S = (j \in dom w ⟼ ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (j)))$
82	75 81	fmptd	$⊢ (((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \land (w : dom s ⟶ B \land \forall k \in dom s ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (k)) = s (k))) \to S : dom w ⟶ C$
83		simprl	$⊢ ((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \to G dom DProd s$
84	83	adantr	$⊢ (((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \land (w : dom s ⟶ B \land \forall k \in dom s ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (k)) = s (k))) \to G dom DProd s$
85	62 59	raleqtrrdv	$⊢ (((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \land (w : dom s ⟶ B \land \forall k \in dom s ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (k)) = s (k))) \to \forall k \in dom w ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (k)) = s (k)$
86		mpteq12	$⊢ (dom w = dom s \land \forall k \in dom w ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (k)) = s (k)) \to (k \in dom w ⟼ ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (k))) = (k \in dom s ⟼ s (k))$
87	59 85 86	syl2anc	$⊢ (((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \land (w : dom s ⟶ B \land \forall k \in dom s ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (k)) = s (k))) \to (k \in dom w ⟼ ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (k))) = (k \in dom s ⟼ s (k))$
88	6 87	eqtrid	$⊢ (((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \land (w : dom s ⟶ B \land \forall k \in dom s ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (k)) = s (k))) \to S = (k \in dom s ⟼ s (k))$
89		dprdf	$⊢ G dom DProd s \to s : dom s ⟶ SubGrp (G)$
90	84 89	syl	$⊢ (((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \land (w : dom s ⟶ B \land \forall k \in dom s ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (k)) = s (k))) \to s : dom s ⟶ SubGrp (G)$
91	90	feqmptd	$⊢ (((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \land (w : dom s ⟶ B \land \forall k \in dom s ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (k)) = s (k))) \to s = (k \in dom s ⟼ s (k))$
92	88 91	eqtr4d	$⊢ (((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \land (w : dom s ⟶ B \land \forall k \in dom s ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (k)) = s (k))) \to S = s$
93	84 92	breqtrrd	$⊢ (((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \land (w : dom s ⟶ B \land \forall k \in dom s ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (k)) = s (k))) \to G dom DProd S$
94	92	oveq2d	$⊢ (((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \land (w : dom s ⟶ B \land \forall k \in dom s ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (k)) = s (k))) \to G DProd S = G DProd s$
95		simplrr	$⊢ (((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \land (w : dom s ⟶ B \land \forall k \in dom s ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (k)) = s (k))) \to G DProd s = B$
96	94 95	eqtrd	$⊢ (((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \land (w : dom s ⟶ B \land \forall k \in dom s ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (k)) = s (k))) \to G DProd S = B$
97	82 93 96	3jca	$⊢ (((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \land (w : dom s ⟶ B \land \forall k \in dom s ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (k)) = s (k))) \to (S : dom w ⟶ C \land G dom DProd S \land G DProd S = B)$
98	58 97	jca	$⊢ (((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \land (w : dom s ⟶ B \land \forall k \in dom s ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (k)) = s (k))) \to (w \in Word B \land (S : dom w ⟶ C \land G dom DProd S \land G DProd S = B))$
99	98	ex	$⊢ ((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \to ((w : dom s ⟶ B \land \forall k \in dom s ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (k)) = s (k)) \to (w \in Word B \land (S : dom w ⟶ C \land G dom DProd S \land G DProd S = B)))$
100	99	eximdv	$⊢ ((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \to (\exists w (w : dom s ⟶ B \land \forall k \in dom s ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (k)) = s (k)) \to \exists w (w \in Word B \land (S : dom w ⟶ C \land G dom DProd S \land G DProd S = B)))$
101	52 100	mpd	$⊢ ((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \to \exists w (w \in Word B \land (S : dom w ⟶ C \land G dom DProd S \land G DProd S = B))$
102		df-rex	$⊢ \exists w \in Word B (S : dom w ⟶ C \land G dom DProd S \land G DProd S = B) \leftrightarrow \exists w (w \in Word B \land (S : dom w ⟶ C \land G dom DProd S \land G DProd S = B))$
103	101 102	sylibr	$⊢ ((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \to \exists w \in Word B (S : dom w ⟶ C \land G dom DProd S \land G DProd S = B)$
104	1 2 3 4	ablfac	$⊢ φ \to \exists s \in Word C (G dom DProd s \land G DProd s = B)$
105	103 104	r19.29a	$⊢ φ \to \exists w \in Word B (S : dom w ⟶ C \land G dom DProd S \land G DProd S = B)$

Metamath Proof Explorer

Theorem ablfac2

Proof