aks6d1c1p5

Description: The product of exponents is introspective. (Contributed by metakunt, 26-Apr-2025)

	Ref	Expression
Hypotheses	aks6d1c1p5.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))\}$
	aks6d1c1p5.2	$⊢ S = {Poly}_{1} (K)$
	aks6d1c1p5.3	$⊢ B = {Base}_{S}$
	aks6d1c1p5.4	$⊢ X = {var}_{1} (K)$
	aks6d1c1p5.5	$⊢ W = {mulGrp}_{S}$
	aks6d1c1p5.6	$⊢ V = {mulGrp}_{K}$
	aks6d1c1p5.7	$⊢ \underset{˙}{\times} = \cdot_{V}$
	aks6d1c1p5.8	$⊢ C = algSc (S)$
	aks6d1c1p5.10	$⊢ P = chr (K)$
	aks6d1c1p5.11	$⊢ O = {eval}_{1} (K)$
	aks6d1c1p5.12	$⊢ \underset{˙}{+} = +_{S}$
	aks6d1c1p5.13	$⊢ φ \to K \in Field$
	aks6d1c1p5.14	$⊢ φ \to P \in ℙ$
	aks6d1c1p5.15	$⊢ φ \to R \in ℕ$
	aks6d1c1p5.16	$⊢ φ \to E \gcd R = 1$
	aks6d1c1p5.17	$⊢ φ \to P ∥ N$
	aks6d1c1p5.18	$⊢ φ \to D \underset{˙}{\sim} F$
	aks6d1c1p5.19	$⊢ φ \to E \underset{˙}{\sim} F$
Assertion	aks6d1c1p5	$⊢ φ \to D E \underset{˙}{\sim} F$

Proof

