aks6d1c6lem2

Description: Every primitive root is root of G(u)-G(v). (Contributed by metakunt, 8-May-2025)

	Ref	Expression
Hypotheses	aks6d1c6.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))\}$
	aks6d1c6.2	$⊢ P = chr (K)$
	aks6d1c6.3	$⊢ φ \to K \in Field$
	aks6d1c6.4	$⊢ φ \to P \in ℙ$
	aks6d1c6.5	$⊢ φ \to R \in ℕ$
	aks6d1c6.6	$⊢ φ \to N \in ℕ$
	aks6d1c6.7	$⊢ φ \to P ∥ N$
	aks6d1c6.8	$⊢ φ \to N \gcd R = 1$
	aks6d1c6.9	$⊢ φ \to A < P$
	aks6d1c6.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)))))$
	aks6d1c6.11	$⊢ φ \to A \in ℕ_{0}$
	aks6d1c6.12	$⊢ E = (k \in ℕ_{0}, l \in ℕ_{0} ⟼ P^{k} {(\frac{N}{P})}^{l})$
	aks6d1c6.13	$⊢ L = ℤRHom (ℤ / R ℤ)$
	aks6d1c6.14	$⊢ φ \to \forall a \in (1 \dots A) N \underset{˙}{\sim} ({var}_{1} (K) +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (a)))$
	aks6d1c6.15	$⊢ φ \to (x \in {Base}_{K} ⟼ P \cdot_{{mulGrp}_{K}} x) \in (K RingIso K)$
	aks6d1c6.16	$⊢ φ \to M \in ({mulGrp}_{K} PrimRoots R)$
	aks6d1c6.17	$⊢ H = (h \in ({ℕ_{0}}^{(0 \dots A)}) ⟼ {eval}_{1} (K) (G (h)) (M))$
	aks6d1c6.18	$⊢ D = \|L [E [ℕ_{0} \times ℕ_{0}]]\|$
	aks6d1c6.19	$⊢ S = \{s \in ({ℕ_{0}}^{(0 \dots A)}) \| \sum_{t = 0}^{A} s (t) \leq D - 1\}$
	aks6d1c6lem2.1	$⊢ φ \to U \in S$
	aks6d1c6lem2.2	$⊢ φ \to V \in S$
	aks6d1c6lem2.3	$⊢ φ \to ({H ↾}_{S}) (U) = ({H ↾}_{S}) (V)$
	aks6d1c6lem2.4	$⊢ φ \to U \neq V$
	aks6d1c6lem2.5	$⊢ J = (j \in (ℕ_{0} \times ℕ_{0}) ⟼ E (j) \cdot_{{mulGrp}_{K}} M)$
	aks6d1c6lem2.6	$⊢ φ \to \|L [E [ℕ_{0} \times ℕ_{0}]]\| \leq \|J [ℕ_{0} \times ℕ_{0}]\|$
Assertion	aks6d1c6lem2	$⊢ φ \to D \leq \|{{eval}_{1} (K) (G (U) -_{{Poly}_{1} (K)} G (V))}^{-1} [\{0_{K}\}]\|$

Proof

