aks6d1c1

	Ref	Expression
Hypotheses	aks6d1c1.1	$⊢ \underset{˙}{\sim} = \{⟨e, f⟩ \| (e \in ℕ \land f \in B \land \forall y \in (V PrimRoots R) e \underset{˙}{\times} O (f) (y) = O (f) (e \underset{˙}{\times} y))\}$
	aks6d1c1.2	$⊢ S = {Poly}_{1} (K)$
	aks6d1c1.3	$⊢ B = {Base}_{S}$
	aks6d1c1.4	$⊢ X = {var}_{1} (K)$
	aks6d1c1.5	$⊢ W = {mulGrp}_{S}$
	aks6d1c1.6	$⊢ V = {mulGrp}_{K}$
	aks6d1c1.7	$⊢ \underset{˙}{\times} = \cdot_{V}$
	aks6d1c1.8	$⊢ C = algSc (S)$
	aks6d1c1.9	$⊢ D = \cdot_{W}$
	aks6d1c1.10	$⊢ P = chr (K)$
	aks6d1c1.11	$⊢ O = {eval}_{1} (K)$
	aks6d1c1.12	$⊢ \underset{˙}{+} = +_{S}$
	aks6d1c1.13	$⊢ φ \to K \in Field$
	aks6d1c1.14	$⊢ φ \to P \in ℙ$
	aks6d1c1.15	$⊢ φ \to R \in ℕ$
	aks6d1c1.16	$⊢ φ \to N \in ℕ$
	aks6d1c1.17	$⊢ φ \to P ∥ N$
	aks6d1c1.18	$⊢ φ \to N \gcd R = 1$
	aks6d1c1.19	$⊢ φ \to F : (0 \dots A) ⟶ ℕ_{0}$
	aks6d1c1.20	$⊢ G = (g \in ({ℕ_{0}}^{(0 \dots A)}) ⟼ {\sum_{W}}_{i = 0}^{A} (g (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))$
	aks6d1c1.21	$⊢ φ \to A \in ℕ_{0}$
	aks6d1c1.22	$⊢ φ \to U \in ℕ_{0}$
	aks6d1c1.23	$⊢ φ \to L \in ℕ_{0}$
	aks6d1c1.24	$⊢ E = P^{U} {(\frac{N}{P})}^{L}$
	aks6d1c1.25	$⊢ φ \to \forall a \in (1 \dots A) N \underset{˙}{\sim} (X \underset{˙}{+} C (ℤRHom (K) (a)))$
	aks6d1c1.26	$⊢ φ \to (x \in {Base}_{K} ⟼ P \underset{˙}{\times} x) \in (K RingIso K)$
Assertion	aks6d1c1	$⊢ φ \to E \underset{˙}{\sim} G (F)$

Proof

Step	Hyp	Ref	Expression
1		aks6d1c1.1	$⊢ \underset{˙}{\sim} = \{⟨e, f⟩ \| (e \in ℕ \land f \in B \land \forall y \in (V PrimRoots R) e \underset{˙}{\times} O (f) (y) = O (f) (e \underset{˙}{\times} y))\}$
2		aks6d1c1.2	$⊢ S = {Poly}_{1} (K)$
3		aks6d1c1.3	$⊢ B = {Base}_{S}$
4		aks6d1c1.4	$⊢ X = {var}_{1} (K)$
5		aks6d1c1.5	$⊢ W = {mulGrp}_{S}$
6		aks6d1c1.6	$⊢ V = {mulGrp}_{K}$
7		aks6d1c1.7	$⊢ \underset{˙}{\times} = \cdot_{V}$
8		aks6d1c1.8	$⊢ C = algSc (S)$
9		aks6d1c1.9	$⊢ D = \cdot_{W}$
10		aks6d1c1.10	$⊢ P = chr (K)$
11		aks6d1c1.11	$⊢ O = {eval}_{1} (K)$
12		aks6d1c1.12	$⊢ \underset{˙}{+} = +_{S}$
13		aks6d1c1.13	$⊢ φ \to K \in Field$
14		aks6d1c1.14	$⊢ φ \to P \in ℙ$
15		aks6d1c1.15	$⊢ φ \to R \in ℕ$
16		aks6d1c1.16	$⊢ φ \to N \in ℕ$
17		aks6d1c1.17	$⊢ φ \to P ∥ N$
18		aks6d1c1.18	$⊢ φ \to N \gcd R = 1$
19		aks6d1c1.19	$⊢ φ \to F : (0 \dots A) ⟶ ℕ_{0}$
20		aks6d1c1.20	$⊢ G = (g \in ({ℕ_{0}}^{(0 \dots A)}) ⟼ {\sum_{W}}_{i = 0}^{A} (g (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))$
21		aks6d1c1.21	$⊢ φ \to A \in ℕ_{0}$
22		aks6d1c1.22	$⊢ φ \to U \in ℕ_{0}$
23		aks6d1c1.23	$⊢ φ \to L \in ℕ_{0}$
24		aks6d1c1.24	$⊢ E = P^{U} {(\frac{N}{P})}^{L}$
25		aks6d1c1.25	$⊢ φ \to \forall a \in (1 \dots A) N \underset{˙}{\sim} (X \underset{˙}{+} C (ℤRHom (K) (a)))$
26		aks6d1c1.26	$⊢ φ \to (x \in {Base}_{K} ⟼ P \underset{˙}{\times} x) \in (K RingIso K)$
27	21	nn0zd	$⊢ φ \to A \in ℤ$
28	21	nn0ge0d	$⊢ φ \to 0 \leq A$
29	21	nn0red	$⊢ φ \to A \in ℝ$
30	29	leidd	$⊢ φ \to A \leq A$
31	27 28 30	3jca	$⊢ φ \to (A \in ℤ \land 0 \leq A \land A \leq A)$
32		oveq2	$⊢ h = 0 \to (0 \dots h) = (0 \dots 0)$
33	32	mpteq1d	$⊢ h = 0 \to (i \in (0 \dots h) ⟼ F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))) = (i \in (0 \dots 0) ⟼ F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i))))$
34	33	oveq2d	$⊢ h = 0 \to {\sum_{W}}_{i = 0}^{h} (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))) = {\sum_{W}}_{i = 0}^{0} (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i))))$
35	34	breq2d	$⊢ h = 0 \to (E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{h}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i))))) \leftrightarrow E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{0}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i))))))$
36		oveq2	$⊢ h = j \to (0 \dots h) = (0 \dots j)$
37	36	mpteq1d	$⊢ h = j \to (i \in (0 \dots h) ⟼ F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))) = (i \in (0 \dots j) ⟼ F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i))))$
38	37	oveq2d	$⊢ h = j \to {\sum_{W}}_{i = 0}^{h} (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))) = {\sum_{W}}_{i = 0}^{j} (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i))))$
39	38	breq2d	$⊢ h = j \to (E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{h}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i))))) \leftrightarrow E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i))))))$
40		oveq2	$⊢ h = j + 1 \to (0 \dots h) = (0 \dots j + 1)$
41	40	mpteq1d	$⊢ h = j + 1 \to (i \in (0 \dots h) ⟼ F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))) = (i \in (0 \dots j + 1) ⟼ F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i))))$
42	41	oveq2d	$⊢ h = j + 1 \to {\sum_{W}}_{i = 0}^{h} (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))) = {\sum_{W}}_{i = 0}^{j + 1} (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i))))$
43	42	breq2d	$⊢ h = j + 1 \to (E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{h}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i))))) \leftrightarrow E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j + 1}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i))))))$
44		oveq2	$⊢ h = A \to (0 \dots h) = (0 \dots A)$
45	44	mpteq1d	$⊢ h = A \to (i \in (0 \dots h) ⟼ F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))) = (i \in (0 \dots A) ⟼ F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i))))$
46	45	oveq2d	$⊢ h = A \to {\sum_{W}}_{i = 0}^{h} (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))) = {\sum_{W}}_{i = 0}^{A} (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i))))$
47	46	breq2d	$⊢ h = A \to (E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{h}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i))))) \leftrightarrow E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{A}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i))))))$
48		prmnn	$⊢ P \in ℙ \to P \in ℕ$
49	14 48	syl	$⊢ φ \to P \in ℕ$
50	49 22	nnexpcld	$⊢ φ \to P^{U} \in ℕ$
51	49	nnzd	$⊢ φ \to P \in ℤ$
52	49	nnne0d	$⊢ φ \to P \neq 0$
53	16	nnzd	$⊢ φ \to N \in ℤ$
54		dvdsval2	$⊢ (P \in ℤ \land P \neq 0 \land N \in ℤ) \to (P ∥ N \leftrightarrow \frac{N}{P} \in ℤ)$
55	51 52 53 54	syl3anc	$⊢ φ \to (P ∥ N \leftrightarrow \frac{N}{P} \in ℤ)$
56	17 55	mpbid	$⊢ φ \to \frac{N}{P} \in ℤ$
57	16	nnred	$⊢ φ \to N \in ℝ$
58	49	nnred	$⊢ φ \to P \in ℝ$
59	16	nngt0d	$⊢ φ \to 0 < N$
60	49	nngt0d	$⊢ φ \to 0 < P$
61	57 58 59 60	divgt0d	$⊢ φ \to 0 < \frac{N}{P}$
62	56 61	jca	$⊢ φ \to (\frac{N}{P} \in ℤ \land 0 < \frac{N}{P})$
63		elnnz	$⊢ \frac{N}{P} \in ℕ \leftrightarrow (\frac{N}{P} \in ℤ \land 0 < \frac{N}{P})$
64	62 63	sylibr	$⊢ φ \to \frac{N}{P} \in ℕ$
65	64 23	nnexpcld	$⊢ φ \to {(\frac{N}{P})}^{L} \in ℕ$
66	50 65	nnmulcld	$⊢ φ \to P^{U} {(\frac{N}{P})}^{L} \in ℕ$
67	24 66	eqeltrid	$⊢ φ \to E \in ℕ$
68	1 2 3 4 6 7 10 11 13 14 15 16 17 18 67	aks6d1c1p7	$⊢ φ \to E \underset{˙}{\sim} X$
69	13	fldcrngd	$⊢ φ \to K \in CRing$
70	2	ply1crng	$⊢ K \in CRing \to S \in CRing$
71	69 70	syl	$⊢ φ \to S \in CRing$
72		crngring	$⊢ S \in CRing \to S \in Ring$
73		ringcmn	$⊢ S \in Ring \to S \in CMnd$
74	72 73	syl	$⊢ S \in CRing \to S \in CMnd$
75	71 74	syl	$⊢ φ \to S \in CMnd$
76		cmnmnd	$⊢ S \in CMnd \to S \in Mnd$
77	75 76	syl	$⊢ φ \to S \in Mnd$
78		crngring	$⊢ K \in CRing \to K \in Ring$
79	69 78	syl	$⊢ φ \to K \in Ring$
80		eqid	$⊢ {Base}_{S} = {Base}_{S}$
81	4 2 80	vr1cl	$⊢ K \in Ring \to X \in {Base}_{S}$
82	79 81	syl	$⊢ φ \to X \in {Base}_{S}$
83		eqid	$⊢ 0_{S} = 0_{S}$
84	80 12 83	mndrid	$⊢ (S \in Mnd \land X \in {Base}_{S}) \to X \underset{˙}{+} 0_{S} = X$
85	77 82 84	syl2anc	$⊢ φ \to X \underset{˙}{+} 0_{S} = X$
86	68 85	breqtrrd	$⊢ φ \to E \underset{˙}{\sim} (X \underset{˙}{+} 0_{S})$
87		eqid	$⊢ ℤRHom (K) = ℤRHom (K)$
88		eqid	$⊢ 0_{K} = 0_{K}$
89	87 88	zrh0	$⊢ K \in Ring \to ℤRHom (K) (0) = 0_{K}$
90	79 89	syl	$⊢ φ \to ℤRHom (K) (0) = 0_{K}$
91	90	fveq2d	$⊢ φ \to C (ℤRHom (K) (0)) = C (0_{K})$
92	2 8 88 83 79	ply1ascl0	$⊢ φ \to C (0_{K}) = 0_{S}$
93	91 92	eqtrd	$⊢ φ \to C (ℤRHom (K) (0)) = 0_{S}$
94	93	oveq2d	$⊢ φ \to X \underset{˙}{+} C (ℤRHom (K) (0)) = X \underset{˙}{+} 0_{S}$
95	86 94	breqtrrd	$⊢ φ \to E \underset{˙}{\sim} (X \underset{˙}{+} C (ℤRHom (K) (0)))$
96		0zd	$⊢ φ \to 0 \in ℤ$
97		0red	$⊢ φ \to 0 \in ℝ$
98	97	leidd	$⊢ φ \to 0 \leq 0$
99	96 27 96 98 28	elfzd	$⊢ φ \to 0 \in (0 \dots A)$
100	19 99	ffvelcdmd	$⊢ φ \to F (0) \in ℕ_{0}$
101	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 95 100	aks6d1c1p6	$⊢ φ \to E \underset{˙}{\sim} (F (0) D (X \underset{˙}{+} C (ℤRHom (K) (0))))$
102	5	crngmgp	$⊢ S \in CRing \to W \in CMnd$
103	71 102	syl	$⊢ φ \to W \in CMnd$
104	103	cmnmndd	$⊢ φ \to W \in Mnd$
105		0z	$⊢ 0 \in ℤ$
106	105	a1i	$⊢ φ \to 0 \in ℤ$
107		eqid	$⊢ {Base}_{W} = {Base}_{W}$
108		0le0	$⊢ 0 \leq 0$
109	108	a1i	$⊢ φ \to 0 \leq 0$
110	106 27 106 109 28	elfzd	$⊢ φ \to 0 \in (0 \dots A)$
111	19 110	ffvelcdmd	$⊢ φ \to F (0) \in ℕ_{0}$
112	87	zrhrhm	$⊢ K \in Ring \to ℤRHom (K) \in (ℤ_{ring} RingHom K)$
113	79 112	syl	$⊢ φ \to ℤRHom (K) \in (ℤ_{ring} RingHom K)$
114		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
115		eqid	$⊢ {Base}_{K} = {Base}_{K}$
116	114 115	rhmf	$⊢ ℤRHom (K) \in (ℤ_{ring} RingHom K) \to ℤRHom (K) : ℤ ⟶ {Base}_{K}$
117	113 116	syl	$⊢ φ \to ℤRHom (K) : ℤ ⟶ {Base}_{K}$
118	117 96	ffvelcdmd	$⊢ φ \to ℤRHom (K) (0) \in {Base}_{K}$
119	2 8 115 80	ply1sclcl	$⊢ (K \in Ring \land ℤRHom (K) (0) \in {Base}_{K}) \to C (ℤRHom (K) (0)) \in {Base}_{S}$
120	79 118 119	syl2anc	$⊢ φ \to C (ℤRHom (K) (0)) \in {Base}_{S}$
121	80 12	mndcl	$⊢ (S \in Mnd \land X \in {Base}_{S} \land C (ℤRHom (K) (0)) \in {Base}_{S}) \to X \underset{˙}{+} C (ℤRHom (K) (0)) \in {Base}_{S}$
122	77 82 120 121	syl3anc	$⊢ φ \to X \underset{˙}{+} C (ℤRHom (K) (0)) \in {Base}_{S}$
123	5 80	mgpbas	$⊢ {Base}_{S} = {Base}_{W}$
124	122 123	eleqtrdi	$⊢ φ \to X \underset{˙}{+} C (ℤRHom (K) (0)) \in {Base}_{W}$
125	107 9 104 111 124	mulgnn0cld	$⊢ φ \to F (0) D (X \underset{˙}{+} C (ℤRHom (K) (0))) \in {Base}_{W}$
126		fveq2	$⊢ i = 0 \to F (i) = F (0)$
127		2fveq3	$⊢ i = 0 \to C (ℤRHom (K) (i)) = C (ℤRHom (K) (0))$
128	127	oveq2d	$⊢ i = 0 \to X \underset{˙}{+} C (ℤRHom (K) (i)) = X \underset{˙}{+} C (ℤRHom (K) (0))$
129	126 128	oveq12d	$⊢ i = 0 \to F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i))) = F (0) D (X \underset{˙}{+} C (ℤRHom (K) (0)))$
130	107 129	gsumsn	$⊢ (W \in Mnd \land 0 \in ℤ \land F (0) D (X \underset{˙}{+} C (ℤRHom (K) (0))) \in {Base}_{W}) \to \underset{i \in \{0\}}{\sum_{W}} (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))) = F (0) D (X \underset{˙}{+} C (ℤRHom (K) (0)))$
131	104 106 125 130	syl3anc	$⊢ φ \to \underset{i \in \{0\}}{\sum_{W}} (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))) = F (0) D (X \underset{˙}{+} C (ℤRHom (K) (0)))$
132	101 131	breqtrrd	$⊢ φ \to E \underset{˙}{\sim} (\underset{i \in \{0\}}{\sum_{W}}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))$
133		fzsn	$⊢ 0 \in ℤ \to (0 \dots 0) = \{0\}$
134	105 133	ax-mp	$⊢ (0 \dots 0) = \{0\}$
135	134	a1i	$⊢ φ \to (0 \dots 0) = \{0\}$
136	135	mpteq1d	$⊢ φ \to (i \in (0 \dots 0) ⟼ F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))) = (i \in \{0\} ⟼ F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i))))$
137	136	oveq2d	$⊢ φ \to {\sum_{W}}_{i = 0}^{0} (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))) = \underset{i \in \{0\}}{\sum_{W}} (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i))))$
138	132 137	breqtrrd	$⊢ φ \to E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{0}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))$
139	13	3ad2ant1	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A) \land E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))) \to K \in Field$
140	14	3ad2ant1	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A) \land E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))) \to P \in ℙ$
141	15	3ad2ant1	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A) \land E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))) \to R \in ℕ$
142	18	3ad2ant1	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A) \land E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))) \to N \gcd R = 1$
143	17	3ad2ant1	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A) \land E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))) \to P ∥ N$
144		simp3	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A) \land E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))) \to E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))$
145		nfcv	$⊢ \underline{Ⅎ} k (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i))))$
146		nfcv	$⊢ \underline{Ⅎ} i (F (k) D (X \underset{˙}{+} C (ℤRHom (K) (k))))$
147		fveq2	$⊢ i = k \to F (i) = F (k)$
148		2fveq3	$⊢ i = k \to C (ℤRHom (K) (i)) = C (ℤRHom (K) (k))$
149	148	oveq2d	$⊢ i = k \to X \underset{˙}{+} C (ℤRHom (K) (i)) = X \underset{˙}{+} C (ℤRHom (K) (k))$
150	147 149	oveq12d	$⊢ i = k \to F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i))) = F (k) D (X \underset{˙}{+} C (ℤRHom (K) (k)))$
151	145 146 150	cbvmpt	$⊢ (i \in (0 \dots j) ⟼ F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))) = (k \in (0 \dots j) ⟼ F (k) D (X \underset{˙}{+} C (ℤRHom (K) (k))))$
152	151	oveq2i	$⊢ {\sum_{W}}_{i = 0}^{j} (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))) = {\sum_{W}}_{k = 0}^{j} (F (k) D (X \underset{˙}{+} C (ℤRHom (K) (k))))$
153	152	a1i	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A) \land E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))) \to {\sum_{W}}_{i = 0}^{j} (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))) = {\sum_{W}}_{k = 0}^{j} (F (k) D (X \underset{˙}{+} C (ℤRHom (K) (k))))$
154	144 153	breqtrd	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A) \land E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))) \to E \underset{˙}{\sim} ({\sum_{W}}_{k = 0}^{j}, (F (k) D (X \underset{˙}{+} C (ℤRHom (K) (k)))))$
155	13	adantr	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A)) \to K \in Field$
156	14	adantr	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A)) \to P \in ℙ$
157	15	adantr	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A)) \to R \in ℕ$
158	16	adantr	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A)) \to N \in ℕ$
159	17	adantr	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A)) \to P ∥ N$
160	18	adantr	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A)) \to N \gcd R = 1$
161	24	a1i	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A)) \to E = P^{U} {(\frac{N}{P})}^{L}$
162	15	nnzd	$⊢ φ \to R \in ℤ$
163	56 162 23	3jca	$⊢ φ \to (\frac{N}{P} \in ℤ \land R \in ℤ \land L \in ℕ_{0})$
164	162 56 53	3jca	$⊢ φ \to (R \in ℤ \land \frac{N}{P} \in ℤ \land N \in ℤ)$
165	53 162	jca	$⊢ φ \to (N \in ℤ \land R \in ℤ)$
166		gcdcom	$⊢ (N \in ℤ \land R \in ℤ) \to N \gcd R = R \gcd N$
167	165 166	syl	$⊢ φ \to N \gcd R = R \gcd N$
168		eqeq1	$⊢ N \gcd R = R \gcd N \to (N \gcd R = 1 \leftrightarrow R \gcd N = 1)$
169	167 168	syl	$⊢ φ \to (N \gcd R = 1 \leftrightarrow R \gcd N = 1)$
170	169	pm5.74i	$⊢ (φ \to N \gcd R = 1) \leftrightarrow (φ \to R \gcd N = 1)$
171	18 170	mpbi	$⊢ φ \to R \gcd N = 1$
172	57	recnd	$⊢ φ \to N \in ℂ$
173	58	recnd	$⊢ φ \to P \in ℂ$
174	97 59	gtned	$⊢ φ \to N \neq 0$
175	172 172 173 174 52	divdiv2d	$⊢ φ \to \frac{N}{\frac{N}{P}} = \frac{N P}{N}$
176	172 173	mulcomd	$⊢ φ \to N P = P \cdot N$
177	176	oveq1d	$⊢ φ \to \frac{N P}{N} = \frac{P \cdot N}{N}$
178	173 172 172 174 174	divdiv2d	$⊢ φ \to \frac{P}{\frac{N}{N}} = \frac{P \cdot N}{N}$
179	178	eqcomd	$⊢ φ \to \frac{P \cdot N}{N} = \frac{P}{\frac{N}{N}}$
180	177 179	eqtrd	$⊢ φ \to \frac{N P}{N} = \frac{P}{\frac{N}{N}}$
181	172 174	dividd	$⊢ φ \to \frac{N}{N} = 1$
182	181	oveq2d	$⊢ φ \to \frac{P}{\frac{N}{N}} = \frac{P}{1}$
183	173	div1d	$⊢ φ \to \frac{P}{1} = P$
184	182 183	eqtrd	$⊢ φ \to \frac{P}{\frac{N}{N}} = P$
185	184 51	eqeltrd	$⊢ φ \to \frac{P}{\frac{N}{N}} \in ℤ$
186	180 185	eqeltrd	$⊢ φ \to \frac{N P}{N} \in ℤ$
187	175 186	eqeltrd	$⊢ φ \to \frac{N}{\frac{N}{P}} \in ℤ$
188	97 61	gtned	$⊢ φ \to \frac{N}{P} \neq 0$
189		dvdsval2	$⊢ (\frac{N}{P} \in ℤ \land \frac{N}{P} \neq 0 \land N \in ℤ) \to ((\frac{N}{P}) ∥ N \leftrightarrow \frac{N}{\frac{N}{P}} \in ℤ)$
190	56 188 53 189	syl3anc	$⊢ φ \to ((\frac{N}{P}) ∥ N \leftrightarrow \frac{N}{\frac{N}{P}} \in ℤ)$
191	187 190	mpbird	$⊢ φ \to (\frac{N}{P}) ∥ N$
192	171 191	jca	$⊢ φ \to (R \gcd N = 1 \land (\frac{N}{P}) ∥ N)$
193		rpdvds	$⊢ ((R \in ℤ \land \frac{N}{P} \in ℤ \land N \in ℤ) \land (R \gcd N = 1 \land (\frac{N}{P}) ∥ N)) \to R \gcd (\frac{N}{P}) = 1$
194	164 192 193	syl2anc	$⊢ φ \to R \gcd (\frac{N}{P}) = 1$
195	162 56	jca	$⊢ φ \to (R \in ℤ \land \frac{N}{P} \in ℤ)$
196		gcdcom	$⊢ (R \in ℤ \land \frac{N}{P} \in ℤ) \to R \gcd (\frac{N}{P}) = (\frac{N}{P}) \gcd R$
197	195 196	syl	$⊢ φ \to R \gcd (\frac{N}{P}) = (\frac{N}{P}) \gcd R$
198		eqeq1	$⊢ R \gcd (\frac{N}{P}) = (\frac{N}{P}) \gcd R \to (R \gcd (\frac{N}{P}) = 1 \leftrightarrow (\frac{N}{P}) \gcd R = 1)$
199	197 198	syl	$⊢ φ \to (R \gcd (\frac{N}{P}) = 1 \leftrightarrow (\frac{N}{P}) \gcd R = 1)$
200	199	pm5.74i	$⊢ (φ \to R \gcd (\frac{N}{P}) = 1) \leftrightarrow (φ \to (\frac{N}{P}) \gcd R = 1)$
201	194 200	mpbi	$⊢ φ \to (\frac{N}{P}) \gcd R = 1$
202		rpexp1i	$⊢ (\frac{N}{P} \in ℤ \land R \in ℤ \land L \in ℕ_{0}) \to ((\frac{N}{P}) \gcd R = 1 \to {(\frac{N}{P})}^{L} \gcd R = 1)$
203	202	imp	$⊢ ((\frac{N}{P} \in ℤ \land R \in ℤ \land L \in ℕ_{0}) \land (\frac{N}{P}) \gcd R = 1) \to {(\frac{N}{P})}^{L} \gcd R = 1$
204	163 201 203	syl2anc	$⊢ φ \to {(\frac{N}{P})}^{L} \gcd R = 1$
205	204	adantr	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A)) \to {(\frac{N}{P})}^{L} \gcd R = 1$
206		eqid	$⊢ X \underset{˙}{+} C (ℤRHom (K) (j + 1)) = X \underset{˙}{+} C (ℤRHom (K) (j + 1))$
207		simpr1	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A)) \to j \in ℤ$
208	207	peano2zd	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A)) \to j + 1 \in ℤ$
209	1 2 3 4 5 6 7 8 9 10 11 12 155 156 157 160 159 206 208	aks6d1c1p2	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A)) \to P \underset{˙}{\sim} (X \underset{˙}{+} C (ℤRHom (K) (j + 1)))$
210	22	adantr	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A)) \to U \in ℕ_{0}$
211	162 51 53	3jca	$⊢ φ \to (R \in ℤ \land P \in ℤ \land N \in ℤ)$
212	171 17	jca	$⊢ φ \to (R \gcd N = 1 \land P ∥ N)$
213		rpdvds	$⊢ ((R \in ℤ \land P \in ℤ \land N \in ℤ) \land (R \gcd N = 1 \land P ∥ N)) \to R \gcd P = 1$
214	211 212 213	syl2anc	$⊢ φ \to R \gcd P = 1$
215	162 51	jca	$⊢ φ \to (R \in ℤ \land P \in ℤ)$
216		gcdcom	$⊢ (R \in ℤ \land P \in ℤ) \to R \gcd P = P \gcd R$
217	215 216	syl	$⊢ φ \to R \gcd P = P \gcd R$
218		eqeq1	$⊢ R \gcd P = P \gcd R \to (R \gcd P = 1 \leftrightarrow P \gcd R = 1)$
219	217 218	syl	$⊢ φ \to (R \gcd P = 1 \leftrightarrow P \gcd R = 1)$
220	219	pm5.74i	$⊢ (φ \to R \gcd P = 1) \leftrightarrow (φ \to P \gcd R = 1)$
221	214 220	mpbi	$⊢ φ \to P \gcd R = 1$
222	221	adantr	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A)) \to P \gcd R = 1$
223	1 2 3 4 5 6 7 8 9 10 11 12 155 156 157 158 159 160 209 210 222	aks6d1c1p8	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A)) \to P^{U} \underset{˙}{\sim} (X \underset{˙}{+} C (ℤRHom (K) (j + 1)))$
224		2fveq3	$⊢ a = j + 1 \to C (ℤRHom (K) (a)) = C (ℤRHom (K) (j + 1))$
225	224	oveq2d	$⊢ a = j + 1 \to X \underset{˙}{+} C (ℤRHom (K) (a)) = X \underset{˙}{+} C (ℤRHom (K) (j + 1))$
226	225	breq2d	$⊢ a = j + 1 \to (N \underset{˙}{\sim} (X \underset{˙}{+} C (ℤRHom (K) (a))) \leftrightarrow N \underset{˙}{\sim} (X \underset{˙}{+} C (ℤRHom (K) (j + 1))))$
227	1 2 3 4 6 7 10 11 13 14 15 16 17 18 16	aks6d1c1p7	$⊢ φ \to N \underset{˙}{\sim} X$
228	227 85	breqtrrd	$⊢ φ \to N \underset{˙}{\sim} (X \underset{˙}{+} 0_{S})$
229	228 94	breqtrrd	$⊢ φ \to N \underset{˙}{\sim} (X \underset{˙}{+} C (ℤRHom (K) (0)))$
230	229	adantr	$⊢ (φ \land a = 0) \to N \underset{˙}{\sim} (X \underset{˙}{+} C (ℤRHom (K) (0)))$
231		simpr	$⊢ (φ \land a = 0) \to a = 0$
232	231	fveq2d	$⊢ (φ \land a = 0) \to ℤRHom (K) (a) = ℤRHom (K) (0)$
233	232	fveq2d	$⊢ (φ \land a = 0) \to C (ℤRHom (K) (a)) = C (ℤRHom (K) (0))$
234	233	oveq2d	$⊢ (φ \land a = 0) \to X \underset{˙}{+} C (ℤRHom (K) (a)) = X \underset{˙}{+} C (ℤRHom (K) (0))$
235	230 234	breqtrrd	$⊢ (φ \land a = 0) \to N \underset{˙}{\sim} (X \underset{˙}{+} C (ℤRHom (K) (a)))$
236	235	ex	$⊢ φ \to (a = 0 \to N \underset{˙}{\sim} (X \underset{˙}{+} C (ℤRHom (K) (a))))$
237	236	adantr	$⊢ (φ \land (a \in (1 \dots A) \to N \underset{˙}{\sim} (X \underset{˙}{+} C (ℤRHom (K) (a))))) \to (a = 0 \to N \underset{˙}{\sim} (X \underset{˙}{+} C (ℤRHom (K) (a))))$
238		simpr	$⊢ (φ \land (a \in (1 \dots A) \to N \underset{˙}{\sim} (X \underset{˙}{+} C (ℤRHom (K) (a))))) \to (a \in (1 \dots A) \to N \underset{˙}{\sim} (X \underset{˙}{+} C (ℤRHom (K) (a))))$
239		1cnd	$⊢ (φ \land (a \in (1 \dots A) \to N \underset{˙}{\sim} (X \underset{˙}{+} C (ℤRHom (K) (a))))) \to 1 \in ℂ$
240	239	addlidd	$⊢ (φ \land (a \in (1 \dots A) \to N \underset{˙}{\sim} (X \underset{˙}{+} C (ℤRHom (K) (a))))) \to 0 + 1 = 1$
241	240	oveq1d	$⊢ (φ \land (a \in (1 \dots A) \to N \underset{˙}{\sim} (X \underset{˙}{+} C (ℤRHom (K) (a))))) \to (0 + 1 \dots A) = (1 \dots A)$
242	241	eleq2d	$⊢ (φ \land (a \in (1 \dots A) \to N \underset{˙}{\sim} (X \underset{˙}{+} C (ℤRHom (K) (a))))) \to (a \in (0 + 1 \dots A) \leftrightarrow a \in (1 \dots A))$
243	242	imbi1d	$⊢ (φ \land (a \in (1 \dots A) \to N \underset{˙}{\sim} (X \underset{˙}{+} C (ℤRHom (K) (a))))) \to ((a \in (0 + 1 \dots A) \to N \underset{˙}{\sim} (X \underset{˙}{+} C (ℤRHom (K) (a)))) \leftrightarrow (a \in (1 \dots A) \to N \underset{˙}{\sim} (X \underset{˙}{+} C (ℤRHom (K) (a)))))$
244	238 243	mpbird	$⊢ (φ \land (a \in (1 \dots A) \to N \underset{˙}{\sim} (X \underset{˙}{+} C (ℤRHom (K) (a))))) \to (a \in (0 + 1 \dots A) \to N \underset{˙}{\sim} (X \underset{˙}{+} C (ℤRHom (K) (a))))$
245	237 244	jaod	$⊢ (φ \land (a \in (1 \dots A) \to N \underset{˙}{\sim} (X \underset{˙}{+} C (ℤRHom (K) (a))))) \to ((a = 0 \lor a \in (0 + 1 \dots A)) \to N \underset{˙}{\sim} (X \underset{˙}{+} C (ℤRHom (K) (a))))$
246	27 28	jca	$⊢ φ \to (A \in ℤ \land 0 \leq A)$
247		eluz1	$⊢ 0 \in ℤ \to (A \in ℤ_{\geq 0} \leftrightarrow (A \in ℤ \land 0 \leq A))$
248	96 247	syl	$⊢ φ \to (A \in ℤ_{\geq 0} \leftrightarrow (A \in ℤ \land 0 \leq A))$
249	246 248	mpbird	$⊢ φ \to A \in ℤ_{\geq 0}$
250	249	adantr	$⊢ (φ \land (a \in (1 \dots A) \to N \underset{˙}{\sim} (X \underset{˙}{+} C (ℤRHom (K) (a))))) \to A \in ℤ_{\geq 0}$
251		elfzp12	$⊢ A \in ℤ_{\geq 0} \to (a \in (0 \dots A) \leftrightarrow (a = 0 \lor a \in (0 + 1 \dots A)))$
252	250 251	syl	$⊢ (φ \land (a \in (1 \dots A) \to N \underset{˙}{\sim} (X \underset{˙}{+} C (ℤRHom (K) (a))))) \to (a \in (0 \dots A) \leftrightarrow (a = 0 \lor a \in (0 + 1 \dots A)))$
253	252	imbi1d	$⊢ (φ \land (a \in (1 \dots A) \to N \underset{˙}{\sim} (X \underset{˙}{+} C (ℤRHom (K) (a))))) \to ((a \in (0 \dots A) \to N \underset{˙}{\sim} (X \underset{˙}{+} C (ℤRHom (K) (a)))) \leftrightarrow ((a = 0 \lor a \in (0 + 1 \dots A)) \to N \underset{˙}{\sim} (X \underset{˙}{+} C (ℤRHom (K) (a)))))$
254	245 253	mpbird	$⊢ (φ \land (a \in (1 \dots A) \to N \underset{˙}{\sim} (X \underset{˙}{+} C (ℤRHom (K) (a))))) \to (a \in (0 \dots A) \to N \underset{˙}{\sim} (X \underset{˙}{+} C (ℤRHom (K) (a))))$
255	254	ex	$⊢ φ \to ((a \in (1 \dots A) \to N \underset{˙}{\sim} (X \underset{˙}{+} C (ℤRHom (K) (a)))) \to (a \in (0 \dots A) \to N \underset{˙}{\sim} (X \underset{˙}{+} C (ℤRHom (K) (a)))))$
256	255	ralimdv2	$⊢ φ \to (\forall a \in (1 \dots A) N \underset{˙}{\sim} (X \underset{˙}{+} C (ℤRHom (K) (a))) \to \forall a \in (0 \dots A) N \underset{˙}{\sim} (X \underset{˙}{+} C (ℤRHom (K) (a))))$
257	25 256	mpd	$⊢ φ \to \forall a \in (0 \dots A) N \underset{˙}{\sim} (X \underset{˙}{+} C (ℤRHom (K) (a)))$
258	257	adantr	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A)) \to \forall a \in (0 \dots A) N \underset{˙}{\sim} (X \underset{˙}{+} C (ℤRHom (K) (a)))$
259		0zd	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A)) \to 0 \in ℤ$
260	27	adantr	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A)) \to A \in ℤ$
261	207	zred	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A)) \to j \in ℝ$
262		1red	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A)) \to 1 \in ℝ$
263		simpr2	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A)) \to 0 \leq j$
264		0le1	$⊢ 0 \leq 1$
265	264	a1i	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A)) \to 0 \leq 1$
266	261 262 263 265	addge0d	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A)) \to 0 \leq j + 1$
267		simpr3	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A)) \to j < A$
268	207 260	zltp1led	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A)) \to (j < A \leftrightarrow j + 1 \leq A)$
269	267 268	mpbid	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A)) \to j + 1 \leq A$
270	259 260 208 266 269	elfzd	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A)) \to j + 1 \in (0 \dots A)$
271	226 258 270	rspcdva	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A)) \to N \underset{˙}{\sim} (X \underset{˙}{+} C (ℤRHom (K) (j + 1)))$
272	26	adantr	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A)) \to (x \in {Base}_{K} ⟼ P \underset{˙}{\times} x) \in (K RingIso K)$
273	1 2 3 4 5 6 7 8 9 10 11 12 155 156 157 160 159 206 208 271 272	aks6d1c1p3	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A)) \to (\frac{N}{P}) \underset{˙}{\sim} (X \underset{˙}{+} C (ℤRHom (K) (j + 1)))$
274	23	adantr	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A)) \to L \in ℕ_{0}$
275	201	adantr	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A)) \to (\frac{N}{P}) \gcd R = 1$
276	1 2 3 4 5 6 7 8 9 10 11 12 155 156 157 158 159 160 273 274 275	aks6d1c1p8	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A)) \to {(\frac{N}{P})}^{L} \underset{˙}{\sim} (X \underset{˙}{+} C (ℤRHom (K) (j + 1)))$
277	1 2 3 4 5 6 7 8 10 11 12 155 156 157 205 159 223 276	aks6d1c1p5	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A)) \to P^{U} {(\frac{N}{P})}^{L} \underset{˙}{\sim} (X \underset{˙}{+} C (ℤRHom (K) (j + 1)))$
278	161 277	eqbrtrd	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A)) \to E \underset{˙}{\sim} (X \underset{˙}{+} C (ℤRHom (K) (j + 1)))$
279	19	adantr	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A)) \to F : (0 \dots A) ⟶ ℕ_{0}$
280	279 270	ffvelcdmd	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A)) \to F (j + 1) \in ℕ_{0}$
281	1 2 3 4 5 6 7 8 9 10 11 12 155 156 157 158 159 160 278 280	aks6d1c1p6	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A)) \to E \underset{˙}{\sim} (F (j + 1) D (X \underset{˙}{+} C (ℤRHom (K) (j + 1))))$
282	104	adantr	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A)) \to W \in Mnd$
283		ovexd	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A)) \to j + 1 \in V$
284	77	adantr	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A)) \to S \in Mnd$
285	82	adantr	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A)) \to X \in {Base}_{S}$
286	79	adantr	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A)) \to K \in Ring$
287	117	adantr	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A)) \to ℤRHom (K) : ℤ ⟶ {Base}_{K}$
288	287 208	ffvelcdmd	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A)) \to ℤRHom (K) (j + 1) \in {Base}_{K}$
289	2 8 115 80	ply1sclcl	$⊢ (K \in Ring \land ℤRHom (K) (j + 1) \in {Base}_{K}) \to C (ℤRHom (K) (j + 1)) \in {Base}_{S}$
290	286 288 289	syl2anc	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A)) \to C (ℤRHom (K) (j + 1)) \in {Base}_{S}$
291	80 12	mndcl	$⊢ (S \in Mnd \land X \in {Base}_{S} \land C (ℤRHom (K) (j + 1)) \in {Base}_{S}) \to X \underset{˙}{+} C (ℤRHom (K) (j + 1)) \in {Base}_{S}$
292	284 285 290 291	syl3anc	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A)) \to X \underset{˙}{+} C (ℤRHom (K) (j + 1)) \in {Base}_{S}$
293	292 123	eleqtrdi	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A)) \to X \underset{˙}{+} C (ℤRHom (K) (j + 1)) \in {Base}_{W}$
294	107 9 282 280 293	mulgnn0cld	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A)) \to F (j + 1) D (X \underset{˙}{+} C (ℤRHom (K) (j + 1))) \in {Base}_{W}$
295		fveq2	$⊢ k = j + 1 \to F (k) = F (j + 1)$
296		2fveq3	$⊢ k = j + 1 \to C (ℤRHom (K) (k)) = C (ℤRHom (K) (j + 1))$
297	296	oveq2d	$⊢ k = j + 1 \to X \underset{˙}{+} C (ℤRHom (K) (k)) = X \underset{˙}{+} C (ℤRHom (K) (j + 1))$
298	295 297	oveq12d	$⊢ k = j + 1 \to F (k) D (X \underset{˙}{+} C (ℤRHom (K) (k))) = F (j + 1) D (X \underset{˙}{+} C (ℤRHom (K) (j + 1)))$
299	107 298	gsumsn	$⊢ (W \in Mnd \land j + 1 \in V \land F (j + 1) D (X \underset{˙}{+} C (ℤRHom (K) (j + 1))) \in {Base}_{W}) \to \underset{k \in \{j + 1\}}{\sum_{W}} (F (k) D (X \underset{˙}{+} C (ℤRHom (K) (k)))) = F (j + 1) D (X \underset{˙}{+} C (ℤRHom (K) (j + 1)))$
300	282 283 294 299	syl3anc	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A)) \to \underset{k \in \{j + 1\}}{\sum_{W}} (F (k) D (X \underset{˙}{+} C (ℤRHom (K) (k)))) = F (j + 1) D (X \underset{˙}{+} C (ℤRHom (K) (j + 1)))$
301	281 300	breqtrrd	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A)) \to E \underset{˙}{\sim} (\underset{k \in \{j + 1\}}{\sum_{W}}, (F (k) D (X \underset{˙}{+} C (ℤRHom (K) (k)))))$
302	301	3adant3	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A) \land E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))) \to E \underset{˙}{\sim} (\underset{k \in \{j + 1\}}{\sum_{W}}, (F (k) D (X \underset{˙}{+} C (ℤRHom (K) (k)))))$
303	1 2 3 4 5 6 7 8 9 10 11 12 139 140 141 142 143 154 302	aks6d1c1p4	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A) \land E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))) \to E \underset{˙}{\sim} (({\sum_{W}}_{k = 0}^{j}, (F (k) D (X \underset{˙}{+} C (ℤRHom (K) (k))))) +_{W} (\underset{k \in \{j + 1\}}{\sum_{W}}, (F (k) D (X \underset{˙}{+} C (ℤRHom (K) (k))))))$
304	145 146 150	cbvmpt	$⊢ (i \in (0 \dots j + 1) ⟼ F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))) = (k \in (0 \dots j + 1) ⟼ F (k) D (X \underset{˙}{+} C (ℤRHom (K) (k))))$
305	304	a1i	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A) \land E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))) \to (i \in (0 \dots j + 1) ⟼ F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))) = (k \in (0 \dots j + 1) ⟼ F (k) D (X \underset{˙}{+} C (ℤRHom (K) (k))))$
306	305	oveq2d	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A) \land E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))) \to {\sum_{W}}_{i = 0}^{j + 1} (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))) = {\sum_{W}}_{k = 0}^{j + 1} (F (k) D (X \underset{˙}{+} C (ℤRHom (K) (k))))$
307		eqid	$⊢ +_{W} = +_{W}$
308	103	3ad2ant1	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A) \land E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))) \to W \in CMnd$
309		simp21	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A) \land E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))) \to j \in ℤ$
310		simp22	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A) \land E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))) \to 0 \leq j$
311	309 310	jca	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A) \land E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))) \to (j \in ℤ \land 0 \leq j)$
312		elnn0z	$⊢ j \in ℕ_{0} \leftrightarrow (j \in ℤ \land 0 \leq j)$
313	311 312	sylibr	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A) \land E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))) \to j \in ℕ_{0}$
314	282	3adant3	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A) \land E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))) \to W \in Mnd$
315	314	adantr	$⊢ ((φ \land (j \in ℤ \land 0 \leq j \land j < A) \land E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))) \land k \in (0 \dots j + 1)) \to W \in Mnd$
316	19	3ad2ant1	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A) \land E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))) \to F : (0 \dots A) ⟶ ℕ_{0}$
317	316	adantr	$⊢ ((φ \land (j \in ℤ \land 0 \leq j \land j < A) \land E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))) \land k \in (0 \dots j + 1)) \to F : (0 \dots A) ⟶ ℕ_{0}$
318		0zd	$⊢ ((φ \land (j \in ℤ \land 0 \leq j \land j < A) \land E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))) \land k \in (0 \dots j + 1)) \to 0 \in ℤ$
319	27	3ad2ant1	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A) \land E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))) \to A \in ℤ$
320	319	adantr	$⊢ ((φ \land (j \in ℤ \land 0 \leq j \land j < A) \land E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))) \land k \in (0 \dots j + 1)) \to A \in ℤ$
321		elfzelz	$⊢ k \in (0 \dots j + 1) \to k \in ℤ$
322	321	adantl	$⊢ ((φ \land (j \in ℤ \land 0 \leq j \land j < A) \land E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))) \land k \in (0 \dots j + 1)) \to k \in ℤ$
323		elfzle1	$⊢ k \in (0 \dots j + 1) \to 0 \leq k$
324	323	adantl	$⊢ ((φ \land (j \in ℤ \land 0 \leq j \land j < A) \land E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))) \land k \in (0 \dots j + 1)) \to 0 \leq k$
325	322	zred	$⊢ ((φ \land (j \in ℤ \land 0 \leq j \land j < A) \land E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))) \land k \in (0 \dots j + 1)) \to k \in ℝ$
326	309	adantr	$⊢ ((φ \land (j \in ℤ \land 0 \leq j \land j < A) \land E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))) \land k \in (0 \dots j + 1)) \to j \in ℤ$
327	326	zred	$⊢ ((φ \land (j \in ℤ \land 0 \leq j \land j < A) \land E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))) \land k \in (0 \dots j + 1)) \to j \in ℝ$
328		1red	$⊢ ((φ \land (j \in ℤ \land 0 \leq j \land j < A) \land E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))) \land k \in (0 \dots j + 1)) \to 1 \in ℝ$
329	327 328	readdcld	$⊢ ((φ \land (j \in ℤ \land 0 \leq j \land j < A) \land E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))) \land k \in (0 \dots j + 1)) \to j + 1 \in ℝ$
330	320	zred	$⊢ ((φ \land (j \in ℤ \land 0 \leq j \land j < A) \land E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))) \land k \in (0 \dots j + 1)) \to A \in ℝ$
331		elfzle2	$⊢ k \in (0 \dots j + 1) \to k \leq j + 1$
332	331	adantl	$⊢ ((φ \land (j \in ℤ \land 0 \leq j \land j < A) \land E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))) \land k \in (0 \dots j + 1)) \to k \leq j + 1$
333		simpl23	$⊢ ((φ \land (j \in ℤ \land 0 \leq j \land j < A) \land E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))) \land k \in (0 \dots j + 1)) \to j < A$
334	326 320	zltp1led	$⊢ ((φ \land (j \in ℤ \land 0 \leq j \land j < A) \land E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))) \land k \in (0 \dots j + 1)) \to (j < A \leftrightarrow j + 1 \leq A)$
335	333 334	mpbid	$⊢ ((φ \land (j \in ℤ \land 0 \leq j \land j < A) \land E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))) \land k \in (0 \dots j + 1)) \to j + 1 \leq A$
336	325 329 330 332 335	letrd	$⊢ ((φ \land (j \in ℤ \land 0 \leq j \land j < A) \land E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))) \land k \in (0 \dots j + 1)) \to k \leq A$
337	318 320 322 324 336	elfzd	$⊢ ((φ \land (j \in ℤ \land 0 \leq j \land j < A) \land E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))) \land k \in (0 \dots j + 1)) \to k \in (0 \dots A)$
338	317 337	ffvelcdmd	$⊢ ((φ \land (j \in ℤ \land 0 \leq j \land j < A) \land E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))) \land k \in (0 \dots j + 1)) \to F (k) \in ℕ_{0}$
339	284	3adant3	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A) \land E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))) \to S \in Mnd$
340	339	adantr	$⊢ ((φ \land (j \in ℤ \land 0 \leq j \land j < A) \land E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))) \land k \in (0 \dots j + 1)) \to S \in Mnd$
341	285	3adant3	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A) \land E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))) \to X \in {Base}_{S}$
342	341	adantr	$⊢ ((φ \land (j \in ℤ \land 0 \leq j \land j < A) \land E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))) \land k \in (0 \dots j + 1)) \to X \in {Base}_{S}$
343	286	3adant3	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A) \land E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))) \to K \in Ring$
344	343	adantr	$⊢ ((φ \land (j \in ℤ \land 0 \leq j \land j < A) \land E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))) \land k \in (0 \dots j + 1)) \to K \in Ring$
345	344 112 116	3syl	$⊢ ((φ \land (j \in ℤ \land 0 \leq j \land j < A) \land E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))) \land k \in (0 \dots j + 1)) \to ℤRHom (K) : ℤ ⟶ {Base}_{K}$
346	345 322	ffvelcdmd	$⊢ ((φ \land (j \in ℤ \land 0 \leq j \land j < A) \land E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))) \land k \in (0 \dots j + 1)) \to ℤRHom (K) (k) \in {Base}_{K}$
347	2 8 115 80	ply1sclcl	$⊢ (K \in Ring \land ℤRHom (K) (k) \in {Base}_{K}) \to C (ℤRHom (K) (k)) \in {Base}_{S}$
348	344 346 347	syl2anc	$⊢ ((φ \land (j \in ℤ \land 0 \leq j \land j < A) \land E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))) \land k \in (0 \dots j + 1)) \to C (ℤRHom (K) (k)) \in {Base}_{S}$
349	80 12	mndcl	$⊢ (S \in Mnd \land X \in {Base}_{S} \land C (ℤRHom (K) (k)) \in {Base}_{S}) \to X \underset{˙}{+} C (ℤRHom (K) (k)) \in {Base}_{S}$
350	340 342 348 349	syl3anc	$⊢ ((φ \land (j \in ℤ \land 0 \leq j \land j < A) \land E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))) \land k \in (0 \dots j + 1)) \to X \underset{˙}{+} C (ℤRHom (K) (k)) \in {Base}_{S}$
351	350 123	eleqtrdi	$⊢ ((φ \land (j \in ℤ \land 0 \leq j \land j < A) \land E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))) \land k \in (0 \dots j + 1)) \to X \underset{˙}{+} C (ℤRHom (K) (k)) \in {Base}_{W}$
352	107 9 315 338 351	mulgnn0cld	$⊢ ((φ \land (j \in ℤ \land 0 \leq j \land j < A) \land E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))) \land k \in (0 \dots j + 1)) \to F (k) D (X \underset{˙}{+} C (ℤRHom (K) (k))) \in {Base}_{W}$
353	107 307 308 313 352	gsummptfzsplit	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A) \land E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))) \to {\sum_{W}}_{k = 0}^{j + 1} (F (k) D (X \underset{˙}{+} C (ℤRHom (K) (k)))) = ({\sum_{W}}_{k = 0}^{j}, (F (k) D (X \underset{˙}{+} C (ℤRHom (K) (k))))) +_{W} (\underset{k \in \{j + 1\}}{\sum_{W}}, (F (k) D (X \underset{˙}{+} C (ℤRHom (K) (k)))))$
354	306 353	eqtrd	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A) \land E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))) \to {\sum_{W}}_{i = 0}^{j + 1} (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))) = ({\sum_{W}}_{k = 0}^{j}, (F (k) D (X \underset{˙}{+} C (ℤRHom (K) (k))))) +_{W} (\underset{k \in \{j + 1\}}{\sum_{W}}, (F (k) D (X \underset{˙}{+} C (ℤRHom (K) (k)))))$
355	303 354	breqtrrd	$⊢ (φ \land (j \in ℤ \land 0 \leq j \land j < A) \land E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))) \to E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{j + 1}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))$
356	35 39 43 47 138 355 96 27 28	fzindd	$⊢ (φ \land (A \in ℤ \land 0 \leq A \land A \leq A)) \to E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{A}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))$
357	356	ex	$⊢ φ \to ((A \in ℤ \land 0 \leq A \land A \leq A) \to E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{A}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i))))))$
358	31 357	mpd	$⊢ φ \to E \underset{˙}{\sim} ({\sum_{W}}_{i = 0}^{A}, (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))$
359	20	a1i	$⊢ φ \to G = (g \in ({ℕ_{0}}^{(0 \dots A)}) ⟼ {\sum_{W}}_{i = 0}^{A} (g (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))))$
360		simplr	$⊢ ((φ \land g = F) \land i \in (0 \dots A)) \to g = F$
361	360	fveq1d	$⊢ ((φ \land g = F) \land i \in (0 \dots A)) \to g (i) = F (i)$
362	361	oveq1d	$⊢ ((φ \land g = F) \land i \in (0 \dots A)) \to g (i) D (X \underset{˙}{+} C (ℤRHom (K) (i))) = F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))$
363	362	mpteq2dva	$⊢ (φ \land g = F) \to (i \in (0 \dots A) ⟼ g (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))) = (i \in (0 \dots A) ⟼ F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i))))$
364	363	oveq2d	$⊢ (φ \land g = F) \to {\sum_{W}}_{i = 0}^{A} (g (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))) = {\sum_{W}}_{i = 0}^{A} (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i))))$
365		nn0ex	$⊢ ℕ_{0} \in V$
366	365	a1i	$⊢ φ \to ℕ_{0} \in V$
367		ovexd	$⊢ φ \to (0 \dots A) \in V$
368	366 367	elmapd	$⊢ φ \to (F \in ({ℕ_{0}}^{(0 \dots A)}) \leftrightarrow F : (0 \dots A) ⟶ ℕ_{0})$
369	19 368	mpbird	$⊢ φ \to F \in ({ℕ_{0}}^{(0 \dots A)})$
370		ovexd	$⊢ φ \to {\sum_{W}}_{i = 0}^{A} (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i)))) \in V$
371	359 364 369 370	fvmptd	$⊢ φ \to G (F) = {\sum_{W}}_{i = 0}^{A} (F (i) D (X \underset{˙}{+} C (ℤRHom (K) (i))))$
372	358 371	breqtrrd	$⊢ φ \to E \underset{˙}{\sim} G (F)$

Metamath Proof Explorer

Theorem aks6d1c1

Proof