aks6d1c1p4

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

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

Proof

Step	Hyp	Ref	Expression
1		aks6d1c1p4.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		aks6d1c1p4.2	$⊢ S = {Poly}_{1} (K)$
3		aks6d1c1p4.3	$⊢ B = {Base}_{S}$
4		aks6d1c1p4.4	$⊢ X = {var}_{1} (K)$
5		aks6d1c1p4.5	$⊢ W = {mulGrp}_{S}$
6		aks6d1c1p4.6	$⊢ V = {mulGrp}_{K}$
7		aks6d1c1p4.7	$⊢ \underset{˙}{\times} = \cdot_{V}$
8		aks6d1c1p4.8	$⊢ C = algSc (S)$
9		aks6d1c1p4.9	$⊢ D = \cdot_{W}$
10		aks6d1c1p4.10	$⊢ P = chr (K)$
11		aks6d1c1p4.11	$⊢ O = {eval}_{1} (K)$
12		aks6d1c1p4.12	$⊢ \underset{˙}{+} = +_{S}$
13		aks6d1c1p4.13	$⊢ φ \to K \in Field$
14		aks6d1c1p4.14	$⊢ φ \to P \in ℙ$
15		aks6d1c1p4.15	$⊢ φ \to R \in ℕ$
16		aks6d1c1p4.16	$⊢ φ \to N \gcd R = 1$
17		aks6d1c1p4.17	$⊢ φ \to P ∥ N$
18		aks6d1c1p4.18	$⊢ φ \to E \underset{˙}{\sim} F$
19		aks6d1c1p4.19	$⊢ φ \to E \underset{˙}{\sim} G$
20		eqid	$⊢ {Base}_{K} = {Base}_{K}$
21	13	fldcrngd	$⊢ φ \to K \in CRing$
22	21	adantr	$⊢ (φ \land y \in (V PrimRoots R)) \to K \in CRing$
23	6 20	mgpbas	$⊢ {Base}_{K} = {Base}_{V}$
24	6	crngmgp	$⊢ K \in CRing \to V \in CMnd$
25	21 24	syl	$⊢ φ \to V \in CMnd$
26	25	cmnmndd	$⊢ φ \to V \in Mnd$
27	26	adantr	$⊢ (φ \land y \in (V PrimRoots R)) \to V \in Mnd$
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	15	nnnn0d	$⊢ φ \to R \in ℕ_{0}$
33		eqid	$⊢ \cdot_{V} = \cdot_{V}$
34	25 32 33	isprimroot	$⊢ φ \to (y \in (V PrimRoots R) \leftrightarrow (y \in {Base}_{V} \land R \cdot_{V} y = 0_{V} \land \forall l \in ℕ_{0} (l \cdot_{V} y = 0_{V} \to R ∥ l)))$
35	34	biimpd	$⊢ φ \to (y \in (V PrimRoots R) \to (y \in {Base}_{V} \land R \cdot_{V} y = 0_{V} \land \forall l \in ℕ_{0} (l \cdot_{V} y = 0_{V} \to R ∥ l)))$
36	35	imp	$⊢ (φ \land y \in (V PrimRoots R)) \to (y \in {Base}_{V} \land R \cdot_{V} y = 0_{V} \land \forall l \in ℕ_{0} (l \cdot_{V} y = 0_{V} \to R ∥ l))$
37	36	simp1d	$⊢ (φ \land y \in (V PrimRoots R)) \to y \in {Base}_{V}$
38	37 23	eleqtrrdi	$⊢ (φ \land y \in (V PrimRoots R)) \to y \in {Base}_{K}$
39	23 7 27 31 38	mulgnn0cld	$⊢ (φ \land y \in (V PrimRoots R)) \to E \underset{˙}{\times} y \in {Base}_{K}$
40	28	simprd	$⊢ φ \to F \in B$
41	40	adantr	$⊢ (φ \land y \in (V PrimRoots R)) \to F \in B$
42		eqidd	$⊢ (φ \land y \in (V PrimRoots R)) \to O (F) (E \underset{˙}{\times} y) = O (F) (E \underset{˙}{\times} y)$
43	41 42	jca	$⊢ (φ \land y \in (V PrimRoots R)) \to (F \in B \land O (F) (E \underset{˙}{\times} y) = O (F) (E \underset{˙}{\times} y))$
44	1 19	aks6d1c1p1rcl	$⊢ φ \to (E \in ℕ \land G \in B)$
45	44	simprd	$⊢ φ \to G \in B$
46	45	adantr	$⊢ (φ \land y \in (V PrimRoots R)) \to G \in B$
47		eqidd	$⊢ (φ \land y \in (V PrimRoots R)) \to O (G) (E \underset{˙}{\times} y) = O (G) (E \underset{˙}{\times} y)$
48	46 47	jca	$⊢ (φ \land y \in (V PrimRoots R)) \to (G \in B \land O (G) (E \underset{˙}{\times} y) = O (G) (E \underset{˙}{\times} y))$
49		eqid	$⊢ \cdot_{S} = \cdot_{S}$
50	5 49	mgpplusg	$⊢ \cdot_{S} = +_{W}$
51	50	eqcomi	$⊢ +_{W} = \cdot_{S}$
52		eqid	$⊢ \cdot_{K} = \cdot_{K}$
53	11 2 20 3 22 39 43 48 51 52	evl1muld	$⊢ (φ \land y \in (V PrimRoots R)) \to (F +_{W} G \in B \land O (F +_{W} G) (E \underset{˙}{\times} y) = O (F) (E \underset{˙}{\times} y) \cdot_{K} O (G) (E \underset{˙}{\times} y))$
54	53	simprd	$⊢ (φ \land y \in (V PrimRoots R)) \to O (F +_{W} G) (E \underset{˙}{\times} y) = O (F) (E \underset{˙}{\times} y) \cdot_{K} O (G) (E \underset{˙}{\times} y)$
55	25	adantr	$⊢ (φ \land y \in (V PrimRoots R)) \to V \in CMnd$
56	11 2 20 3 22 38 41	fveval1fvcl	$⊢ (φ \land y \in (V PrimRoots R)) \to O (F) (y) \in {Base}_{K}$
57	6	eqcomi	$⊢ {mulGrp}_{K} = V$
58	57	fveq2i	$⊢ {Base}_{{mulGrp}_{K}} = {Base}_{V}$
59	23 58	eqtr4i	$⊢ {Base}_{K} = {Base}_{{mulGrp}_{K}}$
60	59	a1i	$⊢ (φ \land y \in (V PrimRoots R)) \to {Base}_{K} = {Base}_{{mulGrp}_{K}}$
61	60	eleq2d	$⊢ (φ \land y \in (V PrimRoots R)) \to (O (F) (y) \in {Base}_{K} \leftrightarrow O (F) (y) \in {Base}_{{mulGrp}_{K}})$
62	56 61	mpbid	$⊢ (φ \land y \in (V PrimRoots R)) \to O (F) (y) \in {Base}_{{mulGrp}_{K}}$
63	11 2 20 3 22 38 46	fveval1fvcl	$⊢ (φ \land y \in (V PrimRoots R)) \to O (G) (y) \in {Base}_{K}$
64	60	eleq2d	$⊢ (φ \land y \in (V PrimRoots R)) \to (O (G) (y) \in {Base}_{K} \leftrightarrow O (G) (y) \in {Base}_{{mulGrp}_{K}})$
65	63 64	mpbid	$⊢ (φ \land y \in (V PrimRoots R)) \to O (G) (y) \in {Base}_{{mulGrp}_{K}}$
66	31 62 65	3jca	$⊢ (φ \land y \in (V PrimRoots R)) \to (E \in ℕ_{0} \land O (F) (y) \in {Base}_{{mulGrp}_{K}} \land O (G) (y) \in {Base}_{{mulGrp}_{K}})$
67	57	fveq2i	$⊢ +_{{mulGrp}_{K}} = +_{V}$
68	58 7 67	mulgnn0di	$⊢ (V \in CMnd \land (E \in ℕ_{0} \land O (F) (y) \in {Base}_{{mulGrp}_{K}} \land O (G) (y) \in {Base}_{{mulGrp}_{K}})) \to E \underset{˙}{\times} (O (F) (y) +_{{mulGrp}_{K}} O (G) (y)) = (E \underset{˙}{\times} O (F) (y)) +_{{mulGrp}_{K}} (E \underset{˙}{\times} O (G) (y))$
69	55 66 68	syl2anc	$⊢ (φ \land y \in (V PrimRoots R)) \to E \underset{˙}{\times} (O (F) (y) +_{{mulGrp}_{K}} O (G) (y)) = (E \underset{˙}{\times} O (F) (y)) +_{{mulGrp}_{K}} (E \underset{˙}{\times} O (G) (y))$
70	6 52	mgpplusg	$⊢ \cdot_{K} = +_{V}$
71	6	fveq2i	$⊢ +_{V} = +_{{mulGrp}_{K}}$
72	70 71	eqtri	$⊢ \cdot_{K} = +_{{mulGrp}_{K}}$
73	72	a1i	$⊢ (φ \land y \in (V PrimRoots R)) \to \cdot_{K} = +_{{mulGrp}_{K}}$
74	73	eqcomd	$⊢ (φ \land y \in (V PrimRoots R)) \to +_{{mulGrp}_{K}} = \cdot_{K}$
75		fveq2	$⊢ z = y \to O (F) (z) = O (F) (y)$
76	75	oveq2d	$⊢ z = y \to E \underset{˙}{\times} O (F) (z) = E \underset{˙}{\times} O (F) (y)$
77		oveq2	$⊢ z = y \to E \underset{˙}{\times} z = E \underset{˙}{\times} y$
78	77	fveq2d	$⊢ z = y \to O (F) (E \underset{˙}{\times} z) = O (F) (E \underset{˙}{\times} y)$
79	76 78	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))$
80	1 40 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))$
81	18 80	mpbid	$⊢ φ \to \forall y \in (V PrimRoots R) E \underset{˙}{\times} O (F) (y) = O (F) (E \underset{˙}{\times} y)$
82		fveq2	$⊢ y = z \to O (F) (y) = O (F) (z)$
83	82	oveq2d	$⊢ y = z \to E \underset{˙}{\times} O (F) (y) = E \underset{˙}{\times} O (F) (z)$
84		oveq2	$⊢ y = z \to E \underset{˙}{\times} y = E \underset{˙}{\times} z$
85	84	fveq2d	$⊢ y = z \to O (F) (E \underset{˙}{\times} y) = O (F) (E \underset{˙}{\times} z)$
86	83 85	eqeq12d	$⊢ y = z \to (E \underset{˙}{\times} O (F) (y) = O (F) (E \underset{˙}{\times} y) \leftrightarrow E \underset{˙}{\times} O (F) (z) = O (F) (E \underset{˙}{\times} z))$
87	86	cbvralvw	$⊢ \forall y \in (V PrimRoots R) E \underset{˙}{\times} O (F) (y) = O (F) (E \underset{˙}{\times} y) \leftrightarrow \forall z \in (V PrimRoots R) E \underset{˙}{\times} O (F) (z) = O (F) (E \underset{˙}{\times} z)$
88	81 87	sylib	$⊢ φ \to \forall z \in (V PrimRoots R) E \underset{˙}{\times} O (F) (z) = O (F) (E \underset{˙}{\times} z)$
89	88	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)$
90		simpr	$⊢ (φ \land y \in (V PrimRoots R)) \to y \in (V PrimRoots R)$
91	79 89 90	rspcdva	$⊢ (φ \land y \in (V PrimRoots R)) \to E \underset{˙}{\times} O (F) (y) = O (F) (E \underset{˙}{\times} y)$
92		fveq2	$⊢ z = y \to O (G) (z) = O (G) (y)$
93	92	oveq2d	$⊢ z = y \to E \underset{˙}{\times} O (G) (z) = E \underset{˙}{\times} O (G) (y)$
94	77	fveq2d	$⊢ z = y \to O (G) (E \underset{˙}{\times} z) = O (G) (E \underset{˙}{\times} y)$
95	93 94	eqeq12d	$⊢ z = y \to (E \underset{˙}{\times} O (G) (z) = O (G) (E \underset{˙}{\times} z) \leftrightarrow E \underset{˙}{\times} O (G) (y) = O (G) (E \underset{˙}{\times} y))$
96	1 45 29	aks6d1c1p1	$⊢ φ \to (E \underset{˙}{\sim} G \leftrightarrow \forall y \in (V PrimRoots R) E \underset{˙}{\times} O (G) (y) = O (G) (E \underset{˙}{\times} y))$
97	19 96	mpbid	$⊢ φ \to \forall y \in (V PrimRoots R) E \underset{˙}{\times} O (G) (y) = O (G) (E \underset{˙}{\times} y)$
98		fveq2	$⊢ y = z \to O (G) (y) = O (G) (z)$
99	98	oveq2d	$⊢ y = z \to E \underset{˙}{\times} O (G) (y) = E \underset{˙}{\times} O (G) (z)$
100	84	fveq2d	$⊢ y = z \to O (G) (E \underset{˙}{\times} y) = O (G) (E \underset{˙}{\times} z)$
101	99 100	eqeq12d	$⊢ y = z \to (E \underset{˙}{\times} O (G) (y) = O (G) (E \underset{˙}{\times} y) \leftrightarrow E \underset{˙}{\times} O (G) (z) = O (G) (E \underset{˙}{\times} z))$
102	101	cbvralvw	$⊢ \forall y \in (V PrimRoots R) E \underset{˙}{\times} O (G) (y) = O (G) (E \underset{˙}{\times} y) \leftrightarrow \forall z \in (V PrimRoots R) E \underset{˙}{\times} O (G) (z) = O (G) (E \underset{˙}{\times} z)$
103	97 102	sylib	$⊢ φ \to \forall z \in (V PrimRoots R) E \underset{˙}{\times} O (G) (z) = O (G) (E \underset{˙}{\times} z)$
104	103	adantr	$⊢ (φ \land y \in (V PrimRoots R)) \to \forall z \in (V PrimRoots R) E \underset{˙}{\times} O (G) (z) = O (G) (E \underset{˙}{\times} z)$
105	95 104 90	rspcdva	$⊢ (φ \land y \in (V PrimRoots R)) \to E \underset{˙}{\times} O (G) (y) = O (G) (E \underset{˙}{\times} y)$
106	74 91 105	oveq123d	$⊢ (φ \land y \in (V PrimRoots R)) \to (E \underset{˙}{\times} O (F) (y)) +_{{mulGrp}_{K}} (E \underset{˙}{\times} O (G) (y)) = O (F) (E \underset{˙}{\times} y) \cdot_{K} O (G) (E \underset{˙}{\times} y)$
107	69 106	eqtr2d	$⊢ (φ \land y \in (V PrimRoots R)) \to O (F) (E \underset{˙}{\times} y) \cdot_{K} O (G) (E \underset{˙}{\times} y) = E \underset{˙}{\times} (O (F) (y) +_{{mulGrp}_{K}} O (G) (y))$
108	72	eqcomi	$⊢ +_{{mulGrp}_{K}} = \cdot_{K}$
109	108	a1i	$⊢ (φ \land y \in (V PrimRoots R)) \to +_{{mulGrp}_{K}} = \cdot_{K}$
110	109	oveqd	$⊢ (φ \land y \in (V PrimRoots R)) \to O (F) (y) +_{{mulGrp}_{K}} O (G) (y) = O (F) (y) \cdot_{K} O (G) (y)$
111	110	oveq2d	$⊢ (φ \land y \in (V PrimRoots R)) \to E \underset{˙}{\times} (O (F) (y) +_{{mulGrp}_{K}} O (G) (y)) = E \underset{˙}{\times} (O (F) (y) \cdot_{K} O (G) (y))$
112	107 111	eqtrd	$⊢ (φ \land y \in (V PrimRoots R)) \to O (F) (E \underset{˙}{\times} y) \cdot_{K} O (G) (E \underset{˙}{\times} y) = E \underset{˙}{\times} (O (F) (y) \cdot_{K} O (G) (y))$
113		eqidd	$⊢ (φ \land y \in (V PrimRoots R)) \to O (F) (y) = O (F) (y)$
114	41 113	jca	$⊢ (φ \land y \in (V PrimRoots R)) \to (F \in B \land O (F) (y) = O (F) (y))$
115		eqidd	$⊢ (φ \land y \in (V PrimRoots R)) \to O (G) (y) = O (G) (y)$
116	46 115	jca	$⊢ (φ \land y \in (V PrimRoots R)) \to (G \in B \land O (G) (y) = O (G) (y))$
117	11 2 20 3 22 38 114 116 51 52	evl1muld	$⊢ (φ \land y \in (V PrimRoots R)) \to (F +_{W} G \in B \land O (F +_{W} G) (y) = O (F) (y) \cdot_{K} O (G) (y))$
118	117	simprd	$⊢ (φ \land y \in (V PrimRoots R)) \to O (F +_{W} G) (y) = O (F) (y) \cdot_{K} O (G) (y)$
119	118	eqcomd	$⊢ (φ \land y \in (V PrimRoots R)) \to O (F) (y) \cdot_{K} O (G) (y) = O (F +_{W} G) (y)$
120	119	oveq2d	$⊢ (φ \land y \in (V PrimRoots R)) \to E \underset{˙}{\times} (O (F) (y) \cdot_{K} O (G) (y)) = E \underset{˙}{\times} O (F +_{W} G) (y)$
121	112 120	eqtrd	$⊢ (φ \land y \in (V PrimRoots R)) \to O (F) (E \underset{˙}{\times} y) \cdot_{K} O (G) (E \underset{˙}{\times} y) = E \underset{˙}{\times} O (F +_{W} G) (y)$
122	54 121	eqtrd	$⊢ (φ \land y \in (V PrimRoots R)) \to O (F +_{W} G) (E \underset{˙}{\times} y) = E \underset{˙}{\times} O (F +_{W} G) (y)$
123	122	eqcomd	$⊢ (φ \land y \in (V PrimRoots R)) \to E \underset{˙}{\times} O (F +_{W} G) (y) = O (F +_{W} G) (E \underset{˙}{\times} y)$
124	123	ralrimiva	$⊢ φ \to \forall y \in (V PrimRoots R) E \underset{˙}{\times} O (F +_{W} G) (y) = O (F +_{W} G) (E \underset{˙}{\times} y)$
125	2	ply1crng	$⊢ K \in CRing \to S \in CRing$
126	21 125	syl	$⊢ φ \to S \in CRing$
127	126	crngringd	$⊢ φ \to S \in Ring$
128	3 51 127 40 45	ringcld	$⊢ φ \to F +_{W} G \in B$
129	1 128 29	aks6d1c1p1	$⊢ φ \to (E \underset{˙}{\sim} (F +_{W} G) \leftrightarrow \forall y \in (V PrimRoots R) E \underset{˙}{\times} O (F +_{W} G) (y) = O (F +_{W} G) (E \underset{˙}{\times} y))$
130	124 129	mpbird	$⊢ φ \to E \underset{˙}{\sim} (F +_{W} G)$

Metamath Proof Explorer

Theorem aks6d1c1p4

Proof