aks6d1c2lem3

Description: Lemma for aks6d1c2 to simplify context. (Contributed by metakunt, 1-May-2025)

	Ref	Expression
Hypotheses	aks6d1c2.1	$⊢ \underset{˙}{\sim} = \{⟨e, f⟩ \| (e \in ℕ \land f \in {Base}_{{Poly}_{1} (K)} \land \forall y \in ({mulGrp}_{K} PrimRoots R) e \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (f) (y) = {eval}_{1} (K) (f) (e \cdot_{{mulGrp}_{K}} y))\}$
	aks6d1c2.2	$⊢ P = chr (K)$
	aks6d1c2.3	$⊢ φ \to K \in Field$
	aks6d1c2.4	$⊢ φ \to P \in ℙ$
	aks6d1c2.5	$⊢ φ \to R \in ℕ$
	aks6d1c2.6	$⊢ φ \to N \in ℕ$
	aks6d1c2.7	$⊢ φ \to P ∥ N$
	aks6d1c2.8	$⊢ φ \to N \gcd R = 1$
	aks6d1c2.9	$⊢ φ \to F : (0 \dots A) ⟶ ℕ_{0}$
	aks6d1c2.10	$⊢ G = (g \in ({ℕ_{0}}^{(0 \dots A)}) ⟼ {\sum_{{mulGrp}_{{Poly}_{1} (K)}}}_{i = 0}^{A} (g (i) \cdot_{{mulGrp}_{{Poly}_{1} (K)}} ({var}_{1} (K) +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (i)))))$
	aks6d1c2.11	$⊢ φ \to A \in ℕ_{0}$
	aks6d1c2.12	$⊢ E = (k \in ℕ_{0}, l \in ℕ_{0} ⟼ P^{k} {(\frac{N}{P})}^{l})$
	aks6d1c2.13	$⊢ L = ℤRHom (ℤ / R ℤ)$
	aks6d1c2.14	$⊢ φ \to \forall a \in (1 \dots A) N \underset{˙}{\sim} ({var}_{1} (K) +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (a)))$
	aks6d1c2.15	$⊢ φ \to (x \in {Base}_{K} ⟼ P \cdot_{{mulGrp}_{K}} x) \in (K RingIso K)$
	aks6d1c2.16	$⊢ φ \to M \in ({mulGrp}_{K} PrimRoots R)$
	aks6d1c2.17	$⊢ H = (h \in ({ℕ_{0}}^{(0 \dots A)}) ⟼ {eval}_{1} (K) (G (h)) (M))$
	aks6d1c2.18	$⊢ B = ⌊\sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|}⌋$
	aks6d1c2.19	$⊢ C = E [(0 \dots B) \times (0 \dots B)]$
	aks6d1c2.20	$⊢ φ \to I \in C$
	aks6d1c2.21	$⊢ φ \to J \in C$
	aks6d1c2.22	$⊢ φ \to I < J$
	aks6d1c2.23	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{{Poly}_{1} (K)}}$
	aks6d1c2.24	$⊢ X = {var}_{1} (K)$
	aks6d1c2.25	$⊢ S = (J \underset{˙}{\times} X) -_{{Poly}_{1} (K)} (I \underset{˙}{\times} X)$
	aks6d1c2.26	$⊢ φ \to U \in ℕ$
	aks6d1c2.27	$⊢ φ \to J = I + U R$
	aks6d1c2p3.1	$⊢ φ \to s \in ({ℕ_{0}}^{(0 \dots A)})$
	aks6d1c2p3.2	$⊢ φ \to r \in (0 \dots B)$
	aks6d1c2p3.3	$⊢ φ \to o \in (0 \dots B)$
	aks6d1c2p3.4	$⊢ φ \to J = r E o$
	aks6d1c2p3.5	$⊢ φ \to p \in (0 \dots B)$
	aks6d1c2p3.6	$⊢ φ \to q \in (0 \dots B)$
	aks6d1c2p3.7	$⊢ φ \to I = p E q$
	aks6d1c2p3.8	$⊢ φ \to I \in ℕ_{0}$
Assertion	aks6d1c2lem3	$⊢ φ \to J \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (G (s)) (M) = I \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (G (s)) (M)$

