aks6d1c1p7

Description: X is introspective to all positive integers. (Contributed by metakunt, 30-Apr-2025)

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

Proof

Step	Hyp	Ref	Expression
1		aks6d1c1p7.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		aks6d1c1p7.2	$⊢ S = {Poly}_{1} (K)$
3		aks6d1c1p7.3	$⊢ B = {Base}_{S}$
4		aks6d1c1p7.4	$⊢ X = {var}_{1} (K)$
5		aks6d1c1p7.5	$⊢ V = {mulGrp}_{K}$
6		aks6d1c1p7.6	$⊢ \underset{˙}{\times} = \cdot_{V}$
7		aks6d1c1p7.7	$⊢ P = chr (K)$
8		aks6d1c1p7.8	$⊢ O = {eval}_{1} (K)$
9		aks6d1c1p7.9	$⊢ φ \to K \in Field$
10		aks6d1c1p7.10	$⊢ φ \to P \in ℙ$
11		aks6d1c1p7.11	$⊢ φ \to R \in ℕ$
12		aks6d1c1p7.12	$⊢ φ \to N \in ℕ$
13		aks6d1c1p7.13	$⊢ φ \to P ∥ N$
14		aks6d1c1p7.14	$⊢ φ \to N \gcd R = 1$
15		aks6d1c1p7.15	$⊢ φ \to L \in ℕ$
16		eqid	$⊢ {Base}_{K} = {Base}_{K}$
17	9	fldcrngd	$⊢ φ \to K \in CRing$
18	17	adantr	$⊢ (φ \land y \in (V PrimRoots R)) \to K \in CRing$
19	5	crngmgp	$⊢ K \in CRing \to V \in CMnd$
20	17 19	syl	$⊢ φ \to V \in CMnd$
21	11	nnnn0d	$⊢ φ \to R \in ℕ_{0}$
22	20 21 6	isprimroot	$⊢ φ \to (y \in (V PrimRoots R) \leftrightarrow (y \in {Base}_{V} \land R \underset{˙}{\times} y = 0_{V} \land \forall l \in ℕ_{0} (l \underset{˙}{\times} y = 0_{V} \to R ∥ l)))$
23	22	biimpd	$⊢ φ \to (y \in (V PrimRoots R) \to (y \in {Base}_{V} \land R \underset{˙}{\times} y = 0_{V} \land \forall l \in ℕ_{0} (l \underset{˙}{\times} y = 0_{V} \to R ∥ l)))$
24	23	imp	$⊢ (φ \land y \in (V PrimRoots R)) \to (y \in {Base}_{V} \land R \underset{˙}{\times} y = 0_{V} \land \forall l \in ℕ_{0} (l \underset{˙}{\times} y = 0_{V} \to R ∥ l))$
25	24	simp1d	$⊢ (φ \land y \in (V PrimRoots R)) \to y \in {Base}_{V}$
26	5 16	mgpbas	$⊢ {Base}_{K} = {Base}_{V}$
27	25 26	eleqtrrdi	$⊢ (φ \land y \in (V PrimRoots R)) \to y \in {Base}_{K}$
28	8 4 16 2 3 18 27	evl1vard	$⊢ (φ \land y \in (V PrimRoots R)) \to (X \in B \land O (X) (y) = y)$
29	28	simprd	$⊢ (φ \land y \in (V PrimRoots R)) \to O (X) (y) = y$
30	29	oveq2d	$⊢ (φ \land y \in (V PrimRoots R)) \to L \underset{˙}{\times} O (X) (y) = L \underset{˙}{\times} y$
31	20	cmnmndd	$⊢ φ \to V \in Mnd$
32	31	adantr	$⊢ (φ \land y \in (V PrimRoots R)) \to V \in Mnd$
33	15	nnnn0d	$⊢ φ \to L \in ℕ_{0}$
34	33	adantr	$⊢ (φ \land y \in (V PrimRoots R)) \to L \in ℕ_{0}$
35	27 26	eleqtrdi	$⊢ (φ \land y \in (V PrimRoots R)) \to y \in {Base}_{V}$
36		eqid	$⊢ {Base}_{V} = {Base}_{V}$
37	36 6	mulgnn0cl	$⊢ (V \in Mnd \land L \in ℕ_{0} \land y \in {Base}_{V}) \to L \underset{˙}{\times} y \in {Base}_{V}$
38	32 34 35 37	syl3anc	$⊢ (φ \land y \in (V PrimRoots R)) \to L \underset{˙}{\times} y \in {Base}_{V}$
39	38 26	eleqtrrdi	$⊢ (φ \land y \in (V PrimRoots R)) \to L \underset{˙}{\times} y \in {Base}_{K}$
40	8 4 16 2 3 18 39	evl1vard	$⊢ (φ \land y \in (V PrimRoots R)) \to (X \in B \land O (X) (L \underset{˙}{\times} y) = L \underset{˙}{\times} y)$
41	40	simprd	$⊢ (φ \land y \in (V PrimRoots R)) \to O (X) (L \underset{˙}{\times} y) = L \underset{˙}{\times} y$
42		eqidd	$⊢ (φ \land y \in (V PrimRoots R)) \to L \underset{˙}{\times} y = L \underset{˙}{\times} y$
43	41 42	eqtr2d	$⊢ (φ \land y \in (V PrimRoots R)) \to L \underset{˙}{\times} y = O (X) (L \underset{˙}{\times} y)$
44	30 43	eqtrd	$⊢ (φ \land y \in (V PrimRoots R)) \to L \underset{˙}{\times} O (X) (y) = O (X) (L \underset{˙}{\times} y)$
45	44	ralrimiva	$⊢ φ \to \forall y \in (V PrimRoots R) L \underset{˙}{\times} O (X) (y) = O (X) (L \underset{˙}{\times} y)$
46		crngring	$⊢ K \in CRing \to K \in Ring$
47	17 46	syl	$⊢ φ \to K \in Ring$
48		eqid	$⊢ {Base}_{S} = {Base}_{S}$
49	4 2 48	vr1cl	$⊢ K \in Ring \to X \in {Base}_{S}$
50	47 49	syl	$⊢ φ \to X \in {Base}_{S}$
51	50 3	eleqtrrdi	$⊢ φ \to X \in B$
52	1 51 15	aks6d1c1p1	$⊢ φ \to (L \underset{˙}{\sim} X \leftrightarrow \forall y \in (V PrimRoots R) L \underset{˙}{\times} O (X) (y) = O (X) (L \underset{˙}{\times} y))$
53	45 52	mpbird	$⊢ φ \to L \underset{˙}{\sim} X$

Metamath Proof Explorer

Theorem aks6d1c1p7

Proof