Theorem selvadd 42302

Description: The "variable selection" function is additive. (Contributed by SN, 7-Feb-2025.)

Hypotheses

Ref	Expression
selvadd.p	⊢ 𝑃 = (𝐼 mPoly 𝑅)
selvadd.b	⊢ 𝐵 = (Base‘𝑃)
selvadd.1	⊢ + = (+g‘𝑃)
selvadd.u	⊢ 𝑈 = ((𝐼 ∖ 𝐽) mPoly 𝑅)
selvadd.t	⊢ 𝑇 = (𝐽 mPoly 𝑈)
selvadd.2	⊢ ✚ = (+g‘𝑇)
selvadd.i	⊢ (𝜑 → 𝐼 ∈ 𝑉)
selvadd.r	⊢ (𝜑 → 𝑅 ∈ CRing)
selvadd.j	⊢ (𝜑 → 𝐽 ⊆ 𝐼)
selvadd.f	⊢ (𝜑 → 𝐹 ∈ 𝐵)
selvadd.g	⊢ (𝜑 → 𝐺 ∈ 𝐵)

Assertion

Ref	Expression
selvadd	⊢ (𝜑 → (((𝐼 selectVars 𝑅)‘𝐽)‘(𝐹 + 𝐺)) = ((((𝐼 selectVars 𝑅)‘𝐽)‘𝐹) ✚ (((𝐼 selectVars 𝑅)‘𝐽)‘𝐺)))