Proof

Step	Hyp	Ref	Expression
1		aks6d1c2.1	$⊢ \underset{˙}{\sim} = \{⟨e, f⟩ \| (e \in ℕ \land f \in {Base}_{{Poly}_{1} (K)} \land \forall y \in ({mulGrp}_{K} PrimRoots R) e \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (f) (y) = {eval}_{1} (K) (f) (e \cdot_{{mulGrp}_{K}} y))\}$
2		aks6d1c2.2	$⊢ P = chr (K)$
3		aks6d1c2.3	$⊢ φ \to K \in Field$
4		aks6d1c2.4	$⊢ φ \to P \in ℙ$
5		aks6d1c2.5	$⊢ φ \to R \in ℕ$
6		aks6d1c2.6	$⊢ φ \to N \in ℕ$
7		aks6d1c2.7	$⊢ φ \to P ∥ N$
8		aks6d1c2.8	$⊢ φ \to N \gcd R = 1$
9		aks6d1c2.9	$⊢ φ \to F : (0 \dots A) ⟶ ℕ_{0}$
10		aks6d1c2.10	$⊢ G = (g \in ({ℕ_{0}}^{(0 \dots A)}) ⟼ {\sum_{{mulGrp}_{{Poly}_{1} (K)}}}_{i = 0}^{A} (g (i) \cdot_{{mulGrp}_{{Poly}_{1} (K)}} ({var}_{1} (K) +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (i)))))$
11		aks6d1c2.11	$⊢ φ \to A \in ℕ_{0}$
12		aks6d1c2.12	$⊢ E = (k \in ℕ_{0}, l \in ℕ_{0} ⟼ P^{k} {(\frac{N}{P})}^{l})$
13		aks6d1c2.13	$⊢ L = ℤRHom (ℤ / R ℤ)$
14		aks6d1c2.14	$⊢ φ \to \forall a \in (1 \dots A) N \underset{˙}{\sim} ({var}_{1} (K) +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (a)))$
15		aks6d1c2.15	$⊢ φ \to (x \in {Base}_{K} ⟼ P \cdot_{{mulGrp}_{K}} x) \in (K RingIso K)$
16		aks6d1c2.16	$⊢ φ \to M \in ({mulGrp}_{K} PrimRoots R)$
17		aks6d1c2.17	$⊢ H = (h \in ({ℕ_{0}}^{(0 \dots A)}) ⟼ {eval}_{1} (K) (G (h)) (M))$
18		aks6d1c2.18	$⊢ B = ⌊\sqrt{\|L [E [ℕ_{0} \times ℕ_{0}]]\|}⌋$
19		aks6d1c2.19	$⊢ C = E [(0 \dots B) \times (0 \dots B)]$
20		aks6d1c2.20	$⊢ φ \to I \in C$
21		aks6d1c2.21	$⊢ φ \to J \in C$
22		aks6d1c2.22	$⊢ φ \to I < J$
23		aks6d1c2.23	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{{Poly}_{1} (K)}}$
24		aks6d1c2.24	$⊢ X = {var}_{1} (K)$
25		aks6d1c2.25	$⊢ S = (J \underset{˙}{\times} X) -_{{Poly}_{1} (K)} (I \underset{˙}{\times} X)$
26		aks6d1c2.26	$⊢ φ \to U \in ℕ$
27		aks6d1c2.27	$⊢ φ \to J = I + U R$
28		aks6d1c2p3.1	$⊢ φ \to s \in ({ℕ_{0}}^{(0 \dots A)})$
29		aks6d1c2p3.2	$⊢ φ \to r \in (0 \dots B)$
30		aks6d1c2p3.3	$⊢ φ \to o \in (0 \dots B)$
31		aks6d1c2p3.4	$⊢ φ \to J = r E o$
32		aks6d1c2p3.5	$⊢ φ \to p \in (0 \dots B)$
33		aks6d1c2p3.6	$⊢ φ \to q \in (0 \dots B)$
34		aks6d1c2p3.7	$⊢ φ \to I = p E q$
35		aks6d1c2p3.8	$⊢ φ \to I \in ℕ_{0}$
36	12	a1i	$⊢ φ \to E = (k \in ℕ_{0}, l \in ℕ_{0} ⟼ P^{k} {(\frac{N}{P})}^{l})$
37		simprl	$⊢ (φ \land (k = r \land l = o)) \to k = r$
38	37	oveq2d	$⊢ (φ \land (k = r \land l = o)) \to P^{k} = P^{r}$
39		simprr	$⊢ (φ \land (k = r \land l = o)) \to l = o$
40	39	oveq2d	$⊢ (φ \land (k = r \land l = o)) \to {(\frac{N}{P})}^{l} = {(\frac{N}{P})}^{o}$
41	38 40	oveq12d	$⊢ (φ \land (k = r \land l = o)) \to P^{k} {(\frac{N}{P})}^{l} = P^{r} {(\frac{N}{P})}^{o}$
42		elfznn0	$⊢ r \in (0 \dots B) \to r \in ℕ_{0}$
43	29 42	syl	$⊢ φ \to r \in ℕ_{0}$
44		elfznn0	$⊢ o \in (0 \dots B) \to o \in ℕ_{0}$
45	30 44	syl	$⊢ φ \to o \in ℕ_{0}$
46		ovexd	$⊢ φ \to P^{r} {(\frac{N}{P})}^{o} \in V$
47	36 41 43 45 46	ovmpod	$⊢ φ \to r E o = P^{r} {(\frac{N}{P})}^{o}$
48	31 47	eqtrd	$⊢ φ \to J = P^{r} {(\frac{N}{P})}^{o}$
49	48	oveq1d	$⊢ φ \to J \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (G (s)) (M) = P^{r} {(\frac{N}{P})}^{o} \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (G (s)) (M)$
50		simprl	$⊢ (φ \land (k = p \land l = q)) \to k = p$
51	50	oveq2d	$⊢ (φ \land (k = p \land l = q)) \to P^{k} = P^{p}$
52		simprr	$⊢ (φ \land (k = p \land l = q)) \to l = q$
53	52	oveq2d	$⊢ (φ \land (k = p \land l = q)) \to {(\frac{N}{P})}^{l} = {(\frac{N}{P})}^{q}$
54	51 53	oveq12d	$⊢ (φ \land (k = p \land l = q)) \to P^{k} {(\frac{N}{P})}^{l} = P^{p} {(\frac{N}{P})}^{q}$
55		elfznn0	$⊢ p \in (0 \dots B) \to p \in ℕ_{0}$
56	32 55	syl	$⊢ φ \to p \in ℕ_{0}$
57		elfznn0	$⊢ q \in (0 \dots B) \to q \in ℕ_{0}$
58	33 57	syl	$⊢ φ \to q \in ℕ_{0}$
59		ovexd	$⊢ φ \to P^{p} {(\frac{N}{P})}^{q} \in V$
60	36 54 56 58 59	ovmpod	$⊢ φ \to p E q = P^{p} {(\frac{N}{P})}^{q}$
61	34 60	eqtrd	$⊢ φ \to I = P^{p} {(\frac{N}{P})}^{q}$
62	61	oveq1d	$⊢ φ \to I \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (G (s)) (M) = P^{p} {(\frac{N}{P})}^{q} \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (G (s)) (M)$
63		fveq2	$⊢ y = M \to {eval}_{1} (K) (G (s)) (y) = {eval}_{1} (K) (G (s)) (M)$
64	63	oveq2d	$⊢ y = M \to P^{p} {(\frac{N}{P})}^{q} \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (G (s)) (y) = P^{p} {(\frac{N}{P})}^{q} \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (G (s)) (M)$
65		oveq2	$⊢ y = M \to P^{p} {(\frac{N}{P})}^{q} \cdot_{{mulGrp}_{K}} y = P^{p} {(\frac{N}{P})}^{q} \cdot_{{mulGrp}_{K}} M$
66	65	fveq2d	$⊢ y = M \to {eval}_{1} (K) (G (s)) (P^{p} {(\frac{N}{P})}^{q} \cdot_{{mulGrp}_{K}} y) = {eval}_{1} (K) (G (s)) (P^{p} {(\frac{N}{P})}^{q} \cdot_{{mulGrp}_{K}} M)$
67	64 66	eqeq12d	$⊢ y = M \to (P^{p} {(\frac{N}{P})}^{q} \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (G (s)) (y) = {eval}_{1} (K) (G (s)) (P^{p} {(\frac{N}{P})}^{q} \cdot_{{mulGrp}_{K}} y) \leftrightarrow P^{p} {(\frac{N}{P})}^{q} \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (G (s)) (M) = {eval}_{1} (K) (G (s)) (P^{p} {(\frac{N}{P})}^{q} \cdot_{{mulGrp}_{K}} M))$
68		nn0ex	$⊢ ℕ_{0} \in V$
69	68	a1i	$⊢ φ \to ℕ_{0} \in V$
70		ovexd	$⊢ φ \to (0 \dots A) \in V$
71		elmapg	$⊢ (ℕ_{0} \in V \land (0 \dots A) \in V) \to (s \in ({ℕ_{0}}^{(0 \dots A)}) \leftrightarrow s : (0 \dots A) ⟶ ℕ_{0})$
72	69 70 71	syl2anc	$⊢ φ \to (s \in ({ℕ_{0}}^{(0 \dots A)}) \leftrightarrow s : (0 \dots A) ⟶ ℕ_{0})$
73	28 72	mpbid	$⊢ φ \to s : (0 \dots A) ⟶ ℕ_{0}$
74		eqid	$⊢ P^{p} {(\frac{N}{P})}^{q} = P^{p} {(\frac{N}{P})}^{q}$
75	1 2 3 4 5 6 7 8 73 10 11 56 58 74 14 15	aks6d1c1rh	$⊢ φ \to P^{p} {(\frac{N}{P})}^{q} \underset{˙}{\sim} G (s)$
76	1 75	aks6d1c1p1rcl	$⊢ φ \to (P^{p} {(\frac{N}{P})}^{q} \in ℕ \land G (s) \in {Base}_{{Poly}_{1} (K)})$
77	76	simprd	$⊢ φ \to G (s) \in {Base}_{{Poly}_{1} (K)}$
78	76	simpld	$⊢ φ \to P^{p} {(\frac{N}{P})}^{q} \in ℕ$
79	1 77 78	aks6d1c1p1	$⊢ φ \to (P^{p} {(\frac{N}{P})}^{q} \underset{˙}{\sim} G (s) \leftrightarrow \forall y \in ({mulGrp}_{K} PrimRoots R) P^{p} {(\frac{N}{P})}^{q} \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (G (s)) (y) = {eval}_{1} (K) (G (s)) (P^{p} {(\frac{N}{P})}^{q} \cdot_{{mulGrp}_{K}} y))$
80	75 79	mpbid	$⊢ φ \to \forall y \in ({mulGrp}_{K} PrimRoots R) P^{p} {(\frac{N}{P})}^{q} \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (G (s)) (y) = {eval}_{1} (K) (G (s)) (P^{p} {(\frac{N}{P})}^{q} \cdot_{{mulGrp}_{K}} y)$
81	67 80 16	rspcdva	$⊢ φ \to P^{p} {(\frac{N}{P})}^{q} \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (G (s)) (M) = {eval}_{1} (K) (G (s)) (P^{p} {(\frac{N}{P})}^{q} \cdot_{{mulGrp}_{K}} M)$
82	61	eqcomd	$⊢ φ \to P^{p} {(\frac{N}{P})}^{q} = I$
83	82	oveq1d	$⊢ φ \to P^{p} {(\frac{N}{P})}^{q} \cdot_{{mulGrp}_{K}} M = I \cdot_{{mulGrp}_{K}} M$
84	48	eqcomd	$⊢ φ \to P^{r} {(\frac{N}{P})}^{o} = J$
85	84	oveq1d	$⊢ φ \to P^{r} {(\frac{N}{P})}^{o} \cdot_{{mulGrp}_{K}} M = J \cdot_{{mulGrp}_{K}} M$
86	27	oveq1d	$⊢ φ \to J \cdot_{{mulGrp}_{K}} M = (I + U R) \cdot_{{mulGrp}_{K}} M$
87	3	fldcrngd	$⊢ φ \to K \in CRing$
88		crngring	$⊢ K \in CRing \to K \in Ring$
89	87 88	syl	$⊢ φ \to K \in Ring$
90		eqid	$⊢ {mulGrp}_{K} = {mulGrp}_{K}$
91	90	ringmgp	$⊢ K \in Ring \to {mulGrp}_{K} \in Mnd$
92	89 91	syl	$⊢ φ \to {mulGrp}_{K} \in Mnd$
93	26	nnnn0d	$⊢ φ \to U \in ℕ_{0}$
94	5	nnnn0d	$⊢ φ \to R \in ℕ_{0}$
95	93 94	nn0mulcld	$⊢ φ \to U R \in ℕ_{0}$
96	90	crngmgp	$⊢ K \in CRing \to {mulGrp}_{K} \in CMnd$
97	87 96	syl	$⊢ φ \to {mulGrp}_{K} \in CMnd$
98		eqid	$⊢ \cdot_{{mulGrp}_{K}} = \cdot_{{mulGrp}_{K}}$
99	97 94 98	isprimroot	$⊢ φ \to (M \in ({mulGrp}_{K} PrimRoots R) \leftrightarrow (M \in {Base}_{{mulGrp}_{K}} \land R \cdot_{{mulGrp}_{K}} M = 0_{{mulGrp}_{K}} \land \forall v \in ℕ_{0} (v \cdot_{{mulGrp}_{K}} M = 0_{{mulGrp}_{K}} \to R ∥ v)))$
100	99	biimpd	$⊢ φ \to (M \in ({mulGrp}_{K} PrimRoots R) \to (M \in {Base}_{{mulGrp}_{K}} \land R \cdot_{{mulGrp}_{K}} M = 0_{{mulGrp}_{K}} \land \forall v \in ℕ_{0} (v \cdot_{{mulGrp}_{K}} M = 0_{{mulGrp}_{K}} \to R ∥ v)))$
101	16 100	mpd	$⊢ φ \to (M \in {Base}_{{mulGrp}_{K}} \land R \cdot_{{mulGrp}_{K}} M = 0_{{mulGrp}_{K}} \land \forall v \in ℕ_{0} (v \cdot_{{mulGrp}_{K}} M = 0_{{mulGrp}_{K}} \to R ∥ v))$
102	101	simp1d	$⊢ φ \to M \in {Base}_{{mulGrp}_{K}}$
103	35 95 102	3jca	$⊢ φ \to (I \in ℕ_{0} \land U R \in ℕ_{0} \land M \in {Base}_{{mulGrp}_{K}})$
104		eqid	$⊢ {Base}_{{mulGrp}_{K}} = {Base}_{{mulGrp}_{K}}$
105		eqid	$⊢ +_{{mulGrp}_{K}} = +_{{mulGrp}_{K}}$
106	104 98 105	mulgnn0dir	$⊢ ({mulGrp}_{K} \in Mnd \land (I \in ℕ_{0} \land U R \in ℕ_{0} \land M \in {Base}_{{mulGrp}_{K}})) \to (I + U R) \cdot_{{mulGrp}_{K}} M = (I \cdot_{{mulGrp}_{K}} M) +_{{mulGrp}_{K}} (U R \cdot_{{mulGrp}_{K}} M)$
107	92 103 106	syl2anc	$⊢ φ \to (I + U R) \cdot_{{mulGrp}_{K}} M = (I \cdot_{{mulGrp}_{K}} M) +_{{mulGrp}_{K}} (U R \cdot_{{mulGrp}_{K}} M)$
108	93 94 102	3jca	$⊢ φ \to (U \in ℕ_{0} \land R \in ℕ_{0} \land M \in {Base}_{{mulGrp}_{K}})$
109	104 98	mulgnn0ass	$⊢ ({mulGrp}_{K} \in Mnd \land (U \in ℕ_{0} \land R \in ℕ_{0} \land M \in {Base}_{{mulGrp}_{K}})) \to U R \cdot_{{mulGrp}_{K}} M = U \cdot_{{mulGrp}_{K}} (R \cdot_{{mulGrp}_{K}} M)$
110	92 108 109	syl2anc	$⊢ φ \to U R \cdot_{{mulGrp}_{K}} M = U \cdot_{{mulGrp}_{K}} (R \cdot_{{mulGrp}_{K}} M)$
111	101	simp2d	$⊢ φ \to R \cdot_{{mulGrp}_{K}} M = 0_{{mulGrp}_{K}}$
112	111	oveq2d	$⊢ φ \to U \cdot_{{mulGrp}_{K}} (R \cdot_{{mulGrp}_{K}} M) = U \cdot_{{mulGrp}_{K}} 0_{{mulGrp}_{K}}$
113		eqid	$⊢ 0_{{mulGrp}_{K}} = 0_{{mulGrp}_{K}}$
114	104 98 113	mulgnn0z	$⊢ ({mulGrp}_{K} \in Mnd \land U \in ℕ_{0}) \to U \cdot_{{mulGrp}_{K}} 0_{{mulGrp}_{K}} = 0_{{mulGrp}_{K}}$
115	92 93 114	syl2anc	$⊢ φ \to U \cdot_{{mulGrp}_{K}} 0_{{mulGrp}_{K}} = 0_{{mulGrp}_{K}}$
116	112 115	eqtrd	$⊢ φ \to U \cdot_{{mulGrp}_{K}} (R \cdot_{{mulGrp}_{K}} M) = 0_{{mulGrp}_{K}}$
117	110 116	eqtrd	$⊢ φ \to U R \cdot_{{mulGrp}_{K}} M = 0_{{mulGrp}_{K}}$
118	117	oveq2d	$⊢ φ \to (I \cdot_{{mulGrp}_{K}} M) +_{{mulGrp}_{K}} (U R \cdot_{{mulGrp}_{K}} M) = (I \cdot_{{mulGrp}_{K}} M) +_{{mulGrp}_{K}} 0_{{mulGrp}_{K}}$
119	104 98 92 35 102	mulgnn0cld	$⊢ φ \to I \cdot_{{mulGrp}_{K}} M \in {Base}_{{mulGrp}_{K}}$
120	104 105 113	mndrid	$⊢ ({mulGrp}_{K} \in Mnd \land I \cdot_{{mulGrp}_{K}} M \in {Base}_{{mulGrp}_{K}}) \to (I \cdot_{{mulGrp}_{K}} M) +_{{mulGrp}_{K}} 0_{{mulGrp}_{K}} = I \cdot_{{mulGrp}_{K}} M$
121	92 119 120	syl2anc	$⊢ φ \to (I \cdot_{{mulGrp}_{K}} M) +_{{mulGrp}_{K}} 0_{{mulGrp}_{K}} = I \cdot_{{mulGrp}_{K}} M$
122	118 121	eqtrd	$⊢ φ \to (I \cdot_{{mulGrp}_{K}} M) +_{{mulGrp}_{K}} (U R \cdot_{{mulGrp}_{K}} M) = I \cdot_{{mulGrp}_{K}} M$
123	107 122	eqtrd	$⊢ φ \to (I + U R) \cdot_{{mulGrp}_{K}} M = I \cdot_{{mulGrp}_{K}} M$
124	86 123	eqtrd	$⊢ φ \to J \cdot_{{mulGrp}_{K}} M = I \cdot_{{mulGrp}_{K}} M$
125	85 124	eqtr2d	$⊢ φ \to I \cdot_{{mulGrp}_{K}} M = P^{r} {(\frac{N}{P})}^{o} \cdot_{{mulGrp}_{K}} M$
126	83 125	eqtrd	$⊢ φ \to P^{p} {(\frac{N}{P})}^{q} \cdot_{{mulGrp}_{K}} M = P^{r} {(\frac{N}{P})}^{o} \cdot_{{mulGrp}_{K}} M$
127	126	fveq2d	$⊢ φ \to {eval}_{1} (K) (G (s)) (P^{p} {(\frac{N}{P})}^{q} \cdot_{{mulGrp}_{K}} M) = {eval}_{1} (K) (G (s)) (P^{r} {(\frac{N}{P})}^{o} \cdot_{{mulGrp}_{K}} M)$
128	63	oveq2d	$⊢ y = M \to P^{r} {(\frac{N}{P})}^{o} \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (G (s)) (y) = P^{r} {(\frac{N}{P})}^{o} \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (G (s)) (M)$
129		oveq2	$⊢ y = M \to P^{r} {(\frac{N}{P})}^{o} \cdot_{{mulGrp}_{K}} y = P^{r} {(\frac{N}{P})}^{o} \cdot_{{mulGrp}_{K}} M$
130	129	fveq2d	$⊢ y = M \to {eval}_{1} (K) (G (s)) (P^{r} {(\frac{N}{P})}^{o} \cdot_{{mulGrp}_{K}} y) = {eval}_{1} (K) (G (s)) (P^{r} {(\frac{N}{P})}^{o} \cdot_{{mulGrp}_{K}} M)$
131	128 130	eqeq12d	$⊢ y = M \to (P^{r} {(\frac{N}{P})}^{o} \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (G (s)) (y) = {eval}_{1} (K) (G (s)) (P^{r} {(\frac{N}{P})}^{o} \cdot_{{mulGrp}_{K}} y) \leftrightarrow P^{r} {(\frac{N}{P})}^{o} \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (G (s)) (M) = {eval}_{1} (K) (G (s)) (P^{r} {(\frac{N}{P})}^{o} \cdot_{{mulGrp}_{K}} M))$
132		eqid	$⊢ P^{r} {(\frac{N}{P})}^{o} = P^{r} {(\frac{N}{P})}^{o}$
133	1 2 3 4 5 6 7 8 73 10 11 43 45 132 14 15	aks6d1c1rh	$⊢ φ \to P^{r} {(\frac{N}{P})}^{o} \underset{˙}{\sim} G (s)$
134	1 133	aks6d1c1p1rcl	$⊢ φ \to (P^{r} {(\frac{N}{P})}^{o} \in ℕ \land G (s) \in {Base}_{{Poly}_{1} (K)})$
135	134	simpld	$⊢ φ \to P^{r} {(\frac{N}{P})}^{o} \in ℕ$
136	1 77 135	aks6d1c1p1	$⊢ φ \to (P^{r} {(\frac{N}{P})}^{o} \underset{˙}{\sim} G (s) \leftrightarrow \forall y \in ({mulGrp}_{K} PrimRoots R) P^{r} {(\frac{N}{P})}^{o} \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (G (s)) (y) = {eval}_{1} (K) (G (s)) (P^{r} {(\frac{N}{P})}^{o} \cdot_{{mulGrp}_{K}} y))$
137	133 136	mpbid	$⊢ φ \to \forall y \in ({mulGrp}_{K} PrimRoots R) P^{r} {(\frac{N}{P})}^{o} \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (G (s)) (y) = {eval}_{1} (K) (G (s)) (P^{r} {(\frac{N}{P})}^{o} \cdot_{{mulGrp}_{K}} y)$
138	131 137 16	rspcdva	$⊢ φ \to P^{r} {(\frac{N}{P})}^{o} \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (G (s)) (M) = {eval}_{1} (K) (G (s)) (P^{r} {(\frac{N}{P})}^{o} \cdot_{{mulGrp}_{K}} M)$
139	138	eqcomd	$⊢ φ \to {eval}_{1} (K) (G (s)) (P^{r} {(\frac{N}{P})}^{o} \cdot_{{mulGrp}_{K}} M) = P^{r} {(\frac{N}{P})}^{o} \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (G (s)) (M)$
140	127 139	eqtrd	$⊢ φ \to {eval}_{1} (K) (G (s)) (P^{p} {(\frac{N}{P})}^{q} \cdot_{{mulGrp}_{K}} M) = P^{r} {(\frac{N}{P})}^{o} \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (G (s)) (M)$
141	81 140	eqtrd	$⊢ φ \to P^{p} {(\frac{N}{P})}^{q} \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (G (s)) (M) = P^{r} {(\frac{N}{P})}^{o} \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (G (s)) (M)$
142	62 141	eqtr2d	$⊢ φ \to P^{r} {(\frac{N}{P})}^{o} \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (G (s)) (M) = I \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (G (s)) (M)$
143	49 142	eqtrd	$⊢ φ \to J \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (G (s)) (M) = I \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (G (s)) (M)$

Metamath Proof Explorer

Theorem aks6d1c2lem3

Proof