Step	Hyp	Ref	Expression
1		aks6d1c1p5.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		aks6d1c1p5.2	$⊢ S = {Poly}_{1} (K)$
3		aks6d1c1p5.3	$⊢ B = {Base}_{S}$
4		aks6d1c1p5.4	$⊢ X = {var}_{1} (K)$
5		aks6d1c1p5.5	$⊢ W = {mulGrp}_{S}$
6		aks6d1c1p5.6	$⊢ V = {mulGrp}_{K}$
7		aks6d1c1p5.7	$⊢ \underset{˙}{\times} = \cdot_{V}$
8		aks6d1c1p5.8	$⊢ C = algSc (S)$
9		aks6d1c1p5.10	$⊢ P = chr (K)$
10		aks6d1c1p5.11	$⊢ O = {eval}_{1} (K)$
11		aks6d1c1p5.12	$⊢ \underset{˙}{+} = +_{S}$
12		aks6d1c1p5.13	$⊢ φ \to K \in Field$
13		aks6d1c1p5.14	$⊢ φ \to P \in ℙ$
14		aks6d1c1p5.15	$⊢ φ \to R \in ℕ$
15		aks6d1c1p5.16	$⊢ φ \to E \gcd R = 1$
16		aks6d1c1p5.17	$⊢ φ \to P ∥ N$
17		aks6d1c1p5.18	$⊢ φ \to D \underset{˙}{\sim} F$
18		aks6d1c1p5.19	$⊢ φ \to E \underset{˙}{\sim} F$
19	12	fldcrngd	$⊢ φ \to K \in CRing$
20	6	crngmgp	$⊢ K \in CRing \to V \in CMnd$
21	19 20	syl	$⊢ φ \to V \in CMnd$
22	21	cmnmndd	$⊢ φ \to V \in Mnd$
23	22	adantr	$⊢ (φ \land y \in (V PrimRoots R)) \to V \in Mnd$
24	1 17	aks6d1c1p1rcl	$⊢ φ \to (D \in ℕ \land F \in B)$
25	24	simpld	$⊢ φ \to D \in ℕ$
26	25	nnnn0d	$⊢ φ \to D \in ℕ_{0}$
27	26	adantr	$⊢ (φ \land y \in (V PrimRoots R)) \to D \in ℕ_{0}$
28	1 18	aks6d1c1p1rcl	$⊢ φ \to (E \in ℕ \land F \in B)$
29	28	simpld	$⊢ φ \to E \in ℕ$
30	29	nnnn0d	$⊢ φ \to E \in ℕ_{0}$
31	30	adantr	$⊢ (φ \land y \in (V PrimRoots R)) \to E \in ℕ_{0}$
32		eqid	$⊢ {Base}_{K} = {Base}_{K}$
33	19	adantr	$⊢ (φ \land y \in (V PrimRoots R)) \to K \in CRing$
34	14	nnnn0d	$⊢ φ \to R \in ℕ_{0}$
35	21 34 7	isprimroot	$⊢ φ \to (y \in (V PrimRoots R) \leftrightarrow (y \in {Base}_{V} \land R \underset{˙}{\times} y = 0_{V} \land \forall q \in ℕ_{0} (q \underset{˙}{\times} y = 0_{V} \to R ∥ q)))$
36	35	biimpd	$⊢ φ \to (y \in (V PrimRoots R) \to (y \in {Base}_{V} \land R \underset{˙}{\times} y = 0_{V} \land \forall q \in ℕ_{0} (q \underset{˙}{\times} y = 0_{V} \to R ∥ q)))$
37	36	imp	$⊢ (φ \land y \in (V PrimRoots R)) \to (y \in {Base}_{V} \land R \underset{˙}{\times} y = 0_{V} \land \forall q \in ℕ_{0} (q \underset{˙}{\times} y = 0_{V} \to R ∥ q))$
38	37	simp1d	$⊢ (φ \land y \in (V PrimRoots R)) \to y \in {Base}_{V}$
39	6 32	mgpbas	$⊢ {Base}_{K} = {Base}_{V}$
40	39	a1i	$⊢ φ \to {Base}_{K} = {Base}_{V}$
41	40	eqcomd	$⊢ φ \to {Base}_{V} = {Base}_{K}$
42	41	adantr	$⊢ (φ \land y \in (V PrimRoots R)) \to {Base}_{V} = {Base}_{K}$
43	38 42	eleqtrd	$⊢ (φ \land y \in (V PrimRoots R)) \to y \in {Base}_{K}$
44	24	simprd	$⊢ φ \to F \in B$
45	44	adantr	$⊢ (φ \land y \in (V PrimRoots R)) \to F \in B$
46	10 2 32 3 33 43 45	fveval1fvcl	$⊢ (φ \land y \in (V PrimRoots R)) \to O (F) (y) \in {Base}_{K}$
47	42	eleq2d	$⊢ (φ \land y \in (V PrimRoots R)) \to (O (F) (y) \in {Base}_{V} \leftrightarrow O (F) (y) \in {Base}_{K})$
48	46 47	mpbird	$⊢ (φ \land y \in (V PrimRoots R)) \to O (F) (y) \in {Base}_{V}$
49	27 31 48	3jca	$⊢ (φ \land y \in (V PrimRoots R)) \to (D \in ℕ_{0} \land E \in ℕ_{0} \land O (F) (y) \in {Base}_{V})$
50		eqid	$⊢ {Base}_{V} = {Base}_{V}$
51	50 7	mulgnn0ass	$⊢ (V \in Mnd \land (D \in ℕ_{0} \land E \in ℕ_{0} \land O (F) (y) \in {Base}_{V})) \to D E \underset{˙}{\times} O (F) (y) = D \underset{˙}{\times} (E \underset{˙}{\times} O (F) (y))$
52	23 49 51	syl2anc	$⊢ (φ \land y \in (V PrimRoots R)) \to D E \underset{˙}{\times} O (F) (y) = D \underset{˙}{\times} (E \underset{˙}{\times} O (F) (y))$
53		eqidd	$⊢ (φ \land y \in (V PrimRoots R)) \to (l \in (V PrimRoots R) ⟼ E \underset{˙}{\times} l) = (l \in (V PrimRoots R) ⟼ E \underset{˙}{\times} l)$
54		simpr	$⊢ ((φ \land y \in (V PrimRoots R)) \land l = y) \to l = y$
55	54	oveq2d	$⊢ ((φ \land y \in (V PrimRoots R)) \land l = y) \to E \underset{˙}{\times} l = E \underset{˙}{\times} y$
56		simpr	$⊢ (φ \land y \in (V PrimRoots R)) \to y \in (V PrimRoots R)$
57	50 7 23 31 38	mulgnn0cld	$⊢ (φ \land y \in (V PrimRoots R)) \to E \underset{˙}{\times} y \in {Base}_{V}$
58	53 55 56 57	fvmptd	$⊢ (φ \land y \in (V PrimRoots R)) \to (l \in (V PrimRoots R) ⟼ E \underset{˙}{\times} l) (y) = E \underset{˙}{\times} y$
59	58	fveq2d	$⊢ (φ \land y \in (V PrimRoots R)) \to O (F) ((l \in (V PrimRoots R) ⟼ E \underset{˙}{\times} l) (y)) = O (F) (E \underset{˙}{\times} y)$
60	59	oveq2d	$⊢ (φ \land y \in (V PrimRoots R)) \to D \underset{˙}{\times} O (F) ((l \in (V PrimRoots R) ⟼ E \underset{˙}{\times} l) (y)) = D \underset{˙}{\times} O (F) (E \underset{˙}{\times} y)$
61	60	eqcomd	$⊢ (φ \land y \in (V PrimRoots R)) \to D \underset{˙}{\times} O (F) (E \underset{˙}{\times} y) = D \underset{˙}{\times} O (F) ((l \in (V PrimRoots R) ⟼ E \underset{˙}{\times} l) (y))$
62		2fveq3	$⊢ i = y \to O (F) ((l \in (V PrimRoots R) ⟼ E \underset{˙}{\times} l) (i)) = O (F) ((l \in (V PrimRoots R) ⟼ E \underset{˙}{\times} l) (y))$
63	62	oveq2d	$⊢ i = y \to D \underset{˙}{\times} O (F) ((l \in (V PrimRoots R) ⟼ E \underset{˙}{\times} l) (i)) = D \underset{˙}{\times} O (F) ((l \in (V PrimRoots R) ⟼ E \underset{˙}{\times} l) (y))$
64		fveq2	$⊢ i = y \to (l \in (V PrimRoots R) ⟼ E \underset{˙}{\times} l) (i) = (l \in (V PrimRoots R) ⟼ E \underset{˙}{\times} l) (y)$
65	64	oveq2d	$⊢ i = y \to D \underset{˙}{\times} (l \in (V PrimRoots R) ⟼ E \underset{˙}{\times} l) (i) = D \underset{˙}{\times} (l \in (V PrimRoots R) ⟼ E \underset{˙}{\times} l) (y)$
66	65	fveq2d	$⊢ i = y \to O (F) (D \underset{˙}{\times} (l \in (V PrimRoots R) ⟼ E \underset{˙}{\times} l) (i)) = O (F) (D \underset{˙}{\times} (l \in (V PrimRoots R) ⟼ E \underset{˙}{\times} l) (y))$
67	63 66	eqeq12d	$⊢ i = y \to (D \underset{˙}{\times} O (F) ((l \in (V PrimRoots R) ⟼ E \underset{˙}{\times} l) (i)) = O (F) (D \underset{˙}{\times} (l \in (V PrimRoots R) ⟼ E \underset{˙}{\times} l) (i)) \leftrightarrow D \underset{˙}{\times} O (F) ((l \in (V PrimRoots R) ⟼ E \underset{˙}{\times} l) (y)) = O (F) (D \underset{˙}{\times} (l \in (V PrimRoots R) ⟼ E \underset{˙}{\times} l) (y)))$
68	1 44 25	aks6d1c1p1	$⊢ φ \to (D \underset{˙}{\sim} F \leftrightarrow \forall y \in (V PrimRoots R) D \underset{˙}{\times} O (F) (y) = O (F) (D \underset{˙}{\times} y))$
69	68	biimpd	$⊢ φ \to (D \underset{˙}{\sim} F \to \forall y \in (V PrimRoots R) D \underset{˙}{\times} O (F) (y) = O (F) (D \underset{˙}{\times} y))$
70	17 69	mpd	$⊢ φ \to \forall y \in (V PrimRoots R) D \underset{˙}{\times} O (F) (y) = O (F) (D \underset{˙}{\times} y)$
71	7	oveqi	$⊢ E \underset{˙}{\times} l = E \cdot_{V} l$
72	71	a1i	$⊢ l \in (V PrimRoots R) \to E \underset{˙}{\times} l = E \cdot_{V} l$
73	72	mpteq2ia	$⊢ (l \in (V PrimRoots R) ⟼ E \underset{˙}{\times} l) = (l \in (V PrimRoots R) ⟼ E \cdot_{V} l)$
74	73 21 14 29 15	primrootscoprbij2	$⊢ φ \to (l \in (V PrimRoots R) ⟼ E \underset{˙}{\times} l) : V PrimRoots R \underset{1-1 onto}{⟶} V PrimRoots R$
75		f1ofo	$⊢ (l \in (V PrimRoots R) ⟼ E \underset{˙}{\times} l) : V PrimRoots R \underset{1-1 onto}{⟶} V PrimRoots R \to (l \in (V PrimRoots R) ⟼ E \underset{˙}{\times} l) : V PrimRoots R \underset{onto}{⟶} V PrimRoots R$
76	74 75	syl	$⊢ φ \to (l \in (V PrimRoots R) ⟼ E \underset{˙}{\times} l) : V PrimRoots R \underset{onto}{⟶} V PrimRoots R$
77		fveq2	$⊢ (l \in (V PrimRoots R) ⟼ E \underset{˙}{\times} l) (i) = y \to O (F) ((l \in (V PrimRoots R) ⟼ E \underset{˙}{\times} l) (i)) = O (F) (y)$
78	77	oveq2d	$⊢ (l \in (V PrimRoots R) ⟼ E \underset{˙}{\times} l) (i) = y \to D \underset{˙}{\times} O (F) ((l \in (V PrimRoots R) ⟼ E \underset{˙}{\times} l) (i)) = D \underset{˙}{\times} O (F) (y)$
79		oveq2	$⊢ (l \in (V PrimRoots R) ⟼ E \underset{˙}{\times} l) (i) = y \to D \underset{˙}{\times} (l \in (V PrimRoots R) ⟼ E \underset{˙}{\times} l) (i) = D \underset{˙}{\times} y$
80	79	fveq2d	$⊢ (l \in (V PrimRoots R) ⟼ E \underset{˙}{\times} l) (i) = y \to O (F) (D \underset{˙}{\times} (l \in (V PrimRoots R) ⟼ E \underset{˙}{\times} l) (i)) = O (F) (D \underset{˙}{\times} y)$
81	78 80	eqeq12d	$⊢ (l \in (V PrimRoots R) ⟼ E \underset{˙}{\times} l) (i) = y \to (D \underset{˙}{\times} O (F) ((l \in (V PrimRoots R) ⟼ E \underset{˙}{\times} l) (i)) = O (F) (D \underset{˙}{\times} (l \in (V PrimRoots R) ⟼ E \underset{˙}{\times} l) (i)) \leftrightarrow D \underset{˙}{\times} O (F) (y) = O (F) (D \underset{˙}{\times} y))$
82	81	cbvfo	$⊢ (l \in (V PrimRoots R) ⟼ E \underset{˙}{\times} l) : V PrimRoots R \underset{onto}{⟶} V PrimRoots R \to (\forall i \in (V PrimRoots R) D \underset{˙}{\times} O (F) ((l \in (V PrimRoots R) ⟼ E \underset{˙}{\times} l) (i)) = O (F) (D \underset{˙}{\times} (l \in (V PrimRoots R) ⟼ E \underset{˙}{\times} l) (i)) \leftrightarrow \forall y \in (V PrimRoots R) D \underset{˙}{\times} O (F) (y) = O (F) (D \underset{˙}{\times} y))$
83	76 82	syl	$⊢ φ \to (\forall i \in (V PrimRoots R) D \underset{˙}{\times} O (F) ((l \in (V PrimRoots R) ⟼ E \underset{˙}{\times} l) (i)) = O (F) (D \underset{˙}{\times} (l \in (V PrimRoots R) ⟼ E \underset{˙}{\times} l) (i)) \leftrightarrow \forall y \in (V PrimRoots R) D \underset{˙}{\times} O (F) (y) = O (F) (D \underset{˙}{\times} y))$
84	70 83	mpbird	$⊢ φ \to \forall i \in (V PrimRoots R) D \underset{˙}{\times} O (F) ((l \in (V PrimRoots R) ⟼ E \underset{˙}{\times} l) (i)) = O (F) (D \underset{˙}{\times} (l \in (V PrimRoots R) ⟼ E \underset{˙}{\times} l) (i))$
85	84	adantr	$⊢ (φ \land y \in (V PrimRoots R)) \to \forall i \in (V PrimRoots R) D \underset{˙}{\times} O (F) ((l \in (V PrimRoots R) ⟼ E \underset{˙}{\times} l) (i)) = O (F) (D \underset{˙}{\times} (l \in (V PrimRoots R) ⟼ E \underset{˙}{\times} l) (i))$
86	67 85 56	rspcdva	$⊢ (φ \land y \in (V PrimRoots R)) \to D \underset{˙}{\times} O (F) ((l \in (V PrimRoots R) ⟼ E \underset{˙}{\times} l) (y)) = O (F) (D \underset{˙}{\times} (l \in (V PrimRoots R) ⟼ E \underset{˙}{\times} l) (y))$
87	58	oveq2d	$⊢ (φ \land y \in (V PrimRoots R)) \to D \underset{˙}{\times} (l \in (V PrimRoots R) ⟼ E \underset{˙}{\times} l) (y) = D \underset{˙}{\times} (E \underset{˙}{\times} y)$
88	87	fveq2d	$⊢ (φ \land y \in (V PrimRoots R)) \to O (F) (D \underset{˙}{\times} (l \in (V PrimRoots R) ⟼ E \underset{˙}{\times} l) (y)) = O (F) (D \underset{˙}{\times} (E \underset{˙}{\times} y))$
89	86 88	eqtrd	$⊢ (φ \land y \in (V PrimRoots R)) \to D \underset{˙}{\times} O (F) ((l \in (V PrimRoots R) ⟼ E \underset{˙}{\times} l) (y)) = O (F) (D \underset{˙}{\times} (E \underset{˙}{\times} y))$
90	61 89	eqtr2d	$⊢ (φ \land y \in (V PrimRoots R)) \to O (F) (D \underset{˙}{\times} (E \underset{˙}{\times} y)) = D \underset{˙}{\times} O (F) (E \underset{˙}{\times} y)$
91		fveq2	$⊢ z = y \to O (F) (z) = O (F) (y)$
92	91	oveq2d	$⊢ z = y \to E \underset{˙}{\times} O (F) (z) = E \underset{˙}{\times} O (F) (y)$
93		oveq2	$⊢ z = y \to E \underset{˙}{\times} z = E \underset{˙}{\times} y$
94	93	fveq2d	$⊢ z = y \to O (F) (E \underset{˙}{\times} z) = O (F) (E \underset{˙}{\times} y)$
95	92 94	eqeq12d	$⊢ z = y \to (E \underset{˙}{\times} O (F) (z) = O (F) (E \underset{˙}{\times} z) \leftrightarrow E \underset{˙}{\times} O (F) (y) = O (F) (E \underset{˙}{\times} y))$
96	1 44 29	aks6d1c1p1	$⊢ φ \to (E \underset{˙}{\sim} F \leftrightarrow \forall y \in (V PrimRoots R) E \underset{˙}{\times} O (F) (y) = O (F) (E \underset{˙}{\times} y))$
97	96	biimpd	$⊢ φ \to (E \underset{˙}{\sim} F \to \forall y \in (V PrimRoots R) E \underset{˙}{\times} O (F) (y) = O (F) (E \underset{˙}{\times} y))$
98	18 97	mpd	$⊢ φ \to \forall y \in (V PrimRoots R) E \underset{˙}{\times} O (F) (y) = O (F) (E \underset{˙}{\times} y)$
99		nfv	$⊢ Ⅎ y E \underset{˙}{\times} O (F) (z) = O (F) (E \underset{˙}{\times} z)$
100		nfv	$⊢ Ⅎ z E \underset{˙}{\times} O (F) (y) = O (F) (E \underset{˙}{\times} y)$
101	99 100 95	cbvralw	$⊢ \forall z \in (V PrimRoots R) E \underset{˙}{\times} O (F) (z) = O (F) (E \underset{˙}{\times} z) \leftrightarrow \forall y \in (V PrimRoots R) E \underset{˙}{\times} O (F) (y) = O (F) (E \underset{˙}{\times} y)$
102	98 101	sylibr	$⊢ φ \to \forall z \in (V PrimRoots R) E \underset{˙}{\times} O (F) (z) = O (F) (E \underset{˙}{\times} z)$
103	102	adantr	$⊢ (φ \land y \in (V PrimRoots R)) \to \forall z \in (V PrimRoots R) E \underset{˙}{\times} O (F) (z) = O (F) (E \underset{˙}{\times} z)$
104	95 103 56	rspcdva	$⊢ (φ \land y \in (V PrimRoots R)) \to E \underset{˙}{\times} O (F) (y) = O (F) (E \underset{˙}{\times} y)$
105	104	eqcomd	$⊢ (φ \land y \in (V PrimRoots R)) \to O (F) (E \underset{˙}{\times} y) = E \underset{˙}{\times} O (F) (y)$
106	105	oveq2d	$⊢ (φ \land y \in (V PrimRoots R)) \to D \underset{˙}{\times} O (F) (E \underset{˙}{\times} y) = D \underset{˙}{\times} (E \underset{˙}{\times} O (F) (y))$
107	90 106	eqtrd	$⊢ (φ \land y \in (V PrimRoots R)) \to O (F) (D \underset{˙}{\times} (E \underset{˙}{\times} y)) = D \underset{˙}{\times} (E \underset{˙}{\times} O (F) (y))$
108	107	eqcomd	$⊢ (φ \land y \in (V PrimRoots R)) \to D \underset{˙}{\times} (E \underset{˙}{\times} O (F) (y)) = O (F) (D \underset{˙}{\times} (E \underset{˙}{\times} y))$
109	27 31 38	3jca	$⊢ (φ \land y \in (V PrimRoots R)) \to (D \in ℕ_{0} \land E \in ℕ_{0} \land y \in {Base}_{V})$
110	50 7	mulgnn0ass	$⊢ (V \in Mnd \land (D \in ℕ_{0} \land E \in ℕ_{0} \land y \in {Base}_{V})) \to D E \underset{˙}{\times} y = D \underset{˙}{\times} (E \underset{˙}{\times} y)$
111	110	eqcomd	$⊢ (V \in Mnd \land (D \in ℕ_{0} \land E \in ℕ_{0} \land y \in {Base}_{V})) \to D \underset{˙}{\times} (E \underset{˙}{\times} y) = D E \underset{˙}{\times} y$
112	23 109 111	syl2anc	$⊢ (φ \land y \in (V PrimRoots R)) \to D \underset{˙}{\times} (E \underset{˙}{\times} y) = D E \underset{˙}{\times} y$
113	112	fveq2d	$⊢ (φ \land y \in (V PrimRoots R)) \to O (F) (D \underset{˙}{\times} (E \underset{˙}{\times} y)) = O (F) (D E \underset{˙}{\times} y)$
114	52 108 113	3eqtrd	$⊢ (φ \land y \in (V PrimRoots R)) \to D E \underset{˙}{\times} O (F) (y) = O (F) (D E \underset{˙}{\times} y)$
115	114	ralrimiva	$⊢ φ \to \forall y \in (V PrimRoots R) D E \underset{˙}{\times} O (F) (y) = O (F) (D E \underset{˙}{\times} y)$
116	25 29	nnmulcld	$⊢ φ \to D E \in ℕ$
117	1 44 116	aks6d1c1p1	$⊢ φ \to (D E \underset{˙}{\sim} F \leftrightarrow \forall y \in (V PrimRoots R) D E \underset{˙}{\times} O (F) (y) = O (F) (D E \underset{˙}{\times} y))$
118	115 117	mpbird	$⊢ φ \to D E \underset{˙}{\sim} F$

Metamath Proof Explorer

Theorem aks6d1c1p5

Proof