Proof of Theorem selvadd

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		selvadd.p	. . . . . 6 ⊢ 𝑃 = (𝐼 mPoly 𝑅)
2		eqid 2729	. . . . . 6 ⊢ (𝐼 mPoly 𝑇) = (𝐼 mPoly 𝑇)
3		selvadd.b	. . . . . 6 ⊢ 𝐵 = (Base‘𝑃)
4		eqid 2729	. . . . . 6 ⊢ (Base‘(𝐼 mPoly 𝑇)) = (Base‘(𝐼 mPoly 𝑇))
5		selvadd.1	. . . . . 6 ⊢ + = (+g‘𝑃)
6		eqid 2729	. . . . . 6 ⊢ (+g‘(𝐼 mPoly 𝑇)) = (+g‘(𝐼 mPoly 𝑇))
7		selvadd.u	. . . . . . . 8 ⊢ 𝑈 = ((𝐼 ∖ 𝐽) mPoly 𝑅)
8		selvadd.t	. . . . . . . 8 ⊢ 𝑇 = (𝐽 mPoly 𝑈)
9		eqid 2729	. . . . . . . 8 ⊢ (algSc‘𝑇) = (algSc‘𝑇)
10		eqid 2729	. . . . . . . 8 ⊢ ((algSc‘𝑇) ∘ (algSc‘𝑈)) = ((algSc‘𝑇) ∘ (algSc‘𝑈))
11		selvadd.i	. . . . . . . . 9 ⊢ (𝜑 → 𝐼 ∈ 𝑉)
12	11	difexd 5337	. . . . . . . 8 ⊢ (𝜑 → (𝐼 ∖ 𝐽) ∈ V)
13		selvadd.j	. . . . . . . . 9 ⊢ (𝜑 → 𝐽 ⊆ 𝐼)
14	11, 13	ssexd 5330	. . . . . . . 8 ⊢ (𝜑 → 𝐽 ∈ V)
15		selvadd.r	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ CRing)
16	7, 8, 9, 10, 12, 14, 15	selvcllem2 42292	. . . . . . 7 ⊢ (𝜑 → ((algSc‘𝑇) ∘ (algSc‘𝑈)) ∈ (𝑅 RingHom 𝑇))
17		rhmghm 20488	. . . . . . 7 ⊢ (((algSc‘𝑇) ∘ (algSc‘𝑈)) ∈ (𝑅 RingHom 𝑇) → ((algSc‘𝑇) ∘ (algSc‘𝑈)) ∈ (𝑅 GrpHom 𝑇))
18		ghmmhm 19242	. . . . . . 7 ⊢ (((algSc‘𝑇) ∘ (algSc‘𝑈)) ∈ (𝑅 GrpHom 𝑇) → ((algSc‘𝑇) ∘ (algSc‘𝑈)) ∈ (𝑅 MndHom 𝑇))
19	16, 17, 18	3syl 18	. . . . . 6 ⊢ (𝜑 → ((algSc‘𝑇) ∘ (algSc‘𝑈)) ∈ (𝑅 MndHom 𝑇))
20		selvadd.f	. . . . . 6 ⊢ (𝜑 → 𝐹 ∈ 𝐵)
21		selvadd.g	. . . . . 6 ⊢ (𝜑 → 𝐺 ∈ 𝐵)
22	1, 2, 3, 4, 5, 6, 19, 20, 21	mhmcoaddmpl 22395	. . . . 5 ⊢ (𝜑 → (((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ (𝐹 + 𝐺)) = ((((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐹)(+g‘(𝐼 mPoly 𝑇))(((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐺)))
23	22	fveq2d 6907	. . . 4 ⊢ (𝜑 → ((𝐼 eval 𝑇)‘(((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ (𝐹 + 𝐺))) = ((𝐼 eval 𝑇)‘((((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐹)(+g‘(𝐼 mPoly 𝑇))(((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐺))))
24	23	fveq1d 6905	. . 3 ⊢ (𝜑 → (((𝐼 eval 𝑇)‘(((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ (𝐹 + 𝐺)))‘(𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), ((algSc‘𝑇)‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥))))) = (((𝐼 eval 𝑇)‘((((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐹)(+g‘(𝐼 mPoly 𝑇))(((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐺)))‘(𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), ((algSc‘𝑇)‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥))))))
25		eqid 2729	. . . . 5 ⊢ (𝐼 eval 𝑇) = (𝐼 eval 𝑇)
26		eqid 2729	. . . . 5 ⊢ (Base‘𝑇) = (Base‘𝑇)
27		selvadd.2	. . . . 5 ⊢ ✚ = (+g‘𝑇)
28	7, 12, 15	mplcrngd 42261	. . . . . 6 ⊢ (𝜑 → 𝑈 ∈ CRing)
29	8, 14, 28	mplcrngd 42261	. . . . 5 ⊢ (𝜑 → 𝑇 ∈ CRing)
30		eqid 2729	. . . . . 6 ⊢ (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), ((algSc‘𝑇)‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥)))) = (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), ((algSc‘𝑇)‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥))))
31	7, 8, 9, 26, 30, 11, 15, 13	selvcllem5 42296	. . . . 5 ⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), ((algSc‘𝑇)‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥)))) ∈ ((Base‘𝑇) ↑m 𝐼))
32	1, 2, 3, 4, 19, 20	mhmcompl 22394	. . . . . 6 ⊢ (𝜑 → (((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐹) ∈ (Base‘(𝐼 mPoly 𝑇)))
33		eqidd 2730	. . . . . 6 ⊢ (𝜑 → (((𝐼 eval 𝑇)‘(((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐹))‘(𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), ((algSc‘𝑇)‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥))))) = (((𝐼 eval 𝑇)‘(((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐹))‘(𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), ((algSc‘𝑇)‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥))))))
34	32, 33	jca 510	. . . . 5 ⊢ (𝜑 → ((((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐹) ∈ (Base‘(𝐼 mPoly 𝑇)) ∧ (((𝐼 eval 𝑇)‘(((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐹))‘(𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), ((algSc‘𝑇)‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥))))) = (((𝐼 eval 𝑇)‘(((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐹))‘(𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), ((algSc‘𝑇)‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥)))))))
35	1, 2, 3, 4, 19, 21	mhmcompl 22394	. . . . . 6 ⊢ (𝜑 → (((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐺) ∈ (Base‘(𝐼 mPoly 𝑇)))
36		eqidd 2730	. . . . . 6 ⊢ (𝜑 → (((𝐼 eval 𝑇)‘(((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐺))‘(𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), ((algSc‘𝑇)‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥))))) = (((𝐼 eval 𝑇)‘(((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐺))‘(𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), ((algSc‘𝑇)‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥))))))
37	35, 36	jca 510	. . . . 5 ⊢ (𝜑 → ((((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐺) ∈ (Base‘(𝐼 mPoly 𝑇)) ∧ (((𝐼 eval 𝑇)‘(((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐺))‘(𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), ((algSc‘𝑇)‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥))))) = (((𝐼 eval 𝑇)‘(((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐺))‘(𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), ((algSc‘𝑇)‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥)))))))
38	25, 2, 26, 4, 6, 27, 11, 29, 31, 34, 37	evladdval 42289	. . . 4 ⊢ (𝜑 → (((((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐹)(+g‘(𝐼 mPoly 𝑇))(((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐺)) ∈ (Base‘(𝐼 mPoly 𝑇)) ∧ (((𝐼 eval 𝑇)‘((((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐹)(+g‘(𝐼 mPoly 𝑇))(((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐺)))‘(𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), ((algSc‘𝑇)‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥))))) = ((((𝐼 eval 𝑇)‘(((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐹))‘(𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), ((algSc‘𝑇)‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥))))) ✚ (((𝐼 eval 𝑇)‘(((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐺))‘(𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), ((algSc‘𝑇)‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥))))))))
39	38	simprd 494	. . 3 ⊢ (𝜑 → (((𝐼 eval 𝑇)‘((((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐹)(+g‘(𝐼 mPoly 𝑇))(((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐺)))‘(𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), ((algSc‘𝑇)‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥))))) = ((((𝐼 eval 𝑇)‘(((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐹))‘(𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), ((algSc‘𝑇)‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥))))) ✚ (((𝐼 eval 𝑇)‘(((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐺))‘(𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), ((algSc‘𝑇)‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥)))))))
40	24, 39	eqtrd 2769	. 2 ⊢ (𝜑 → (((𝐼 eval 𝑇)‘(((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ (𝐹 + 𝐺)))‘(𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), ((algSc‘𝑇)‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥))))) = ((((𝐼 eval 𝑇)‘(((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐹))‘(𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), ((algSc‘𝑇)‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥))))) ✚ (((𝐼 eval 𝑇)‘(((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐺))‘(𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), ((algSc‘𝑇)‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥)))))))
41	1, 11, 15	mplcrngd 42261	. . . . 5 ⊢ (𝜑 → 𝑃 ∈ CRing)
42	41	crnggrpd 20252	. . . 4 ⊢ (𝜑 → 𝑃 ∈ Grp)
43	3, 5, 42, 20, 21	grpcld 18963	. . 3 ⊢ (𝜑 → (𝐹 + 𝐺) ∈ 𝐵)
44	1, 3, 7, 8, 9, 10, 15, 13, 43	selvval2 42298	. 2 ⊢ (𝜑 → (((𝐼 selectVars 𝑅)‘𝐽)‘(𝐹 + 𝐺)) = (((𝐼 eval 𝑇)‘(((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ (𝐹 + 𝐺)))‘(𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), ((algSc‘𝑇)‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥))))))
45	1, 3, 7, 8, 9, 10, 15, 13, 20	selvval2 42298	. . 3 ⊢ (𝜑 → (((𝐼 selectVars 𝑅)‘𝐽)‘𝐹) = (((𝐼 eval 𝑇)‘(((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐹))‘(𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), ((algSc‘𝑇)‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥))))))
46	1, 3, 7, 8, 9, 10, 15, 13, 21	selvval2 42298	. . 3 ⊢ (𝜑 → (((𝐼 selectVars 𝑅)‘𝐽)‘𝐺) = (((𝐼 eval 𝑇)‘(((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐺))‘(𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), ((algSc‘𝑇)‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥))))))
47	45, 46	oveq12d 7446	. 2 ⊢ (𝜑 → ((((𝐼 selectVars 𝑅)‘𝐽)‘𝐹) ✚ (((𝐼 selectVars 𝑅)‘𝐽)‘𝐺)) = ((((𝐼 eval 𝑇)‘(((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐹))‘(𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), ((algSc‘𝑇)‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥))))) ✚ (((𝐼 eval 𝑇)‘(((algSc‘𝑇) ∘ (algSc‘𝑈)) ∘ 𝐺))‘(𝑥 ∈ 𝐼 ↦ if(𝑥 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑥), ((algSc‘𝑇)‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑥)))))))
48	40, 44, 47	3eqtr4d 2779	1 ⊢ (𝜑 → (((𝐼 selectVars 𝑅)‘𝐽)‘(𝐹 + 𝐺)) = ((((𝐼 selectVars 𝑅)‘𝐽)‘𝐹) ✚ (((𝐼 selectVars 𝑅)‘𝐽)‘𝐺)))

