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	ffvelrnda	$⊢ (((φ \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	31	rexeqdv	$⊢ (((φ \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))} \leftrightarrow \exists x \in {Base}_{(G ↾_{𝑠} s (k))} ran (n \in ℤ ⟼ n \cdot_{(G ↾_{𝑠} s (k))} x) = {Base}_{(G ↾_{𝑠} s (k))})$
33	28 32	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 \cdot_{(G ↾_{𝑠} s (k))} x) = {Base}_{(G ↾_{𝑠} s (k))}$
34	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)$
35		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 ℤ$
36		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)$
37	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$
38	34 35 36 37	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$
39	38	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)$
40	39	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)$
41	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))}$
42	40 41	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))})$
43	42	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))})$
44	33 43	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)$
45		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))$
46	20 44 45	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)$
47	46	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)$
48		oveq2	$⊢ x = w (k) \to n \underset{˙}{\cdot} x = n \underset{˙}{\cdot} w (k)$
49	48	mpteq2dv	$⊢ x = w (k) \to (n \in ℤ ⟼ n \underset{˙}{\cdot} x) = (n \in ℤ ⟼ n \underset{˙}{\cdot} w (k))$
50	49	rneqd	$⊢ x = w (k) \to ran (n \in ℤ ⟼ n \underset{˙}{\cdot} x) = ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (k))$
51	50	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))$
52	51	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))$
53	11 47 52	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))$
54		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$
55	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\|)$
56	55	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)$
57	54 56	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$
58		iswrdi	$⊢ w : (0 ..^\|s\|) ⟶ B \to w \in Word B$
59	57 58	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$
60	54	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$
61	60	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)$
62	61	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$
63		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)$
64		simpl	$⊢ (k = j \land n \in ℤ) \to k = j$
65	64	fveq2d	$⊢ (k = j \land n \in ℤ) \to w (k) = w (j)$
66	65	oveq2d	$⊢ (k = j \land n \in ℤ) \to n \underset{˙}{\cdot} w (k) = n \underset{˙}{\cdot} w (j)$
67	66	mpteq2dva	$⊢ k = j \to (n \in ℤ ⟼ n \underset{˙}{\cdot} w (k)) = (n \in ℤ ⟼ n \underset{˙}{\cdot} w (j))$
68	67	rneqd	$⊢ k = j \to ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (k)) = ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (j))$
69		fveq2	$⊢ k = j \to s (k) = s (j)$
70	68 69	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))$
71	70	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)$
72	63 71	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)$
73	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$
74	73	ffvelrnda	$⊢ ((((φ \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$
75	72 74	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$
76	62 75	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$
77		fveq2	$⊢ k = j \to w (k) = w (j)$
78	77	oveq2d	$⊢ k = j \to n \underset{˙}{\cdot} w (k) = n \underset{˙}{\cdot} w (j)$
79	78	mpteq2dv	$⊢ k = j \to (n \in ℤ ⟼ n \underset{˙}{\cdot} w (k)) = (n \in ℤ ⟼ n \underset{˙}{\cdot} w (j))$
80	79	rneqd	$⊢ k = j \to ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (k)) = ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (j))$
81	80	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)))$
82	6 81	eqtri	$⊢ S = (j \in dom w ⟼ ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (j)))$
83	76 82	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$
84		simprl	$⊢ ((φ \land s \in Word C) \land (G dom DProd s \land G DProd s = B)) \to G dom DProd s$
85	84	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$
86	60	raleqdv	$⊢ (((φ \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) \leftrightarrow \forall k \in dom s ran (n \in ℤ ⟼ n \underset{˙}{\cdot} w (k)) = s (k))$
87	63 86	mpbird	$⊢ (((φ \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)$
88		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))$
89	60 87 88	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))$
90	6 89	syl5eq	$⊢ (((φ \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))$
91		dprdf	$⊢ G dom DProd s \to s : dom s ⟶ SubGrp (G)$
92	85 91	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)$
93	92	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))$
94	90 93	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$
95	85 94	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$
96	94	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$
97		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$
98	96 97	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$
99	83 95 98	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)$
100	59 99	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))$
101	100	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)))$
102	101	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)))$
103	53 102	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))$
104		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))$
105	103 104	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)$
106	1 2 3 4	ablfac	$⊢ φ \to \exists s \in Word C (G dom DProd s \land G DProd s = B)$
107	105 106	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