Step	Hyp	Ref	Expression
1		aks6d1c6.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		aks6d1c6.2	$⊢ P = chr (K)$
3		aks6d1c6.3	$⊢ φ \to K \in Field$
4		aks6d1c6.4	$⊢ φ \to P \in ℙ$
5		aks6d1c6.5	$⊢ φ \to R \in ℕ$
6		aks6d1c6.6	$⊢ φ \to N \in ℕ$
7		aks6d1c6.7	$⊢ φ \to P ∥ N$
8		aks6d1c6.8	$⊢ φ \to N \gcd R = 1$
9		aks6d1c6.9	$⊢ φ \to A < P$
10		aks6d1c6.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		aks6d1c6.11	$⊢ φ \to A \in ℕ_{0}$
12		aks6d1c6.12	$⊢ E = (k \in ℕ_{0}, l \in ℕ_{0} ⟼ P^{k} {(\frac{N}{P})}^{l})$
13		aks6d1c6.13	$⊢ L = ℤRHom (ℤ / R ℤ)$
14		aks6d1c6.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		aks6d1c6.15	$⊢ φ \to (x \in {Base}_{K} ⟼ P \cdot_{{mulGrp}_{K}} x) \in (K RingIso K)$
16		aks6d1c6.16	$⊢ φ \to M \in ({mulGrp}_{K} PrimRoots R)$
17		aks6d1c6.17	$⊢ H = (h \in ({ℕ_{0}}^{(0 \dots A)}) ⟼ {eval}_{1} (K) (G (h)) (M))$
18		aks6d1c6.18	$⊢ D = \|L [E [ℕ_{0} \times ℕ_{0}]]\|$
19		aks6d1c6.19	$⊢ S = \{s \in ({ℕ_{0}}^{(0 \dots A)}) \| \sum_{t = 0}^{A} s (t) \leq D - 1\}$
20		aks6d1c6lem2.1	$⊢ φ \to U \in S$
21		aks6d1c6lem2.2	$⊢ φ \to V \in S$
22		aks6d1c6lem2.3	$⊢ φ \to ({H ↾}_{S}) (U) = ({H ↾}_{S}) (V)$
23		aks6d1c6lem2.4	$⊢ φ \to U \neq V$
24		aks6d1c6lem2.5	$⊢ J = (j \in (ℕ_{0} \times ℕ_{0}) ⟼ E (j) \cdot_{{mulGrp}_{K}} M)$
25		aks6d1c6lem2.6	$⊢ φ \to \|L [E [ℕ_{0} \times ℕ_{0}]]\| \leq \|J [ℕ_{0} \times ℕ_{0}]\|$
26		fvexd	$⊢ φ \to ℤRHom (ℤ / R ℤ) \in V$
27	13 26	eqeltrid	$⊢ φ \to L \in V$
28	27	imaexd	$⊢ φ \to L [E [ℕ_{0} \times ℕ_{0}]] \in V$
29		hashxrcl	$⊢ L [E [ℕ_{0} \times ℕ_{0}]] \in V \to \|L [E [ℕ_{0} \times ℕ_{0}]]\| \in ℝ^{*}$
30	28 29	syl	$⊢ φ \to \|L [E [ℕ_{0} \times ℕ_{0}]]\| \in ℝ^{*}$
31	18 30	eqeltrid	$⊢ φ \to D \in ℝ^{*}$
32	24	a1i	$⊢ φ \to J = (j \in (ℕ_{0} \times ℕ_{0}) ⟼ E (j) \cdot_{{mulGrp}_{K}} M)$
33		nn0ex	$⊢ ℕ_{0} \in V$
34	33	a1i	$⊢ φ \to ℕ_{0} \in V$
35	34 34	xpexd	$⊢ φ \to ℕ_{0} \times ℕ_{0} \in V$
36	35	mptexd	$⊢ φ \to (j \in (ℕ_{0} \times ℕ_{0}) ⟼ E (j) \cdot_{{mulGrp}_{K}} M) \in V$
37	32 36	eqeltrd	$⊢ φ \to J \in V$
38	37	imaexd	$⊢ φ \to J [ℕ_{0} \times ℕ_{0}] \in V$
39		hashxrcl	$⊢ J [ℕ_{0} \times ℕ_{0}] \in V \to \|J [ℕ_{0} \times ℕ_{0}]\| \in ℝ^{*}$
40	38 39	syl	$⊢ φ \to \|J [ℕ_{0} \times ℕ_{0}]\| \in ℝ^{*}$
41		fvexd	$⊢ φ \to {eval}_{1} (K) (G (U) -_{{Poly}_{1} (K)} G (V)) \in V$
42		cnvexg	$⊢ {eval}_{1} (K) (G (U) -_{{Poly}_{1} (K)} G (V)) \in V \to {{eval}_{1} (K) (G (U) -_{{Poly}_{1} (K)} G (V))}^{-1} \in V$
43	41 42	syl	$⊢ φ \to {{eval}_{1} (K) (G (U) -_{{Poly}_{1} (K)} G (V))}^{-1} \in V$
44	43	imaexd	$⊢ φ \to {{eval}_{1} (K) (G (U) -_{{Poly}_{1} (K)} G (V))}^{-1} [\{0_{K}\}] \in V$
45		hashxrcl	$⊢ {{eval}_{1} (K) (G (U) -_{{Poly}_{1} (K)} G (V))}^{-1} [\{0_{K}\}] \in V \to \|{{eval}_{1} (K) (G (U) -_{{Poly}_{1} (K)} G (V))}^{-1} [\{0_{K}\}]\| \in ℝ^{*}$
46	44 45	syl	$⊢ φ \to \|{{eval}_{1} (K) (G (U) -_{{Poly}_{1} (K)} G (V))}^{-1} [\{0_{K}\}]\| \in ℝ^{*}$
47	18	a1i	$⊢ φ \to D = \|L [E [ℕ_{0} \times ℕ_{0}]]\|$
48	47 25	eqbrtrd	$⊢ φ \to D \leq \|J [ℕ_{0} \times ℕ_{0}]\|$
49	44	elexd	$⊢ φ \to {{eval}_{1} (K) (G (U) -_{{Poly}_{1} (K)} G (V))}^{-1} [\{0_{K}\}] \in V$
50		nfv	$⊢ Ⅎ w φ$
51		ovexd	$⊢ (φ \land j \in (ℕ_{0} \times ℕ_{0})) \to E (j) \cdot_{{mulGrp}_{K}} M \in V$
52	51 24	fmptd	$⊢ φ \to J : ℕ_{0} \times ℕ_{0} ⟶ V$
53		ffun	$⊢ J : ℕ_{0} \times ℕ_{0} ⟶ V \to Fun J$
54	52 53	syl	$⊢ φ \to Fun J$
55	24	a1i	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to J = (j \in (ℕ_{0} \times ℕ_{0}) ⟼ E (j) \cdot_{{mulGrp}_{K}} M)$
56		simpr	$⊢ ((φ \land w \in (ℕ_{0} \times ℕ_{0})) \land j = w) \to j = w$
57	56	fveq2d	$⊢ ((φ \land w \in (ℕ_{0} \times ℕ_{0})) \land j = w) \to E (j) = E (w)$
58	57	oveq1d	$⊢ ((φ \land w \in (ℕ_{0} \times ℕ_{0})) \land j = w) \to E (j) \cdot_{{mulGrp}_{K}} M = E (w) \cdot_{{mulGrp}_{K}} M$
59		simpr	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to w \in (ℕ_{0} \times ℕ_{0})$
60		ovexd	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to E (w) \cdot_{{mulGrp}_{K}} M \in V$
61	55 58 59 60	fvmptd	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to J (w) = E (w) \cdot_{{mulGrp}_{K}} M$
62		eqid	$⊢ {eval}_{1} (K) = {eval}_{1} (K)$
63		eqid	$⊢ {Poly}_{1} (K) = {Poly}_{1} (K)$
64		eqid	$⊢ {Base}_{K} = {Base}_{K}$
65		eqid	$⊢ {Base}_{{Poly}_{1} (K)} = {Base}_{{Poly}_{1} (K)}$
66	3	fldcrngd	$⊢ φ \to K \in CRing$
67	66	adantr	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to K \in CRing$
68		eqid	$⊢ {mulGrp}_{K} = {mulGrp}_{K}$
69	68 64	mgpbas	$⊢ {Base}_{K} = {Base}_{{mulGrp}_{K}}$
70		eqid	$⊢ \cdot_{{mulGrp}_{K}} = \cdot_{{mulGrp}_{K}}$
71	66	crngringd	$⊢ φ \to K \in Ring$
72	68	ringmgp	$⊢ K \in Ring \to {mulGrp}_{K} \in Mnd$
73	71 72	syl	$⊢ φ \to {mulGrp}_{K} \in Mnd$
74	73	adantr	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to {mulGrp}_{K} \in Mnd$
75	6 4 7 12	aks6d1c2p1	$⊢ φ \to E : ℕ_{0} \times ℕ_{0} ⟶ ℕ$
76	75	ffvelcdmda	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to E (w) \in ℕ$
77	76	nnnn0d	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to E (w) \in ℕ_{0}$
78	68	crngmgp	$⊢ K \in CRing \to {mulGrp}_{K} \in CMnd$
79	66 78	syl	$⊢ φ \to {mulGrp}_{K} \in CMnd$
80	5	nnnn0d	$⊢ φ \to R \in ℕ_{0}$
81	79 80 70	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 o \in ℕ_{0} (o \cdot_{{mulGrp}_{K}} M = 0_{{mulGrp}_{K}} \to R ∥ o)))$
82	16 81	mpbid	$⊢ φ \to (M \in {Base}_{{mulGrp}_{K}} \land R \cdot_{{mulGrp}_{K}} M = 0_{{mulGrp}_{K}} \land \forall o \in ℕ_{0} (o \cdot_{{mulGrp}_{K}} M = 0_{{mulGrp}_{K}} \to R ∥ o))$
83	82	simp1d	$⊢ φ \to M \in {Base}_{{mulGrp}_{K}}$
84	83 69	eleqtrrdi	$⊢ φ \to M \in {Base}_{K}$
85	84	adantr	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to M \in {Base}_{K}$
86	69 70 74 77 85	mulgnn0cld	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to E (w) \cdot_{{mulGrp}_{K}} M \in {Base}_{K}$
87		eqid	$⊢ {var}_{1} (K) = {var}_{1} (K)$
88		eqid	$⊢ \cdot_{{mulGrp}_{{Poly}_{1} (K)}} = \cdot_{{mulGrp}_{{Poly}_{1} (K)}}$
89	3 4 2 11 9 87 88 10	aks6d1c5lem0	$⊢ φ \to G : {ℕ_{0}}^{(0 \dots A)} ⟶ {Base}_{{Poly}_{1} (K)}$
90	19	eleq2i	$⊢ U \in S \leftrightarrow U \in \{s \in ({ℕ_{0}}^{(0 \dots A)}) \| \sum_{t = 0}^{A} s (t) \leq D - 1\}$
91	20 90	sylib	$⊢ φ \to U \in \{s \in ({ℕ_{0}}^{(0 \dots A)}) \| \sum_{t = 0}^{A} s (t) \leq D - 1\}$
92		elrabi	$⊢ U \in \{s \in ({ℕ_{0}}^{(0 \dots A)}) \| \sum_{t = 0}^{A} s (t) \leq D - 1\} \to U \in ({ℕ_{0}}^{(0 \dots A)})$
93	92	a1i	$⊢ φ \to (U \in \{s \in ({ℕ_{0}}^{(0 \dots A)}) \| \sum_{t = 0}^{A} s (t) \leq D - 1\} \to U \in ({ℕ_{0}}^{(0 \dots A)}))$
94	91 93	mpd	$⊢ φ \to U \in ({ℕ_{0}}^{(0 \dots A)})$
95	89 94	ffvelcdmd	$⊢ φ \to G (U) \in {Base}_{{Poly}_{1} (K)}$
96	95	adantr	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to G (U) \in {Base}_{{Poly}_{1} (K)}$
97		eqidd	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to {eval}_{1} (K) (G (U)) (E (w) \cdot_{{mulGrp}_{K}} M) = {eval}_{1} (K) (G (U)) (E (w) \cdot_{{mulGrp}_{K}} M)$
98	96 97	jca	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to (G (U) \in {Base}_{{Poly}_{1} (K)} \land {eval}_{1} (K) (G (U)) (E (w) \cdot_{{mulGrp}_{K}} M) = {eval}_{1} (K) (G (U)) (E (w) \cdot_{{mulGrp}_{K}} M))$
99	19	eleq2i	$⊢ V \in S \leftrightarrow V \in \{s \in ({ℕ_{0}}^{(0 \dots A)}) \| \sum_{t = 0}^{A} s (t) \leq D - 1\}$
100	21 99	sylib	$⊢ φ \to V \in \{s \in ({ℕ_{0}}^{(0 \dots A)}) \| \sum_{t = 0}^{A} s (t) \leq D - 1\}$
101		elrabi	$⊢ V \in \{s \in ({ℕ_{0}}^{(0 \dots A)}) \| \sum_{t = 0}^{A} s (t) \leq D - 1\} \to V \in ({ℕ_{0}}^{(0 \dots A)})$
102	101	a1i	$⊢ φ \to (V \in \{s \in ({ℕ_{0}}^{(0 \dots A)}) \| \sum_{t = 0}^{A} s (t) \leq D - 1\} \to V \in ({ℕ_{0}}^{(0 \dots A)}))$
103	100 102	mpd	$⊢ φ \to V \in ({ℕ_{0}}^{(0 \dots A)})$
104	89 103	ffvelcdmd	$⊢ φ \to G (V) \in {Base}_{{Poly}_{1} (K)}$
105	104	adantr	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to G (V) \in {Base}_{{Poly}_{1} (K)}$
106		eqidd	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to {eval}_{1} (K) (G (V)) (E (w) \cdot_{{mulGrp}_{K}} M) = {eval}_{1} (K) (G (V)) (E (w) \cdot_{{mulGrp}_{K}} M)$
107	105 106	jca	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to (G (V) \in {Base}_{{Poly}_{1} (K)} \land {eval}_{1} (K) (G (V)) (E (w) \cdot_{{mulGrp}_{K}} M) = {eval}_{1} (K) (G (V)) (E (w) \cdot_{{mulGrp}_{K}} M))$
108		eqid	$⊢ -_{{Poly}_{1} (K)} = -_{{Poly}_{1} (K)}$
109		eqid	$⊢ -_{K} = -_{K}$
110	62 63 64 65 67 86 98 107 108 109	evl1subd	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to (G (U) -_{{Poly}_{1} (K)} G (V) \in {Base}_{{Poly}_{1} (K)} \land {eval}_{1} (K) (G (U) -_{{Poly}_{1} (K)} G (V)) (E (w) \cdot_{{mulGrp}_{K}} M) = {eval}_{1} (K) (G (U)) (E (w) \cdot_{{mulGrp}_{K}} M) -_{K} {eval}_{1} (K) (G (V)) (E (w) \cdot_{{mulGrp}_{K}} M))$
111	110	simprd	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to {eval}_{1} (K) (G (U) -_{{Poly}_{1} (K)} G (V)) (E (w) \cdot_{{mulGrp}_{K}} M) = {eval}_{1} (K) (G (U)) (E (w) \cdot_{{mulGrp}_{K}} M) -_{K} {eval}_{1} (K) (G (V)) (E (w) \cdot_{{mulGrp}_{K}} M)$
112		fveq2	$⊢ y = M \to {eval}_{1} (K) (G (U)) (y) = {eval}_{1} (K) (G (U)) (M)$
113	112	oveq2d	$⊢ y = M \to E (w) \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (G (U)) (y) = E (w) \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (G (U)) (M)$
114		oveq2	$⊢ y = M \to E (w) \cdot_{{mulGrp}_{K}} y = E (w) \cdot_{{mulGrp}_{K}} M$
115	114	fveq2d	$⊢ y = M \to {eval}_{1} (K) (G (U)) (E (w) \cdot_{{mulGrp}_{K}} y) = {eval}_{1} (K) (G (U)) (E (w) \cdot_{{mulGrp}_{K}} M)$
116	113 115	eqeq12d	$⊢ y = M \to (E (w) \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (G (U)) (y) = {eval}_{1} (K) (G (U)) (E (w) \cdot_{{mulGrp}_{K}} y) \leftrightarrow E (w) \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (G (U)) (M) = {eval}_{1} (K) (G (U)) (E (w) \cdot_{{mulGrp}_{K}} M))$
117		vex	$⊢ k \in V$
118		vex	$⊢ l \in V$
119	117 118	op1std	$⊢ s = ⟨k, l⟩ \to 1^{st} (s) = k$
120	119	oveq2d	$⊢ s = ⟨k, l⟩ \to P^{1^{st} (s)} = P^{k}$
121	117 118	op2ndd	$⊢ s = ⟨k, l⟩ \to 2^{nd} (s) = l$
122	121	oveq2d	$⊢ s = ⟨k, l⟩ \to {(\frac{N}{P})}^{2^{nd} (s)} = {(\frac{N}{P})}^{l}$
123	120 122	oveq12d	$⊢ s = ⟨k, l⟩ \to P^{1^{st} (s)} {(\frac{N}{P})}^{2^{nd} (s)} = P^{k} {(\frac{N}{P})}^{l}$
124	123	mpompt	$⊢ (s \in (ℕ_{0} \times ℕ_{0}) ⟼ P^{1^{st} (s)} {(\frac{N}{P})}^{2^{nd} (s)}) = (k \in ℕ_{0}, l \in ℕ_{0} ⟼ P^{k} {(\frac{N}{P})}^{l})$
125	12	eqcomi	$⊢ (k \in ℕ_{0}, l \in ℕ_{0} ⟼ P^{k} {(\frac{N}{P})}^{l}) = E$
126	124 125	eqtri	$⊢ (s \in (ℕ_{0} \times ℕ_{0}) ⟼ P^{1^{st} (s)} {(\frac{N}{P})}^{2^{nd} (s)}) = E$
127	126	eqcomi	$⊢ E = (s \in (ℕ_{0} \times ℕ_{0}) ⟼ P^{1^{st} (s)} {(\frac{N}{P})}^{2^{nd} (s)})$
128	127	a1i	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to E = (s \in (ℕ_{0} \times ℕ_{0}) ⟼ P^{1^{st} (s)} {(\frac{N}{P})}^{2^{nd} (s)})$
129		simpr	$⊢ ((φ \land w \in (ℕ_{0} \times ℕ_{0})) \land s = w) \to s = w$
130	129	fveq2d	$⊢ ((φ \land w \in (ℕ_{0} \times ℕ_{0})) \land s = w) \to 1^{st} (s) = 1^{st} (w)$
131	130	oveq2d	$⊢ ((φ \land w \in (ℕ_{0} \times ℕ_{0})) \land s = w) \to P^{1^{st} (s)} = P^{1^{st} (w)}$
132	129	fveq2d	$⊢ ((φ \land w \in (ℕ_{0} \times ℕ_{0})) \land s = w) \to 2^{nd} (s) = 2^{nd} (w)$
133	132	oveq2d	$⊢ ((φ \land w \in (ℕ_{0} \times ℕ_{0})) \land s = w) \to {(\frac{N}{P})}^{2^{nd} (s)} = {(\frac{N}{P})}^{2^{nd} (w)}$
134	131 133	oveq12d	$⊢ ((φ \land w \in (ℕ_{0} \times ℕ_{0})) \land s = w) \to P^{1^{st} (s)} {(\frac{N}{P})}^{2^{nd} (s)} = P^{1^{st} (w)} {(\frac{N}{P})}^{2^{nd} (w)}$
135		ovexd	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to P^{1^{st} (w)} {(\frac{N}{P})}^{2^{nd} (w)} \in V$
136	128 134 59 135	fvmptd	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to E (w) = P^{1^{st} (w)} {(\frac{N}{P})}^{2^{nd} (w)}$
137	3	adantr	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to K \in Field$
138	4	adantr	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to P \in ℙ$
139	5	adantr	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to R \in ℕ$
140	6	adantr	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to N \in ℕ$
141	7	adantr	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to P ∥ N$
142	8	adantr	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to N \gcd R = 1$
143		ovexd	$⊢ φ \to (0 \dots A) \in V$
144	34 143	elmapd	$⊢ φ \to (U \in ({ℕ_{0}}^{(0 \dots A)}) \leftrightarrow U : (0 \dots A) ⟶ ℕ_{0})$
145	94 144	mpbid	$⊢ φ \to U : (0 \dots A) ⟶ ℕ_{0}$
146	145	adantr	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to U : (0 \dots A) ⟶ ℕ_{0}$
147	11	adantr	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to A \in ℕ_{0}$
148		xp1st	$⊢ w \in (ℕ_{0} \times ℕ_{0}) \to 1^{st} (w) \in ℕ_{0}$
149	148	adantl	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to 1^{st} (w) \in ℕ_{0}$
150		xp2nd	$⊢ w \in (ℕ_{0} \times ℕ_{0}) \to 2^{nd} (w) \in ℕ_{0}$
151	150	adantl	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to 2^{nd} (w) \in ℕ_{0}$
152		eqid	$⊢ P^{1^{st} (w)} {(\frac{N}{P})}^{2^{nd} (w)} = P^{1^{st} (w)} {(\frac{N}{P})}^{2^{nd} (w)}$
153	14	adantr	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to \forall a \in (1 \dots A) N \underset{˙}{\sim} ({var}_{1} (K) +_{{Poly}_{1} (K)} algSc ({Poly}_{1} (K)) (ℤRHom (K) (a)))$
154	15	adantr	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to (x \in {Base}_{K} ⟼ P \cdot_{{mulGrp}_{K}} x) \in (K RingIso K)$
155	1 2 137 138 139 140 141 142 146 10 147 149 151 152 153 154	aks6d1c1rh	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to P^{1^{st} (w)} {(\frac{N}{P})}^{2^{nd} (w)} \underset{˙}{\sim} G (U)$
156	136 155	eqbrtrd	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to E (w) \underset{˙}{\sim} G (U)$
157	1 96 76	aks6d1c1p1	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to (E (w) \underset{˙}{\sim} G (U) \leftrightarrow \forall y \in ({mulGrp}_{K} PrimRoots R) E (w) \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (G (U)) (y) = {eval}_{1} (K) (G (U)) (E (w) \cdot_{{mulGrp}_{K}} y))$
158	156 157	mpbid	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to \forall y \in ({mulGrp}_{K} PrimRoots R) E (w) \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (G (U)) (y) = {eval}_{1} (K) (G (U)) (E (w) \cdot_{{mulGrp}_{K}} y)$
159	16	adantr	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to M \in ({mulGrp}_{K} PrimRoots R)$
160	116 158 159	rspcdva	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to E (w) \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (G (U)) (M) = {eval}_{1} (K) (G (U)) (E (w) \cdot_{{mulGrp}_{K}} M)$
161	160	eqcomd	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to {eval}_{1} (K) (G (U)) (E (w) \cdot_{{mulGrp}_{K}} M) = E (w) \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (G (U)) (M)$
162	17	a1i	$⊢ φ \to H = (h \in ({ℕ_{0}}^{(0 \dots A)}) ⟼ {eval}_{1} (K) (G (h)) (M))$
163	162	reseq1d	$⊢ φ \to {H ↾}_{S} = {(h \in ({ℕ_{0}}^{(0 \dots A)}) ⟼ {eval}_{1} (K) (G (h)) (M)) ↾}_{S}$
164	19	a1i	$⊢ φ \to S = \{s \in ({ℕ_{0}}^{(0 \dots A)}) \| \sum_{t = 0}^{A} s (t) \leq D - 1\}$
165		ssrab2	$⊢ \{s \in ({ℕ_{0}}^{(0 \dots A)}) \| \sum_{t = 0}^{A} s (t) \leq D - 1\} \subseteq {ℕ_{0}}^{(0 \dots A)}$
166	165	a1i	$⊢ φ \to \{s \in ({ℕ_{0}}^{(0 \dots A)}) \| \sum_{t = 0}^{A} s (t) \leq D - 1\} \subseteq {ℕ_{0}}^{(0 \dots A)}$
167	164 166	eqsstrd	$⊢ φ \to S \subseteq {ℕ_{0}}^{(0 \dots A)}$
168	167	resmptd	$⊢ φ \to {(h \in ({ℕ_{0}}^{(0 \dots A)}) ⟼ {eval}_{1} (K) (G (h)) (M)) ↾}_{S} = (h \in S ⟼ {eval}_{1} (K) (G (h)) (M))$
169	163 168	eqtrd	$⊢ φ \to {H ↾}_{S} = (h \in S ⟼ {eval}_{1} (K) (G (h)) (M))$
170		simpr	$⊢ (φ \land h = U) \to h = U$
171	170	fveq2d	$⊢ (φ \land h = U) \to G (h) = G (U)$
172	171	fveq2d	$⊢ (φ \land h = U) \to {eval}_{1} (K) (G (h)) = {eval}_{1} (K) (G (U))$
173	172	fveq1d	$⊢ (φ \land h = U) \to {eval}_{1} (K) (G (h)) (M) = {eval}_{1} (K) (G (U)) (M)$
174		fvexd	$⊢ φ \to {eval}_{1} (K) (G (U)) (M) \in V$
175	169 173 20 174	fvmptd	$⊢ φ \to ({H ↾}_{S}) (U) = {eval}_{1} (K) (G (U)) (M)$
176	175	eqcomd	$⊢ φ \to {eval}_{1} (K) (G (U)) (M) = ({H ↾}_{S}) (U)$
177		simpr	$⊢ (φ \land h = V) \to h = V$
178	177	fveq2d	$⊢ (φ \land h = V) \to G (h) = G (V)$
179	178	fveq2d	$⊢ (φ \land h = V) \to {eval}_{1} (K) (G (h)) = {eval}_{1} (K) (G (V))$
180	179	fveq1d	$⊢ (φ \land h = V) \to {eval}_{1} (K) (G (h)) (M) = {eval}_{1} (K) (G (V)) (M)$
181		fvexd	$⊢ φ \to {eval}_{1} (K) (G (V)) (M) \in V$
182	169 180 21 181	fvmptd	$⊢ φ \to ({H ↾}_{S}) (V) = {eval}_{1} (K) (G (V)) (M)$
183	176 22 182	3eqtrd	$⊢ φ \to {eval}_{1} (K) (G (U)) (M) = {eval}_{1} (K) (G (V)) (M)$
184	183	adantr	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to {eval}_{1} (K) (G (U)) (M) = {eval}_{1} (K) (G (V)) (M)$
185	184	oveq2d	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to E (w) \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (G (U)) (M) = E (w) \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (G (V)) (M)$
186	161 185	eqtrd	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to {eval}_{1} (K) (G (U)) (E (w) \cdot_{{mulGrp}_{K}} M) = E (w) \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (G (V)) (M)$
187		fveq2	$⊢ y = M \to {eval}_{1} (K) (G (V)) (y) = {eval}_{1} (K) (G (V)) (M)$
188	187	oveq2d	$⊢ y = M \to E (w) \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (G (V)) (y) = E (w) \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (G (V)) (M)$
189	114	fveq2d	$⊢ y = M \to {eval}_{1} (K) (G (V)) (E (w) \cdot_{{mulGrp}_{K}} y) = {eval}_{1} (K) (G (V)) (E (w) \cdot_{{mulGrp}_{K}} M)$
190	188 189	eqeq12d	$⊢ y = M \to (E (w) \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (G (V)) (y) = {eval}_{1} (K) (G (V)) (E (w) \cdot_{{mulGrp}_{K}} y) \leftrightarrow E (w) \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (G (V)) (M) = {eval}_{1} (K) (G (V)) (E (w) \cdot_{{mulGrp}_{K}} M))$
191	34 143	elmapd	$⊢ φ \to (V \in ({ℕ_{0}}^{(0 \dots A)}) \leftrightarrow V : (0 \dots A) ⟶ ℕ_{0})$
192	103 191	mpbid	$⊢ φ \to V : (0 \dots A) ⟶ ℕ_{0}$
193	192	adantr	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to V : (0 \dots A) ⟶ ℕ_{0}$
194	1 2 137 138 139 140 141 142 193 10 147 149 151 152 153 154	aks6d1c1rh	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to P^{1^{st} (w)} {(\frac{N}{P})}^{2^{nd} (w)} \underset{˙}{\sim} G (V)$
195	136 194	eqbrtrd	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to E (w) \underset{˙}{\sim} G (V)$
196	1 105 76	aks6d1c1p1	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to (E (w) \underset{˙}{\sim} G (V) \leftrightarrow \forall y \in ({mulGrp}_{K} PrimRoots R) E (w) \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (G (V)) (y) = {eval}_{1} (K) (G (V)) (E (w) \cdot_{{mulGrp}_{K}} y))$
197	195 196	mpbid	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to \forall y \in ({mulGrp}_{K} PrimRoots R) E (w) \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (G (V)) (y) = {eval}_{1} (K) (G (V)) (E (w) \cdot_{{mulGrp}_{K}} y)$
198	190 197 159	rspcdva	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to E (w) \cdot_{{mulGrp}_{K}} {eval}_{1} (K) (G (V)) (M) = {eval}_{1} (K) (G (V)) (E (w) \cdot_{{mulGrp}_{K}} M)$
199	186 198	eqtrd	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to {eval}_{1} (K) (G (U)) (E (w) \cdot_{{mulGrp}_{K}} M) = {eval}_{1} (K) (G (V)) (E (w) \cdot_{{mulGrp}_{K}} M)$
200	66	crnggrpd	$⊢ φ \to K \in Grp$
201	200	adantr	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to K \in Grp$
202	62 63 64 65 67 86 96	fveval1fvcl	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to {eval}_{1} (K) (G (U)) (E (w) \cdot_{{mulGrp}_{K}} M) \in {Base}_{K}$
203	62 63 64 65 67 86 105	fveval1fvcl	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to {eval}_{1} (K) (G (V)) (E (w) \cdot_{{mulGrp}_{K}} M) \in {Base}_{K}$
204		eqid	$⊢ 0_{K} = 0_{K}$
205	64 204 109	grpsubeq0	$⊢ (K \in Grp \land {eval}_{1} (K) (G (U)) (E (w) \cdot_{{mulGrp}_{K}} M) \in {Base}_{K} \land {eval}_{1} (K) (G (V)) (E (w) \cdot_{{mulGrp}_{K}} M) \in {Base}_{K}) \to ({eval}_{1} (K) (G (U)) (E (w) \cdot_{{mulGrp}_{K}} M) -_{K} {eval}_{1} (K) (G (V)) (E (w) \cdot_{{mulGrp}_{K}} M) = 0_{K} \leftrightarrow {eval}_{1} (K) (G (U)) (E (w) \cdot_{{mulGrp}_{K}} M) = {eval}_{1} (K) (G (V)) (E (w) \cdot_{{mulGrp}_{K}} M))$
206	201 202 203 205	syl3anc	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to ({eval}_{1} (K) (G (U)) (E (w) \cdot_{{mulGrp}_{K}} M) -_{K} {eval}_{1} (K) (G (V)) (E (w) \cdot_{{mulGrp}_{K}} M) = 0_{K} \leftrightarrow {eval}_{1} (K) (G (U)) (E (w) \cdot_{{mulGrp}_{K}} M) = {eval}_{1} (K) (G (V)) (E (w) \cdot_{{mulGrp}_{K}} M))$
207	199 206	mpbird	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to {eval}_{1} (K) (G (U)) (E (w) \cdot_{{mulGrp}_{K}} M) -_{K} {eval}_{1} (K) (G (V)) (E (w) \cdot_{{mulGrp}_{K}} M) = 0_{K}$
208	111 207	eqtrd	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to {eval}_{1} (K) (G (U) -_{{Poly}_{1} (K)} G (V)) (E (w) \cdot_{{mulGrp}_{K}} M) = 0_{K}$
209		fvexd	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to {eval}_{1} (K) (G (U) -_{{Poly}_{1} (K)} G (V)) (E (w) \cdot_{{mulGrp}_{K}} M) \in V$
210		elsng	$⊢ {eval}_{1} (K) (G (U) -_{{Poly}_{1} (K)} G (V)) (E (w) \cdot_{{mulGrp}_{K}} M) \in V \to ({eval}_{1} (K) (G (U) -_{{Poly}_{1} (K)} G (V)) (E (w) \cdot_{{mulGrp}_{K}} M) \in \{0_{K}\} \leftrightarrow {eval}_{1} (K) (G (U) -_{{Poly}_{1} (K)} G (V)) (E (w) \cdot_{{mulGrp}_{K}} M) = 0_{K})$
211	209 210	syl	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to ({eval}_{1} (K) (G (U) -_{{Poly}_{1} (K)} G (V)) (E (w) \cdot_{{mulGrp}_{K}} M) \in \{0_{K}\} \leftrightarrow {eval}_{1} (K) (G (U) -_{{Poly}_{1} (K)} G (V)) (E (w) \cdot_{{mulGrp}_{K}} M) = 0_{K})$
212	208 211	mpbird	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to {eval}_{1} (K) (G (U) -_{{Poly}_{1} (K)} G (V)) (E (w) \cdot_{{mulGrp}_{K}} M) \in \{0_{K}\}$
213		eqid	$⊢ K ↑_{𝑠} {Base}_{K} = K ↑_{𝑠} {Base}_{K}$
214	62 63 213 64	evl1rhm	$⊢ K \in CRing \to {eval}_{1} (K) \in ({Poly}_{1} (K) RingHom (K ↑_{𝑠} {Base}_{K}))$
215	66 214	syl	$⊢ φ \to {eval}_{1} (K) \in ({Poly}_{1} (K) RingHom (K ↑_{𝑠} {Base}_{K}))$
216		eqid	$⊢ {Base}_{(K ↑_{𝑠} {Base}_{K})} = {Base}_{(K ↑_{𝑠} {Base}_{K})}$
217	65 216	rhmf	$⊢ {eval}_{1} (K) \in ({Poly}_{1} (K) RingHom (K ↑_{𝑠} {Base}_{K})) \to {eval}_{1} (K) : {Base}_{{Poly}_{1} (K)} ⟶ {Base}_{(K ↑_{𝑠} {Base}_{K})}$
218	215 217	syl	$⊢ φ \to {eval}_{1} (K) : {Base}_{{Poly}_{1} (K)} ⟶ {Base}_{(K ↑_{𝑠} {Base}_{K})}$
219		fvexd	$⊢ φ \to {Base}_{K} \in V$
220	213 64	pwsbas	$⊢ (K \in Field \land {Base}_{K} \in V) \to {Base}_{K}^{{Base}_{K}} = {Base}_{(K ↑_{𝑠} {Base}_{K})}$
221	3 219 220	syl2anc	$⊢ φ \to {Base}_{K}^{{Base}_{K}} = {Base}_{(K ↑_{𝑠} {Base}_{K})}$
222	221	feq3d	$⊢ φ \to ({eval}_{1} (K) : {Base}_{{Poly}_{1} (K)} ⟶ {Base}_{K}^{{Base}_{K}} \leftrightarrow {eval}_{1} (K) : {Base}_{{Poly}_{1} (K)} ⟶ {Base}_{(K ↑_{𝑠} {Base}_{K})})$
223	218 222	mpbird	$⊢ φ \to {eval}_{1} (K) : {Base}_{{Poly}_{1} (K)} ⟶ {Base}_{K}^{{Base}_{K}}$
224	63	ply1ring	$⊢ K \in Ring \to {Poly}_{1} (K) \in Ring$
225	71 224	syl	$⊢ φ \to {Poly}_{1} (K) \in Ring$
226		ringgrp	$⊢ {Poly}_{1} (K) \in Ring \to {Poly}_{1} (K) \in Grp$
227	225 226	syl	$⊢ φ \to {Poly}_{1} (K) \in Grp$
228	65 108	grpsubcl	$⊢ ({Poly}_{1} (K) \in Grp \land G (U) \in {Base}_{{Poly}_{1} (K)} \land G (V) \in {Base}_{{Poly}_{1} (K)}) \to G (U) -_{{Poly}_{1} (K)} G (V) \in {Base}_{{Poly}_{1} (K)}$
229	227 95 104 228	syl3anc	$⊢ φ \to G (U) -_{{Poly}_{1} (K)} G (V) \in {Base}_{{Poly}_{1} (K)}$
230	223 229	ffvelcdmd	$⊢ φ \to {eval}_{1} (K) (G (U) -_{{Poly}_{1} (K)} G (V)) \in ({Base}_{K}^{{Base}_{K}})$
231	219 219	elmapd	$⊢ φ \to ({eval}_{1} (K) (G (U) -_{{Poly}_{1} (K)} G (V)) \in ({Base}_{K}^{{Base}_{K}}) \leftrightarrow {eval}_{1} (K) (G (U) -_{{Poly}_{1} (K)} G (V)) : {Base}_{K} ⟶ {Base}_{K})$
232	230 231	mpbid	$⊢ φ \to {eval}_{1} (K) (G (U) -_{{Poly}_{1} (K)} G (V)) : {Base}_{K} ⟶ {Base}_{K}$
233	232	ffund	$⊢ φ \to Fun {eval}_{1} (K) (G (U) -_{{Poly}_{1} (K)} G (V))$
234	233	adantr	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to Fun {eval}_{1} (K) (G (U) -_{{Poly}_{1} (K)} G (V))$
235	232	ffnd	$⊢ φ \to {eval}_{1} (K) (G (U) -_{{Poly}_{1} (K)} G (V)) Fn {Base}_{K}$
236	235	adantr	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to {eval}_{1} (K) (G (U) -_{{Poly}_{1} (K)} G (V)) Fn {Base}_{K}$
237	236	fndmd	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to dom {eval}_{1} (K) (G (U) -_{{Poly}_{1} (K)} G (V)) = {Base}_{K}$
238	237	eqcomd	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to {Base}_{K} = dom {eval}_{1} (K) (G (U) -_{{Poly}_{1} (K)} G (V))$
239	86 238	eleqtrd	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to E (w) \cdot_{{mulGrp}_{K}} M \in dom {eval}_{1} (K) (G (U) -_{{Poly}_{1} (K)} G (V))$
240		fvimacnv	$⊢ (Fun {eval}_{1} (K) (G (U) -_{{Poly}_{1} (K)} G (V)) \land E (w) \cdot_{{mulGrp}_{K}} M \in dom {eval}_{1} (K) (G (U) -_{{Poly}_{1} (K)} G (V))) \to ({eval}_{1} (K) (G (U) -_{{Poly}_{1} (K)} G (V)) (E (w) \cdot_{{mulGrp}_{K}} M) \in \{0_{K}\} \leftrightarrow E (w) \cdot_{{mulGrp}_{K}} M \in {{eval}_{1} (K) (G (U) -_{{Poly}_{1} (K)} G (V))}^{-1} [\{0_{K}\}])$
241	234 239 240	syl2anc	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to ({eval}_{1} (K) (G (U) -_{{Poly}_{1} (K)} G (V)) (E (w) \cdot_{{mulGrp}_{K}} M) \in \{0_{K}\} \leftrightarrow E (w) \cdot_{{mulGrp}_{K}} M \in {{eval}_{1} (K) (G (U) -_{{Poly}_{1} (K)} G (V))}^{-1} [\{0_{K}\}])$
242	212 241	mpbid	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to E (w) \cdot_{{mulGrp}_{K}} M \in {{eval}_{1} (K) (G (U) -_{{Poly}_{1} (K)} G (V))}^{-1} [\{0_{K}\}]$
243	61 242	eqeltrd	$⊢ (φ \land w \in (ℕ_{0} \times ℕ_{0})) \to J (w) \in {{eval}_{1} (K) (G (U) -_{{Poly}_{1} (K)} G (V))}^{-1} [\{0_{K}\}]$
244	50 54 243	funimassd	$⊢ φ \to J [ℕ_{0} \times ℕ_{0}] \subseteq {{eval}_{1} (K) (G (U) -_{{Poly}_{1} (K)} G (V))}^{-1} [\{0_{K}\}]$
245		hashss	$⊢ ({{eval}_{1} (K) (G (U) -_{{Poly}_{1} (K)} G (V))}^{-1} [\{0_{K}\}] \in V \land J [ℕ_{0} \times ℕ_{0}] \subseteq {{eval}_{1} (K) (G (U) -_{{Poly}_{1} (K)} G (V))}^{-1} [\{0_{K}\}]) \to \|J [ℕ_{0} \times ℕ_{0}]\| \leq \|{{eval}_{1} (K) (G (U) -_{{Poly}_{1} (K)} G (V))}^{-1} [\{0_{K}\}]\|$
246	49 244 245	syl2anc	$⊢ φ \to \|J [ℕ_{0} \times ℕ_{0}]\| \leq \|{{eval}_{1} (K) (G (U) -_{{Poly}_{1} (K)} G (V))}^{-1} [\{0_{K}\}]\|$
247	31 40 46 48 246	xrletrd	$⊢ φ \to D \leq \|{{eval}_{1} (K) (G (U) -_{{Poly}_{1} (K)} G (V))}^{-1} [\{0_{K}\}]\|$

Metamath Proof Explorer

Theorem aks6d1c6lem2

Proof