Syntax hints:   → wi 4   = wceq 1534   ∈ wcel 2100  Vcvv 3472   ∖ cdif 3954   ⊆ wss 3957  ifcif 4534   ↦ cmpt 5237   ∘ ccom 5688  ‘cfv 6556  (class class class)co 7428  Basecbs 17234  +_gcplusg 17287   MndHom cmhm 18792   GrpHom cghm 19228  CRingccrg 20239   RingHom crh 20473  algSccascl 21872   mVar cmvr 21924   mPoly cmpl 21925   eval cevl 22108   selectVars cslv 22145

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2102  ax-9 2110  ax-10 2133  ax-11 2150  ax-12 2170  ax-ext 2700  ax-rep 5291  ax-sep 5305  ax-nul 5312  ax-pow 5371  ax-pr 5435  ax-un 7749  ax-cnex 11221  ax-resscn 11222  ax-1cn 11223  ax-icn 11224  ax-addcl 11225  ax-addrcl 11226  ax-mulcl 11227  ax-mulrcl 11228  ax-mulcom 11229  ax-addass 11230  ax-mulass 11231  ax-distr 11232  ax-i2m1 11233  ax-1ne0 11234  ax-1rid 11235  ax-rnegex 11236  ax-rrecex 11237  ax-cnre 11238  ax-pre-lttri 11239  ax-pre-lttrn 11240  ax-pre-ltadd 11241  ax-pre-mulgt0 11242

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2062  df-mo 2532  df-eu 2561  df-clab 2707  df-cleq 2721  df-clel 2806  df-nfc 2881  df-ne 2934  df-nel 3040  df-ral 3055  df-rex 3064  df-rmo 3373  df-reu 3374  df-rab 3429  df-v 3474  df-sbc 3787  df-csb 3903  df-dif 3960  df-un 3962  df-in 3964  df-ss 3974  df-pss 3977  df-nul 4334  df-if 4535  df-pw 4610  df-sn 4635  df-pr 4637  df-tp 4639  df-op 4641  df-uni 4917  df-int 4958  df-iun 5006  df-iin 5007  df-br 5155  df-opab 5217  df-mpt 5238  df-tr 5272  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5639  df-se 5640  df-we 5641  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-pred 6315  df-ord 6381  df-on 6382  df-lim 6383  df-suc 6384  df-iota 6508  df-fun 6558  df-fn 6559  df-f 6560  df-f1 6561  df-fo 6562  df-f1o 6563  df-fv 6564  df-isom 6565  df-riota 7384  df-ov 7431  df-oprab 7432  df-mpo 7433  df-of 7693  df-ofr 7694  df-om 7883  df-1st 8009  df-2nd 8010  df-supp 8181  df-frecs 8302  df-wrecs 8333  df-recs 8407  df-rdg 8446  df-1o 8502  df-2o 8503  df-er 8740  df-map 8863  df-pm 8864  df-ixp 8933  df-en 8981  df-dom 8982  df-sdom 8983  df-fin 8984  df-fsupp 9413  df-sup 9492  df-oi 9560  df-card 9989  df-pnf 11307  df-mnf 11308  df-xr 11309  df-ltxr 11310  df-le 11311  df-sub 11503  df-neg 11504  df-nn 12275  df-2 12337  df-3 12338  df-4 12339  df-5 12340  df-6 12341  df-7 12342  df-8 12343  df-9 12344  df-n0 12535  df-z 12621  df-dec 12740  df-uz 12885  df-fz 13549  df-fzo 13692  df-seq 14033  df-hash 14360  df-struct 17170  df-sets 17187  df-slot 17205  df-ndx 17217  df-base 17235  df-ress 17264  df-plusg 17300  df-mulr 17301  df-sca 17303  df-vsca 17304  df-ip 17305  df-tset 17306  df-ple 17307  df-ds 17309  df-hom 17311  df-cco 17312  df-0g 17477  df-gsum 17478  df-prds 17483  df-pws 17485  df-mre 17620  df-mrc 17621  df-acs 17623  df-mgm 18654  df-sgrp 18733  df-mnd 18749  df-mhm 18794  df-submnd 18795  df-grp 18952  df-minusg 18953  df-sbg 18954  df-mulg 19084  df-subg 19139  df-ghm 19229  df-cntz 19333  df-cmn 19802  df-abl 19803  df-mgp 20140  df-rng 20158  df-ur 20187  df-srg 20192  df-ring 20240  df-cring 20241  df-rhm 20476  df-subrng 20550  df-subrg 20575  df-lmod 20860  df-lss 20931  df-lsp 20971  df-assa 21873  df-asp 21874  df-ascl 21875  df-psr 21928  df-mvr 21929  df-mpl 21930  df-evls 22109  df-evl 22110  df-selv 22149

This theorem is referenced by: (None)