aks6d1c1p3

Description: In a field with a Frobenius isomorphism (read: algebraic closure or finite field), N and linear factors are introspective. (Contributed by metakunt, 25-Apr-2025)

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

Proof

Step	Hyp	Ref	Expression
1		aks6d1c1p3.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		aks6d1c1p3.2	$⊢ S = {Poly}_{1} (K)$
3		aks6d1c1p3.3	$⊢ B = {Base}_{S}$
4		aks6d1c1p3.4	$⊢ X = {var}_{1} (K)$
5		aks6d1c1p3.5	$⊢ W = {mulGrp}_{S}$
6		aks6d1c1p3.6	$⊢ V = {mulGrp}_{K}$
7		aks6d1c1p3.7	$⊢ \underset{˙}{\times} = \cdot_{V}$
8		aks6d1c1p3.8	$⊢ C = algSc (S)$
9		aks6d1c1p3.9	$⊢ D = \cdot_{W}$
10		aks6d1c1p3.10	$⊢ P = chr (K)$
11		aks6d1c1p3.11	$⊢ O = {eval}_{1} (K)$
12		aks6d1c1p3.12	$⊢ \underset{˙}{+} = +_{S}$
13		aks6d1c1p3.13	$⊢ φ \to K \in Field$
14		aks6d1c1p3.14	$⊢ φ \to P \in ℙ$
15		aks6d1c1p3.15	$⊢ φ \to R \in ℕ$
16		aks6d1c1p3.16	$⊢ φ \to N \gcd R = 1$
17		aks6d1c1p3.17	$⊢ φ \to P ∥ N$
18		aks6d1c1p3.18	$⊢ F = X \underset{˙}{+} C (ℤRHom (K) (A))$
19		aks6d1c1p3.19	$⊢ φ \to A \in ℤ$
20		aks6d1c1p3.20	$⊢ φ \to N \underset{˙}{\sim} F$
21		aks6d1c1p3.21	$⊢ φ \to (x \in {Base}_{K} ⟼ P \underset{˙}{\times} x) \in (K RingIso K)$
22	18	a1i	$⊢ (φ \land y \in (V PrimRoots R)) \to F = X \underset{˙}{+} C (ℤRHom (K) (A))$
23	22	fveq2d	$⊢ (φ \land y \in (V PrimRoots R)) \to O (F) = O (X \underset{˙}{+} C (ℤRHom (K) (A)))$
24	23	fveq1d	$⊢ (φ \land y \in (V PrimRoots R)) \to O (F) ((\frac{N}{P}) \underset{˙}{\times} y) = O (X \underset{˙}{+} C (ℤRHom (K) (A))) ((\frac{N}{P}) \underset{˙}{\times} y)$
25		eqid	$⊢ {Base}_{K} = {Base}_{K}$
26	13	fldcrngd	$⊢ φ \to K \in CRing$
27	26	adantr	$⊢ (φ \land y \in (V PrimRoots R)) \to K \in CRing$
28		eqid	$⊢ {Base}_{V} = {Base}_{V}$
29	6	crngmgp	$⊢ K \in CRing \to V \in CMnd$
30	26 29	syl	$⊢ φ \to V \in CMnd$
31	30	cmnmndd	$⊢ φ \to V \in Mnd$
32	31	adantr	$⊢ (φ \land y \in (V PrimRoots R)) \to V \in Mnd$
33	1 20	aks6d1c1p1rcl	$⊢ φ \to (N \in ℕ \land F \in B)$
34	33	simpld	$⊢ φ \to N \in ℕ$
35		prmnn	$⊢ P \in ℙ \to P \in ℕ$
36	14 35	syl	$⊢ φ \to P \in ℕ$
37		nndivdvds	$⊢ (N \in ℕ \land P \in ℕ) \to (P ∥ N \leftrightarrow \frac{N}{P} \in ℕ)$
38	34 36 37	syl2anc	$⊢ φ \to (P ∥ N \leftrightarrow \frac{N}{P} \in ℕ)$
39	17 38	mpbid	$⊢ φ \to \frac{N}{P} \in ℕ$
40	39	nnnn0d	$⊢ φ \to \frac{N}{P} \in ℕ_{0}$
41	40	adantr	$⊢ (φ \land y \in (V PrimRoots R)) \to \frac{N}{P} \in ℕ_{0}$
42	15	nnnn0d	$⊢ φ \to R \in ℕ_{0}$
43	30 42 7	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)))$
44	43	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)))$
45	44	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))$
46	45	simp1d	$⊢ (φ \land y \in (V PrimRoots R)) \to y \in {Base}_{V}$
47	28 7 32 41 46	mulgnn0cld	$⊢ (φ \land y \in (V PrimRoots R)) \to (\frac{N}{P}) \underset{˙}{\times} y \in {Base}_{V}$
48	6 25	mgpbas	$⊢ {Base}_{K} = {Base}_{V}$
49	48	eqcomi	$⊢ {Base}_{V} = {Base}_{K}$
50	49	a1i	$⊢ φ \to {Base}_{V} = {Base}_{K}$
51	50	adantr	$⊢ (φ \land y \in (V PrimRoots R)) \to {Base}_{V} = {Base}_{K}$
52	47 51	eleqtrd	$⊢ (φ \land y \in (V PrimRoots R)) \to (\frac{N}{P}) \underset{˙}{\times} y \in {Base}_{K}$
53	11 4 25 2 3 27 52	evl1vard	$⊢ (φ \land y \in (V PrimRoots R)) \to (X \in B \land O (X) ((\frac{N}{P}) \underset{˙}{\times} y) = (\frac{N}{P}) \underset{˙}{\times} y)$
54	26	crngringd	$⊢ φ \to K \in Ring$
55		eqid	$⊢ ℤRHom (K) = ℤRHom (K)$
56	55	zrhrhm	$⊢ K \in Ring \to ℤRHom (K) \in (ℤ_{ring} RingHom K)$
57		rhmghm	$⊢ ℤRHom (K) \in (ℤ_{ring} RingHom K) \to ℤRHom (K) \in (ℤ_{ring} GrpHom K)$
58		zringbas	$⊢ ℤ = {Base}_{ℤ_{ring}}$
59	58 25	ghmf	$⊢ ℤRHom (K) \in (ℤ_{ring} GrpHom K) \to ℤRHom (K) : ℤ ⟶ {Base}_{K}$
60	54 56 57 59	4syl	$⊢ φ \to ℤRHom (K) : ℤ ⟶ {Base}_{K}$
61	60 19	ffvelcdmd	$⊢ φ \to ℤRHom (K) (A) \in {Base}_{K}$
62	61	adantr	$⊢ (φ \land y \in (V PrimRoots R)) \to ℤRHom (K) (A) \in {Base}_{K}$
63	11 2 25 8 3 27 62 52	evl1scad	$⊢ (φ \land y \in (V PrimRoots R)) \to (C (ℤRHom (K) (A)) \in B \land O (C (ℤRHom (K) (A))) ((\frac{N}{P}) \underset{˙}{\times} y) = ℤRHom (K) (A))$
64		eqid	$⊢ +_{K} = +_{K}$
65	11 2 25 3 27 52 53 63 12 64	evl1addd	$⊢ (φ \land y \in (V PrimRoots R)) \to (X \underset{˙}{+} C (ℤRHom (K) (A)) \in B \land O (X \underset{˙}{+} C (ℤRHom (K) (A))) ((\frac{N}{P}) \underset{˙}{\times} y) = ((\frac{N}{P}) \underset{˙}{\times} y) +_{K} ℤRHom (K) (A))$
66	65	simprd	$⊢ (φ \land y \in (V PrimRoots R)) \to O (X \underset{˙}{+} C (ℤRHom (K) (A))) ((\frac{N}{P}) \underset{˙}{\times} y) = ((\frac{N}{P}) \underset{˙}{\times} y) +_{K} ℤRHom (K) (A)$
67	24 66	eqtrd	$⊢ (φ \land y \in (V PrimRoots R)) \to O (F) ((\frac{N}{P}) \underset{˙}{\times} y) = ((\frac{N}{P}) \underset{˙}{\times} y) +_{K} ℤRHom (K) (A)$
68	23	fveq1d	$⊢ (φ \land y \in (V PrimRoots R)) \to O (F) (y) = O (X \underset{˙}{+} C (ℤRHom (K) (A))) (y)$
69	68	oveq2d	$⊢ (φ \land y \in (V PrimRoots R)) \to (\frac{N}{P}) \underset{˙}{\times} O (F) (y) = (\frac{N}{P}) \underset{˙}{\times} O (X \underset{˙}{+} C (ℤRHom (K) (A))) (y)$
70	51	eleq2d	$⊢ (φ \land y \in (V PrimRoots R)) \to (y \in {Base}_{V} \leftrightarrow y \in {Base}_{K})$
71	46 70	mpbid	$⊢ (φ \land y \in (V PrimRoots R)) \to y \in {Base}_{K}$
72	11 4 49 2 3 27 46	evl1vard	$⊢ (φ \land y \in (V PrimRoots R)) \to (X \in B \land O (X) (y) = y)$
73	11 2 25 8 3 27 62 71	evl1scad	$⊢ (φ \land y \in (V PrimRoots R)) \to (C (ℤRHom (K) (A)) \in B \land O (C (ℤRHom (K) (A))) (y) = ℤRHom (K) (A))$
74	11 2 25 3 27 71 72 73 12 64	evl1addd	$⊢ (φ \land y \in (V PrimRoots R)) \to (X \underset{˙}{+} C (ℤRHom (K) (A)) \in B \land O (X \underset{˙}{+} C (ℤRHom (K) (A))) (y) = y +_{K} ℤRHom (K) (A))$
75	74	simprd	$⊢ (φ \land y \in (V PrimRoots R)) \to O (X \underset{˙}{+} C (ℤRHom (K) (A))) (y) = y +_{K} ℤRHom (K) (A)$
76	75	oveq2d	$⊢ (φ \land y \in (V PrimRoots R)) \to (\frac{N}{P}) \underset{˙}{\times} O (X \underset{˙}{+} C (ℤRHom (K) (A))) (y) = (\frac{N}{P}) \underset{˙}{\times} (y +_{K} ℤRHom (K) (A))$
77	69 76	eqtrd	$⊢ (φ \land y \in (V PrimRoots R)) \to (\frac{N}{P}) \underset{˙}{\times} O (F) (y) = (\frac{N}{P}) \underset{˙}{\times} (y +_{K} ℤRHom (K) (A))$
78	25 25	isrim	$⊢ (x \in {Base}_{K} ⟼ P \underset{˙}{\times} x) \in (K RingIso K) \leftrightarrow ((x \in {Base}_{K} ⟼ P \underset{˙}{\times} x) \in (K RingHom K) \land (x \in {Base}_{K} ⟼ P \underset{˙}{\times} x) : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K})$
79	21 78	sylib	$⊢ φ \to ((x \in {Base}_{K} ⟼ P \underset{˙}{\times} x) \in (K RingHom K) \land (x \in {Base}_{K} ⟼ P \underset{˙}{\times} x) : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K})$
80	79	simprd	$⊢ φ \to (x \in {Base}_{K} ⟼ P \underset{˙}{\times} x) : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K}$
81	80	adantr	$⊢ (φ \land y \in (V PrimRoots R)) \to (x \in {Base}_{K} ⟼ P \underset{˙}{\times} x) : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K}$
82	27	crnggrpd	$⊢ (φ \land y \in (V PrimRoots R)) \to K \in Grp$
83	25 64 82 52 62	grpcld	$⊢ (φ \land y \in (V PrimRoots R)) \to ((\frac{N}{P}) \underset{˙}{\times} y) +_{K} ℤRHom (K) (A) \in {Base}_{K}$
84		f1ocnvfv1	$⊢ ((x \in {Base}_{K} ⟼ P \underset{˙}{\times} x) : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K} \land ((\frac{N}{P}) \underset{˙}{\times} y) +_{K} ℤRHom (K) (A) \in {Base}_{K}) \to {(x \in {Base}_{K} ⟼ P \underset{˙}{\times} x)}^{-1} ((x \in {Base}_{K} ⟼ P \underset{˙}{\times} x) (((\frac{N}{P}) \underset{˙}{\times} y) +_{K} ℤRHom (K) (A))) = ((\frac{N}{P}) \underset{˙}{\times} y) +_{K} ℤRHom (K) (A)$
85	81 83 84	syl2anc	$⊢ (φ \land y \in (V PrimRoots R)) \to {(x \in {Base}_{K} ⟼ P \underset{˙}{\times} x)}^{-1} ((x \in {Base}_{K} ⟼ P \underset{˙}{\times} x) (((\frac{N}{P}) \underset{˙}{\times} y) +_{K} ℤRHom (K) (A))) = ((\frac{N}{P}) \underset{˙}{\times} y) +_{K} ℤRHom (K) (A)$
86	85	eqcomd	$⊢ (φ \land y \in (V PrimRoots R)) \to ((\frac{N}{P}) \underset{˙}{\times} y) +_{K} ℤRHom (K) (A) = {(x \in {Base}_{K} ⟼ P \underset{˙}{\times} x)}^{-1} ((x \in {Base}_{K} ⟼ P \underset{˙}{\times} x) (((\frac{N}{P}) \underset{˙}{\times} y) +_{K} ℤRHom (K) (A)))$
87		eqidd	$⊢ (φ \land y \in (V PrimRoots R)) \to (x \in {Base}_{K} ⟼ P \underset{˙}{\times} x) = (x \in {Base}_{K} ⟼ P \underset{˙}{\times} x)$
88		id	$⊢ x = ((\frac{N}{P}) \underset{˙}{\times} y) +_{K} ℤRHom (K) (A) \to x = ((\frac{N}{P}) \underset{˙}{\times} y) +_{K} ℤRHom (K) (A)$
89	88	adantl	$⊢ ((φ \land y \in (V PrimRoots R)) \land x = ((\frac{N}{P}) \underset{˙}{\times} y) +_{K} ℤRHom (K) (A)) \to x = ((\frac{N}{P}) \underset{˙}{\times} y) +_{K} ℤRHom (K) (A)$
90	89	oveq2d	$⊢ ((φ \land y \in (V PrimRoots R)) \land x = ((\frac{N}{P}) \underset{˙}{\times} y) +_{K} ℤRHom (K) (A)) \to P \underset{˙}{\times} x = P \underset{˙}{\times} (((\frac{N}{P}) \underset{˙}{\times} y) +_{K} ℤRHom (K) (A))$
91		eqid	$⊢ {mulGrp}_{K} = {mulGrp}_{K}$
92	91 25	mgpbas	$⊢ {Base}_{K} = {Base}_{{mulGrp}_{K}}$
93	6	fveq2i	$⊢ \cdot_{V} = \cdot_{{mulGrp}_{K}}$
94	7 93	eqtri	$⊢ \underset{˙}{\times} = \cdot_{{mulGrp}_{K}}$
95	91	ringmgp	$⊢ K \in Ring \to {mulGrp}_{K} \in Mnd$
96	54 95	syl	$⊢ φ \to {mulGrp}_{K} \in Mnd$
97	96	adantr	$⊢ (φ \land y \in (V PrimRoots R)) \to {mulGrp}_{K} \in Mnd$
98	36	nnnn0d	$⊢ φ \to P \in ℕ_{0}$
99	98	adantr	$⊢ (φ \land y \in (V PrimRoots R)) \to P \in ℕ_{0}$
100	92 94 97 99 83	mulgnn0cld	$⊢ (φ \land y \in (V PrimRoots R)) \to P \underset{˙}{\times} (((\frac{N}{P}) \underset{˙}{\times} y) +_{K} ℤRHom (K) (A)) \in {Base}_{K}$
101	87 90 83 100	fvmptd	$⊢ (φ \land y \in (V PrimRoots R)) \to (x \in {Base}_{K} ⟼ P \underset{˙}{\times} x) (((\frac{N}{P}) \underset{˙}{\times} y) +_{K} ℤRHom (K) (A)) = P \underset{˙}{\times} (((\frac{N}{P}) \underset{˙}{\times} y) +_{K} ℤRHom (K) (A))$
102	101	eqcomd	$⊢ (φ \land y \in (V PrimRoots R)) \to P \underset{˙}{\times} (((\frac{N}{P}) \underset{˙}{\times} y) +_{K} ℤRHom (K) (A)) = (x \in {Base}_{K} ⟼ P \underset{˙}{\times} x) (((\frac{N}{P}) \underset{˙}{\times} y) +_{K} ℤRHom (K) (A))$
103	79	simpld	$⊢ φ \to (x \in {Base}_{K} ⟼ P \underset{˙}{\times} x) \in (K RingHom K)$
104		rhmghm	$⊢ (x \in {Base}_{K} ⟼ P \underset{˙}{\times} x) \in (K RingHom K) \to (x \in {Base}_{K} ⟼ P \underset{˙}{\times} x) \in (K GrpHom K)$
105	103 104	syl	$⊢ φ \to (x \in {Base}_{K} ⟼ P \underset{˙}{\times} x) \in (K GrpHom K)$
106	105	adantr	$⊢ (φ \land y \in (V PrimRoots R)) \to (x \in {Base}_{K} ⟼ P \underset{˙}{\times} x) \in (K GrpHom K)$
107	25 64 64	ghmlin	$⊢ ((x \in {Base}_{K} ⟼ P \underset{˙}{\times} x) \in (K GrpHom K) \land (\frac{N}{P}) \underset{˙}{\times} y \in {Base}_{K} \land ℤRHom (K) (A) \in {Base}_{K}) \to (x \in {Base}_{K} ⟼ P \underset{˙}{\times} x) (((\frac{N}{P}) \underset{˙}{\times} y) +_{K} ℤRHom (K) (A)) = (x \in {Base}_{K} ⟼ P \underset{˙}{\times} x) ((\frac{N}{P}) \underset{˙}{\times} y) +_{K} (x \in {Base}_{K} ⟼ P \underset{˙}{\times} x) (ℤRHom (K) (A))$
108	106 52 62 107	syl3anc	$⊢ (φ \land y \in (V PrimRoots R)) \to (x \in {Base}_{K} ⟼ P \underset{˙}{\times} x) (((\frac{N}{P}) \underset{˙}{\times} y) +_{K} ℤRHom (K) (A)) = (x \in {Base}_{K} ⟼ P \underset{˙}{\times} x) ((\frac{N}{P}) \underset{˙}{\times} y) +_{K} (x \in {Base}_{K} ⟼ P \underset{˙}{\times} x) (ℤRHom (K) (A))$
109		id	$⊢ x = (\frac{N}{P}) \underset{˙}{\times} y \to x = (\frac{N}{P}) \underset{˙}{\times} y$
110	109	adantl	$⊢ ((φ \land y \in (V PrimRoots R)) \land x = (\frac{N}{P}) \underset{˙}{\times} y) \to x = (\frac{N}{P}) \underset{˙}{\times} y$
111	110	oveq2d	$⊢ ((φ \land y \in (V PrimRoots R)) \land x = (\frac{N}{P}) \underset{˙}{\times} y) \to P \underset{˙}{\times} x = P \underset{˙}{\times} ((\frac{N}{P}) \underset{˙}{\times} y)$
112	92 94 97 99 52	mulgnn0cld	$⊢ (φ \land y \in (V PrimRoots R)) \to P \underset{˙}{\times} ((\frac{N}{P}) \underset{˙}{\times} y) \in {Base}_{K}$
113	87 111 52 112	fvmptd	$⊢ (φ \land y \in (V PrimRoots R)) \to (x \in {Base}_{K} ⟼ P \underset{˙}{\times} x) ((\frac{N}{P}) \underset{˙}{\times} y) = P \underset{˙}{\times} ((\frac{N}{P}) \underset{˙}{\times} y)$
114		id	$⊢ x = ℤRHom (K) (A) \to x = ℤRHom (K) (A)$
115	114	oveq2d	$⊢ x = ℤRHom (K) (A) \to P \underset{˙}{\times} x = P \underset{˙}{\times} ℤRHom (K) (A)$
116	115	adantl	$⊢ ((φ \land y \in (V PrimRoots R)) \land x = ℤRHom (K) (A)) \to P \underset{˙}{\times} x = P \underset{˙}{\times} ℤRHom (K) (A)$
117		eqid	$⊢ ℤRHom (K) (A) = ℤRHom (K) (A)$
118	10 25 94 117 14 19 26	fermltlchr	$⊢ φ \to P \underset{˙}{\times} ℤRHom (K) (A) = ℤRHom (K) (A)$
119	118	eqcomd	$⊢ φ \to ℤRHom (K) (A) = P \underset{˙}{\times} ℤRHom (K) (A)$
120	119	adantr	$⊢ (φ \land y \in (V PrimRoots R)) \to ℤRHom (K) (A) = P \underset{˙}{\times} ℤRHom (K) (A)$
121	120 62	eqeltrrd	$⊢ (φ \land y \in (V PrimRoots R)) \to P \underset{˙}{\times} ℤRHom (K) (A) \in {Base}_{K}$
122	87 116 62 121	fvmptd	$⊢ (φ \land y \in (V PrimRoots R)) \to (x \in {Base}_{K} ⟼ P \underset{˙}{\times} x) (ℤRHom (K) (A)) = P \underset{˙}{\times} ℤRHom (K) (A)$
123	113 122	oveq12d	$⊢ (φ \land y \in (V PrimRoots R)) \to (x \in {Base}_{K} ⟼ P \underset{˙}{\times} x) ((\frac{N}{P}) \underset{˙}{\times} y) +_{K} (x \in {Base}_{K} ⟼ P \underset{˙}{\times} x) (ℤRHom (K) (A)) = (P \underset{˙}{\times} ((\frac{N}{P}) \underset{˙}{\times} y)) +_{K} (P \underset{˙}{\times} ℤRHom (K) (A))$
124	102 108 123	3eqtrd	$⊢ (φ \land y \in (V PrimRoots R)) \to P \underset{˙}{\times} (((\frac{N}{P}) \underset{˙}{\times} y) +_{K} ℤRHom (K) (A)) = (P \underset{˙}{\times} ((\frac{N}{P}) \underset{˙}{\times} y)) +_{K} (P \underset{˙}{\times} ℤRHom (K) (A))$
125	34	nncnd	$⊢ φ \to N \in ℂ$
126	125	adantr	$⊢ (φ \land y \in (V PrimRoots R)) \to N \in ℂ$
127	36	nncnd	$⊢ φ \to P \in ℂ$
128	127	adantr	$⊢ (φ \land y \in (V PrimRoots R)) \to P \in ℂ$
129	36	nnne0d	$⊢ φ \to P \neq 0$
130	129	adantr	$⊢ (φ \land y \in (V PrimRoots R)) \to P \neq 0$
131	126 128 130	divcan2d	$⊢ (φ \land y \in (V PrimRoots R)) \to P (\frac{N}{P}) = N$
132	131	oveq1d	$⊢ (φ \land y \in (V PrimRoots R)) \to P (\frac{N}{P}) \underset{˙}{\times} (y +_{K} ℤRHom (K) (A)) = N \underset{˙}{\times} (y +_{K} ℤRHom (K) (A))$
133	68	oveq2d	$⊢ (φ \land y \in (V PrimRoots R)) \to N \underset{˙}{\times} O (F) (y) = N \underset{˙}{\times} O (X \underset{˙}{+} C (ℤRHom (K) (A))) (y)$
134	75	oveq2d	$⊢ (φ \land y \in (V PrimRoots R)) \to N \underset{˙}{\times} O (X \underset{˙}{+} C (ℤRHom (K) (A))) (y) = N \underset{˙}{\times} (y +_{K} ℤRHom (K) (A))$
135	133 134	eqtrd	$⊢ (φ \land y \in (V PrimRoots R)) \to N \underset{˙}{\times} O (F) (y) = N \underset{˙}{\times} (y +_{K} ℤRHom (K) (A))$
136	135	eqcomd	$⊢ (φ \land y \in (V PrimRoots R)) \to N \underset{˙}{\times} (y +_{K} ℤRHom (K) (A)) = N \underset{˙}{\times} O (F) (y)$
137		fveq2	$⊢ z = y \to O (F) (z) = O (F) (y)$
138	137	oveq2d	$⊢ z = y \to N \underset{˙}{\times} O (F) (z) = N \underset{˙}{\times} O (F) (y)$
139		oveq2	$⊢ z = y \to N \underset{˙}{\times} z = N \underset{˙}{\times} y$
140	139	fveq2d	$⊢ z = y \to O (F) (N \underset{˙}{\times} z) = O (F) (N \underset{˙}{\times} y)$
141	138 140	eqeq12d	$⊢ z = y \to (N \underset{˙}{\times} O (F) (z) = O (F) (N \underset{˙}{\times} z) \leftrightarrow N \underset{˙}{\times} O (F) (y) = O (F) (N \underset{˙}{\times} y))$
142	2	ply1crng	$⊢ K \in CRing \to S \in CRing$
143	26 142	syl	$⊢ φ \to S \in CRing$
144	143	crnggrpd	$⊢ φ \to S \in Grp$
145	4 2 3	vr1cl	$⊢ K \in Ring \to X \in B$
146	54 145	syl	$⊢ φ \to X \in B$
147	2 8 25 3	ply1sclcl	$⊢ (K \in Ring \land ℤRHom (K) (A) \in {Base}_{K}) \to C (ℤRHom (K) (A)) \in B$
148	54 61 147	syl2anc	$⊢ φ \to C (ℤRHom (K) (A)) \in B$
149	144 146 148	3jca	$⊢ φ \to (S \in Grp \land X \in B \land C (ℤRHom (K) (A)) \in B)$
150	3 12	grpcl	$⊢ (S \in Grp \land X \in B \land C (ℤRHom (K) (A)) \in B) \to X \underset{˙}{+} C (ℤRHom (K) (A)) \in B$
151	149 150	syl	$⊢ φ \to X \underset{˙}{+} C (ℤRHom (K) (A)) \in B$
152	18	a1i	$⊢ φ \to F = X \underset{˙}{+} C (ℤRHom (K) (A))$
153	152	eleq1d	$⊢ φ \to (F \in B \leftrightarrow X \underset{˙}{+} C (ℤRHom (K) (A)) \in B)$
154	151 153	mpbird	$⊢ φ \to F \in B$
155	1 154 34	aks6d1c1p1	$⊢ φ \to (N \underset{˙}{\sim} F \leftrightarrow \forall y \in (V PrimRoots R) N \underset{˙}{\times} O (F) (y) = O (F) (N \underset{˙}{\times} y))$
156	20 155	mpbid	$⊢ φ \to \forall y \in (V PrimRoots R) N \underset{˙}{\times} O (F) (y) = O (F) (N \underset{˙}{\times} y)$
157		fveq2	$⊢ y = z \to O (F) (y) = O (F) (z)$
158	157	oveq2d	$⊢ y = z \to N \underset{˙}{\times} O (F) (y) = N \underset{˙}{\times} O (F) (z)$
159		oveq2	$⊢ y = z \to N \underset{˙}{\times} y = N \underset{˙}{\times} z$
160	159	fveq2d	$⊢ y = z \to O (F) (N \underset{˙}{\times} y) = O (F) (N \underset{˙}{\times} z)$
161	158 160	eqeq12d	$⊢ y = z \to (N \underset{˙}{\times} O (F) (y) = O (F) (N \underset{˙}{\times} y) \leftrightarrow N \underset{˙}{\times} O (F) (z) = O (F) (N \underset{˙}{\times} z))$
162	161	cbvralvw	$⊢ \forall y \in (V PrimRoots R) N \underset{˙}{\times} O (F) (y) = O (F) (N \underset{˙}{\times} y) \leftrightarrow \forall z \in (V PrimRoots R) N \underset{˙}{\times} O (F) (z) = O (F) (N \underset{˙}{\times} z)$
163	156 162	sylib	$⊢ φ \to \forall z \in (V PrimRoots R) N \underset{˙}{\times} O (F) (z) = O (F) (N \underset{˙}{\times} z)$
164	163	adantr	$⊢ (φ \land y \in (V PrimRoots R)) \to \forall z \in (V PrimRoots R) N \underset{˙}{\times} O (F) (z) = O (F) (N \underset{˙}{\times} z)$
165		simpr	$⊢ (φ \land y \in (V PrimRoots R)) \to y \in (V PrimRoots R)$
166	141 164 165	rspcdva	$⊢ (φ \land y \in (V PrimRoots R)) \to N \underset{˙}{\times} O (F) (y) = O (F) (N \underset{˙}{\times} y)$
167	23	fveq1d	$⊢ (φ \land y \in (V PrimRoots R)) \to O (F) (N \underset{˙}{\times} y) = O (X \underset{˙}{+} C (ℤRHom (K) (A))) (N \underset{˙}{\times} y)$
168	34	nnnn0d	$⊢ φ \to N \in ℕ_{0}$
169	168	adantr	$⊢ (φ \land y \in (V PrimRoots R)) \to N \in ℕ_{0}$
170	28 7 32 169 46	mulgnn0cld	$⊢ (φ \land y \in (V PrimRoots R)) \to N \underset{˙}{\times} y \in {Base}_{V}$
171	170 51	eleqtrd	$⊢ (φ \land y \in (V PrimRoots R)) \to N \underset{˙}{\times} y \in {Base}_{K}$
172	146	adantr	$⊢ (φ \land y \in (V PrimRoots R)) \to X \in B$
173	11 4 25 2 3 27 171	evl1vard	$⊢ (φ \land y \in (V PrimRoots R)) \to (X \in B \land O (X) (N \underset{˙}{\times} y) = N \underset{˙}{\times} y)$
174	173	simprd	$⊢ (φ \land y \in (V PrimRoots R)) \to O (X) (N \underset{˙}{\times} y) = N \underset{˙}{\times} y$
175	172 174	jca	$⊢ (φ \land y \in (V PrimRoots R)) \to (X \in B \land O (X) (N \underset{˙}{\times} y) = N \underset{˙}{\times} y)$
176	148	adantr	$⊢ (φ \land y \in (V PrimRoots R)) \to C (ℤRHom (K) (A)) \in B$
177	11 2 25 8 3 27 62 171	evl1scad	$⊢ (φ \land y \in (V PrimRoots R)) \to (C (ℤRHom (K) (A)) \in B \land O (C (ℤRHom (K) (A))) (N \underset{˙}{\times} y) = ℤRHom (K) (A))$
178	177	simprd	$⊢ (φ \land y \in (V PrimRoots R)) \to O (C (ℤRHom (K) (A))) (N \underset{˙}{\times} y) = ℤRHom (K) (A)$
179	176 178	jca	$⊢ (φ \land y \in (V PrimRoots R)) \to (C (ℤRHom (K) (A)) \in B \land O (C (ℤRHom (K) (A))) (N \underset{˙}{\times} y) = ℤRHom (K) (A))$
180	11 2 25 3 27 171 175 179 12 64	evl1addd	$⊢ (φ \land y \in (V PrimRoots R)) \to (X \underset{˙}{+} C (ℤRHom (K) (A)) \in B \land O (X \underset{˙}{+} C (ℤRHom (K) (A))) (N \underset{˙}{\times} y) = (N \underset{˙}{\times} y) +_{K} ℤRHom (K) (A))$
181	180	simprd	$⊢ (φ \land y \in (V PrimRoots R)) \to O (X \underset{˙}{+} C (ℤRHom (K) (A))) (N \underset{˙}{\times} y) = (N \underset{˙}{\times} y) +_{K} ℤRHom (K) (A)$
182	167 181	eqtrd	$⊢ (φ \land y \in (V PrimRoots R)) \to O (F) (N \underset{˙}{\times} y) = (N \underset{˙}{\times} y) +_{K} ℤRHom (K) (A)$
183	166 182	eqtrd	$⊢ (φ \land y \in (V PrimRoots R)) \to N \underset{˙}{\times} O (F) (y) = (N \underset{˙}{\times} y) +_{K} ℤRHom (K) (A)$
184	136 183	eqtrd	$⊢ (φ \land y \in (V PrimRoots R)) \to N \underset{˙}{\times} (y +_{K} ℤRHom (K) (A)) = (N \underset{˙}{\times} y) +_{K} ℤRHom (K) (A)$
185	132 184	eqtrd	$⊢ (φ \land y \in (V PrimRoots R)) \to P (\frac{N}{P}) \underset{˙}{\times} (y +_{K} ℤRHom (K) (A)) = (N \underset{˙}{\times} y) +_{K} ℤRHom (K) (A)$
186	131	eqcomd	$⊢ (φ \land y \in (V PrimRoots R)) \to N = P (\frac{N}{P})$
187	186	oveq1d	$⊢ (φ \land y \in (V PrimRoots R)) \to N \underset{˙}{\times} y = P (\frac{N}{P}) \underset{˙}{\times} y$
188	187 120	oveq12d	$⊢ (φ \land y \in (V PrimRoots R)) \to (N \underset{˙}{\times} y) +_{K} ℤRHom (K) (A) = (P (\frac{N}{P}) \underset{˙}{\times} y) +_{K} (P \underset{˙}{\times} ℤRHom (K) (A))$
189	185 188	eqtr2d	$⊢ (φ \land y \in (V PrimRoots R)) \to (P (\frac{N}{P}) \underset{˙}{\times} y) +_{K} (P \underset{˙}{\times} ℤRHom (K) (A)) = P (\frac{N}{P}) \underset{˙}{\times} (y +_{K} ℤRHom (K) (A))$
190	71 92	eleqtrdi	$⊢ (φ \land y \in (V PrimRoots R)) \to y \in {Base}_{{mulGrp}_{K}}$
191	99 41 190	3jca	$⊢ (φ \land y \in (V PrimRoots R)) \to (P \in ℕ_{0} \land \frac{N}{P} \in ℕ_{0} \land y \in {Base}_{{mulGrp}_{K}})$
192		eqid	$⊢ {Base}_{{mulGrp}_{K}} = {Base}_{{mulGrp}_{K}}$
193	192 94	mulgnn0ass	$⊢ ({mulGrp}_{K} \in Mnd \land (P \in ℕ_{0} \land \frac{N}{P} \in ℕ_{0} \land y \in {Base}_{{mulGrp}_{K}})) \to P (\frac{N}{P}) \underset{˙}{\times} y = P \underset{˙}{\times} ((\frac{N}{P}) \underset{˙}{\times} y)$
194	97 191 193	syl2anc	$⊢ (φ \land y \in (V PrimRoots R)) \to P (\frac{N}{P}) \underset{˙}{\times} y = P \underset{˙}{\times} ((\frac{N}{P}) \underset{˙}{\times} y)$
195	194	oveq1d	$⊢ (φ \land y \in (V PrimRoots R)) \to (P (\frac{N}{P}) \underset{˙}{\times} y) +_{K} (P \underset{˙}{\times} ℤRHom (K) (A)) = (P \underset{˙}{\times} ((\frac{N}{P}) \underset{˙}{\times} y)) +_{K} (P \underset{˙}{\times} ℤRHom (K) (A))$
196	189 195	eqtr3d	$⊢ (φ \land y \in (V PrimRoots R)) \to P (\frac{N}{P}) \underset{˙}{\times} (y +_{K} ℤRHom (K) (A)) = (P \underset{˙}{\times} ((\frac{N}{P}) \underset{˙}{\times} y)) +_{K} (P \underset{˙}{\times} ℤRHom (K) (A))$
197	25 64 82 71 62	grpcld	$⊢ (φ \land y \in (V PrimRoots R)) \to y +_{K} ℤRHom (K) (A) \in {Base}_{K}$
198	197 92	eleqtrdi	$⊢ (φ \land y \in (V PrimRoots R)) \to y +_{K} ℤRHom (K) (A) \in {Base}_{{mulGrp}_{K}}$
199	99 41 198	3jca	$⊢ (φ \land y \in (V PrimRoots R)) \to (P \in ℕ_{0} \land \frac{N}{P} \in ℕ_{0} \land y +_{K} ℤRHom (K) (A) \in {Base}_{{mulGrp}_{K}})$
200	192 94	mulgnn0ass	$⊢ ({mulGrp}_{K} \in Mnd \land (P \in ℕ_{0} \land \frac{N}{P} \in ℕ_{0} \land y +_{K} ℤRHom (K) (A) \in {Base}_{{mulGrp}_{K}})) \to P (\frac{N}{P}) \underset{˙}{\times} (y +_{K} ℤRHom (K) (A)) = P \underset{˙}{\times} ((\frac{N}{P}) \underset{˙}{\times} (y +_{K} ℤRHom (K) (A)))$
201	97 199 200	syl2anc	$⊢ (φ \land y \in (V PrimRoots R)) \to P (\frac{N}{P}) \underset{˙}{\times} (y +_{K} ℤRHom (K) (A)) = P \underset{˙}{\times} ((\frac{N}{P}) \underset{˙}{\times} (y +_{K} ℤRHom (K) (A)))$
202	196 201	eqtr3d	$⊢ (φ \land y \in (V PrimRoots R)) \to (P \underset{˙}{\times} ((\frac{N}{P}) \underset{˙}{\times} y)) +_{K} (P \underset{˙}{\times} ℤRHom (K) (A)) = P \underset{˙}{\times} ((\frac{N}{P}) \underset{˙}{\times} (y +_{K} ℤRHom (K) (A)))$
203	124 202	eqtrd	$⊢ (φ \land y \in (V PrimRoots R)) \to P \underset{˙}{\times} (((\frac{N}{P}) \underset{˙}{\times} y) +_{K} ℤRHom (K) (A)) = P \underset{˙}{\times} ((\frac{N}{P}) \underset{˙}{\times} (y +_{K} ℤRHom (K) (A)))$
204		id	$⊢ x = (\frac{N}{P}) \underset{˙}{\times} (y +_{K} ℤRHom (K) (A)) \to x = (\frac{N}{P}) \underset{˙}{\times} (y +_{K} ℤRHom (K) (A))$
205	204	oveq2d	$⊢ x = (\frac{N}{P}) \underset{˙}{\times} (y +_{K} ℤRHom (K) (A)) \to P \underset{˙}{\times} x = P \underset{˙}{\times} ((\frac{N}{P}) \underset{˙}{\times} (y +_{K} ℤRHom (K) (A)))$
206	205	adantl	$⊢ ((φ \land y \in (V PrimRoots R)) \land x = (\frac{N}{P}) \underset{˙}{\times} (y +_{K} ℤRHom (K) (A))) \to P \underset{˙}{\times} x = P \underset{˙}{\times} ((\frac{N}{P}) \underset{˙}{\times} (y +_{K} ℤRHom (K) (A)))$
207	92 94 97 41 197	mulgnn0cld	$⊢ (φ \land y \in (V PrimRoots R)) \to (\frac{N}{P}) \underset{˙}{\times} (y +_{K} ℤRHom (K) (A)) \in {Base}_{K}$
208	203 100	eqeltrrd	$⊢ (φ \land y \in (V PrimRoots R)) \to P \underset{˙}{\times} ((\frac{N}{P}) \underset{˙}{\times} (y +_{K} ℤRHom (K) (A))) \in {Base}_{K}$
209	87 206 207 208	fvmptd	$⊢ (φ \land y \in (V PrimRoots R)) \to (x \in {Base}_{K} ⟼ P \underset{˙}{\times} x) ((\frac{N}{P}) \underset{˙}{\times} (y +_{K} ℤRHom (K) (A))) = P \underset{˙}{\times} ((\frac{N}{P}) \underset{˙}{\times} (y +_{K} ℤRHom (K) (A)))$
210	209	eqcomd	$⊢ (φ \land y \in (V PrimRoots R)) \to P \underset{˙}{\times} ((\frac{N}{P}) \underset{˙}{\times} (y +_{K} ℤRHom (K) (A))) = (x \in {Base}_{K} ⟼ P \underset{˙}{\times} x) ((\frac{N}{P}) \underset{˙}{\times} (y +_{K} ℤRHom (K) (A)))$
211	101 203 210	3eqtrd	$⊢ (φ \land y \in (V PrimRoots R)) \to (x \in {Base}_{K} ⟼ P \underset{˙}{\times} x) (((\frac{N}{P}) \underset{˙}{\times} y) +_{K} ℤRHom (K) (A)) = (x \in {Base}_{K} ⟼ P \underset{˙}{\times} x) ((\frac{N}{P}) \underset{˙}{\times} (y +_{K} ℤRHom (K) (A)))$
212	211	fveq2d	$⊢ (φ \land y \in (V PrimRoots R)) \to {(x \in {Base}_{K} ⟼ P \underset{˙}{\times} x)}^{-1} ((x \in {Base}_{K} ⟼ P \underset{˙}{\times} x) (((\frac{N}{P}) \underset{˙}{\times} y) +_{K} ℤRHom (K) (A))) = {(x \in {Base}_{K} ⟼ P \underset{˙}{\times} x)}^{-1} ((x \in {Base}_{K} ⟼ P \underset{˙}{\times} x) ((\frac{N}{P}) \underset{˙}{\times} (y +_{K} ℤRHom (K) (A))))$
213		f1ocnvfv1	$⊢ ((x \in {Base}_{K} ⟼ P \underset{˙}{\times} x) : {Base}_{K} \underset{1-1 onto}{⟶} {Base}_{K} \land (\frac{N}{P}) \underset{˙}{\times} (y +_{K} ℤRHom (K) (A)) \in {Base}_{K}) \to {(x \in {Base}_{K} ⟼ P \underset{˙}{\times} x)}^{-1} ((x \in {Base}_{K} ⟼ P \underset{˙}{\times} x) ((\frac{N}{P}) \underset{˙}{\times} (y +_{K} ℤRHom (K) (A)))) = (\frac{N}{P}) \underset{˙}{\times} (y +_{K} ℤRHom (K) (A))$
214	81 207 213	syl2anc	$⊢ (φ \land y \in (V PrimRoots R)) \to {(x \in {Base}_{K} ⟼ P \underset{˙}{\times} x)}^{-1} ((x \in {Base}_{K} ⟼ P \underset{˙}{\times} x) ((\frac{N}{P}) \underset{˙}{\times} (y +_{K} ℤRHom (K) (A)))) = (\frac{N}{P}) \underset{˙}{\times} (y +_{K} ℤRHom (K) (A))$
215	86 212 214	3eqtrd	$⊢ (φ \land y \in (V PrimRoots R)) \to ((\frac{N}{P}) \underset{˙}{\times} y) +_{K} ℤRHom (K) (A) = (\frac{N}{P}) \underset{˙}{\times} (y +_{K} ℤRHom (K) (A))$
216	215	eqcomd	$⊢ (φ \land y \in (V PrimRoots R)) \to (\frac{N}{P}) \underset{˙}{\times} (y +_{K} ℤRHom (K) (A)) = ((\frac{N}{P}) \underset{˙}{\times} y) +_{K} ℤRHom (K) (A)$
217	77 216	eqtr2d	$⊢ (φ \land y \in (V PrimRoots R)) \to ((\frac{N}{P}) \underset{˙}{\times} y) +_{K} ℤRHom (K) (A) = (\frac{N}{P}) \underset{˙}{\times} O (F) (y)$
218	67 217	eqtrd	$⊢ (φ \land y \in (V PrimRoots R)) \to O (F) ((\frac{N}{P}) \underset{˙}{\times} y) = (\frac{N}{P}) \underset{˙}{\times} O (F) (y)$
219	218	eqcomd	$⊢ (φ \land y \in (V PrimRoots R)) \to (\frac{N}{P}) \underset{˙}{\times} O (F) (y) = O (F) ((\frac{N}{P}) \underset{˙}{\times} y)$
220	219	ralrimiva	$⊢ φ \to \forall y \in (V PrimRoots R) (\frac{N}{P}) \underset{˙}{\times} O (F) (y) = O (F) ((\frac{N}{P}) \underset{˙}{\times} y)$
221	1 154 39	aks6d1c1p1	$⊢ φ \to ((\frac{N}{P}) \underset{˙}{\sim} F \leftrightarrow \forall y \in (V PrimRoots R) (\frac{N}{P}) \underset{˙}{\times} O (F) (y) = O (F) ((\frac{N}{P}) \underset{˙}{\times} y))$
222	220 221	mpbird	$⊢ φ \to (\frac{N}{P}) \underset{˙}{\sim} F$

Metamath Proof Explorer

Theorem aks6d1c1p3

Proof