Theorem selvascl 33704

Description: The "variable selection" function evaluated at a scalar. (Contributed by Thierry Arnoux, 4-May-2026.)

Hypotheses

Ref	Expression
selvascl.1	⊢ 𝐵 = (Base‘𝑅)
selvascl.2	⊢ 𝑃 = (𝐼 mPoly 𝑅)
selvascl.3	⊢ 𝐴 = (algSc‘𝑃)
selvascl.4	⊢ 𝐶 = (algSc‘𝑇)
selvascl.5	⊢ (𝜑 → 𝐼 ∈ 𝑉)
selvascl.6	⊢ (𝜑 → 𝑋 ∈ 𝐵)
selvascl.7	⊢ 𝑈 = ((𝐼 ∖ 𝐽) mPoly 𝑅)
selvascl.8	⊢ 𝑇 = (𝐽 mPoly 𝑈)
selvascl.9	⊢ 𝐷 = (𝐶 ∘ (algSc‘𝑈))
selvascl.10	⊢ (𝜑 → 𝑅 ∈ CRing)
selvascl.11	⊢ (𝜑 → 𝐽 ⊆ 𝐼)

Assertion

Ref	Expression
selvascl	⊢ (𝜑 → (((𝐼 selectVars 𝑅)‘𝐽)‘(𝐴‘𝑋)) = (𝐷‘𝑋))

Proof of Theorem selvascl

Dummy variables 𝑖 ℎ are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		selvascl.9	. . . . . . . . . 10 ⊢ 𝐷 = (𝐶 ∘ (algSc‘𝑈))
2	1	coeq1i 5804	. . . . . . . . 9 ⊢ (𝐷 ∘ (𝐴‘𝑋)) = ((𝐶 ∘ (algSc‘𝑈)) ∘ (𝐴‘𝑋))
3		coass 6220	. . . . . . . . 9 ⊢ ((𝐶 ∘ (algSc‘𝑈)) ∘ (𝐴‘𝑋)) = (𝐶 ∘ ((algSc‘𝑈) ∘ (𝐴‘𝑋)))
4	2, 3	eqtri 2759	. . . . . . . 8 ⊢ (𝐷 ∘ (𝐴‘𝑋)) = (𝐶 ∘ ((algSc‘𝑈) ∘ (𝐴‘𝑋)))
5		selvascl.1	. . . . . . . . . 10 ⊢ 𝐵 = (Base‘𝑅)
6		selvascl.7	. . . . . . . . . 10 ⊢ 𝑈 = ((𝐼 ∖ 𝐽) mPoly 𝑅)
7		selvascl.2	. . . . . . . . . 10 ⊢ 𝑃 = (𝐼 mPoly 𝑅)
8		eqid 2736	. . . . . . . . . 10 ⊢ (𝐼 mPoly 𝑈) = (𝐼 mPoly 𝑈)
9		eqid 2736	. . . . . . . . . 10 ⊢ (algSc‘𝑈) = (algSc‘𝑈)
10		selvascl.3	. . . . . . . . . 10 ⊢ 𝐴 = (algSc‘𝑃)
11		eqid 2736	. . . . . . . . . 10 ⊢ (algSc‘(𝐼 mPoly 𝑈)) = (algSc‘(𝐼 mPoly 𝑈))
12		eqid 2736	. . . . . . . . . 10 ⊢ {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin} = {ℎ ∈ (ℕ0 ↑m 𝐼) ∣ (◡ℎ “ ℕ) ∈ Fin}
13		eqid 2736	. . . . . . . . . 10 ⊢ {ℎ ∈ (ℕ0 ↑m (𝐼 ∖ 𝐽)) ∣ (◡ℎ “ ℕ) ∈ Fin} = {ℎ ∈ (ℕ0 ↑m (𝐼 ∖ 𝐽)) ∣ (◡ℎ “ ℕ) ∈ Fin}
14		selvascl.5	. . . . . . . . . 10 ⊢ (𝜑 → 𝐼 ∈ 𝑉)
15		difssd 4070	. . . . . . . . . 10 ⊢ (𝜑 → (𝐼 ∖ 𝐽) ⊆ 𝐼)
16		selvascl.10	. . . . . . . . . 10 ⊢ (𝜑 → 𝑅 ∈ CRing)
17		selvascl.6	. . . . . . . . . 10 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
18	5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17	mplasclco 33703	. . . . . . . . 9 ⊢ (𝜑 → ((algSc‘𝑈) ∘ (𝐴‘𝑋)) = ((algSc‘(𝐼 mPoly 𝑈))‘((algSc‘𝑈)‘𝑋)))
19	18	coeq2d 5807	. . . . . . . 8 ⊢ (𝜑 → (𝐶 ∘ ((algSc‘𝑈) ∘ (𝐴‘𝑋))) = (𝐶 ∘ ((algSc‘(𝐼 mPoly 𝑈))‘((algSc‘𝑈)‘𝑋))))
20	4, 19	eqtrid 2783	. . . . . . 7 ⊢ (𝜑 → (𝐷 ∘ (𝐴‘𝑋)) = (𝐶 ∘ ((algSc‘(𝐼 mPoly 𝑈))‘((algSc‘𝑈)‘𝑋))))
21		eqid 2736	. . . . . . . 8 ⊢ (Base‘𝑈) = (Base‘𝑈)
22		selvascl.8	. . . . . . . 8 ⊢ 𝑇 = (𝐽 mPoly 𝑈)
23		eqid 2736	. . . . . . . 8 ⊢ (𝐼 mPoly 𝑇) = (𝐼 mPoly 𝑇)
24		selvascl.4	. . . . . . . 8 ⊢ 𝐶 = (algSc‘𝑇)
25		eqid 2736	. . . . . . . 8 ⊢ (algSc‘(𝐼 mPoly 𝑇)) = (algSc‘(𝐼 mPoly 𝑇))
26		eqid 2736	. . . . . . . 8 ⊢ {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ (◡ℎ “ ℕ) ∈ Fin} = {ℎ ∈ (ℕ0 ↑m 𝐽) ∣ (◡ℎ “ ℕ) ∈ Fin}
27		selvascl.11	. . . . . . . 8 ⊢ (𝜑 → 𝐽 ⊆ 𝐼)
28	14	difexd 5262	. . . . . . . . 9 ⊢ (𝜑 → (𝐼 ∖ 𝐽) ∈ V)
29	6, 28, 16	mplcrngd 22001	. . . . . . . 8 ⊢ (𝜑 → 𝑈 ∈ CRing)
30		eqid 2736	. . . . . . . . . 10 ⊢ (Scalar‘𝑈) = (Scalar‘𝑈)
31	16	crngringd 20221	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑅 ∈ Ring)
32	6, 28, 31	mplringd 22000	. . . . . . . . . 10 ⊢ (𝜑 → 𝑈 ∈ Ring)
33	6, 28, 31	mpllmodd 22002	. . . . . . . . . 10 ⊢ (𝜑 → 𝑈 ∈ LMod)
34		eqid 2736	. . . . . . . . . 10 ⊢ (Base‘(Scalar‘𝑈)) = (Base‘(Scalar‘𝑈))
35	9, 30, 32, 33, 34, 21	asclf 21859	. . . . . . . . 9 ⊢ (𝜑 → (algSc‘𝑈):(Base‘(Scalar‘𝑈))⟶(Base‘𝑈))
36	6, 28, 31	mplsca 21990	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑅 = (Scalar‘𝑈))
37	36	fveq2d 6834	. . . . . . . . . . 11 ⊢ (𝜑 → (Base‘𝑅) = (Base‘(Scalar‘𝑈)))
38	5, 37	eqtr2id 2784	. . . . . . . . . 10 ⊢ (𝜑 → (Base‘(Scalar‘𝑈)) = 𝐵)
39	17, 38	eleqtrrd 2839	. . . . . . . . 9 ⊢ (𝜑 → 𝑋 ∈ (Base‘(Scalar‘𝑈)))
40	35, 39	ffvelcdmd 7029	. . . . . . . 8 ⊢ (𝜑 → ((algSc‘𝑈)‘𝑋) ∈ (Base‘𝑈))
41	21, 22, 8, 23, 24, 11, 25, 12, 26, 14, 27, 29, 40	mplasclco 33703	. . . . . . 7 ⊢ (𝜑 → (𝐶 ∘ ((algSc‘(𝐼 mPoly 𝑈))‘((algSc‘𝑈)‘𝑋))) = ((algSc‘(𝐼 mPoly 𝑇))‘(𝐶‘((algSc‘𝑈)‘𝑋))))
42	20, 41	eqtrd 2771	. . . . . 6 ⊢ (𝜑 → (𝐷 ∘ (𝐴‘𝑋)) = ((algSc‘(𝐼 mPoly 𝑇))‘(𝐶‘((algSc‘𝑈)‘𝑋))))
43	42	fveq2d 6834	. . . . 5 ⊢ (𝜑 → ((𝐼 eval 𝑇)‘(𝐷 ∘ (𝐴‘𝑋))) = ((𝐼 eval 𝑇)‘((algSc‘(𝐼 mPoly 𝑇))‘(𝐶‘((algSc‘𝑈)‘𝑋)))))
44		eqid 2736	. . . . . 6 ⊢ (𝐼 eval 𝑇) = (𝐼 eval 𝑇)
45		eqid 2736	. . . . . 6 ⊢ (Base‘𝑇) = (Base‘𝑇)
46	14, 27	ssexd 5255	. . . . . . 7 ⊢ (𝜑 → 𝐽 ∈ V)
47	22, 46, 29	mplcrngd 22001	. . . . . 6 ⊢ (𝜑 → 𝑇 ∈ CRing)
48	22, 45, 21, 24, 46, 32	mplasclf 22044	. . . . . . 7 ⊢ (𝜑 → 𝐶:(Base‘𝑈)⟶(Base‘𝑇))
49	48, 40	ffvelcdmd 7029	. . . . . 6 ⊢ (𝜑 → (𝐶‘((algSc‘𝑈)‘𝑋)) ∈ (Base‘𝑇))
50	44, 23, 45, 25, 14, 47, 49	evlsca 22085	. . . . 5 ⊢ (𝜑 → ((𝐼 eval 𝑇)‘((algSc‘(𝐼 mPoly 𝑇))‘(𝐶‘((algSc‘𝑈)‘𝑋)))) = (((Base‘𝑇) ↑m 𝐼) × {(𝐶‘((algSc‘𝑈)‘𝑋))}))
51	43, 50	eqtrd 2771	. . . 4 ⊢ (𝜑 → ((𝐼 eval 𝑇)‘(𝐷 ∘ (𝐴‘𝑋))) = (((Base‘𝑇) ↑m 𝐼) × {(𝐶‘((algSc‘𝑈)‘𝑋))}))
52	51	fveq1d 6832	. . 3 ⊢ (𝜑 → (((𝐼 eval 𝑇)‘(𝐷 ∘ (𝐴‘𝑋)))‘(𝑖 ∈ 𝐼 ↦ if(𝑖 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑖), (𝐶‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑖))))) = ((((Base‘𝑇) ↑m 𝐼) × {(𝐶‘((algSc‘𝑈)‘𝑋))})‘(𝑖 ∈ 𝐼 ↦ if(𝑖 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑖), (𝐶‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑖))))))
53	47	crngringd 20221	. . . . . 6 ⊢ (𝜑 → 𝑇 ∈ Ring)
54	45	subrgid 20548	. . . . . 6 ⊢ (𝑇 ∈ Ring → (Base‘𝑇) ∈ (SubRing‘𝑇))
55	53, 54	syl 17	. . . . 5 ⊢ (𝜑 → (Base‘𝑇) ∈ (SubRing‘𝑇))
56		eqid 2736	. . . . . . . 8 ⊢ (𝐽 mVar 𝑈) = (𝐽 mVar 𝑈)
57	46	ad2antrr 728	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ 𝑖 ∈ 𝐽) → 𝐽 ∈ V)
58	32	ad2antrr 728	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ 𝑖 ∈ 𝐽) → 𝑈 ∈ Ring)
59		simpr 485	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ 𝑖 ∈ 𝐽) → 𝑖 ∈ 𝐽)
60	22, 56, 45, 57, 58, 59	mvrcl 21969	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ 𝑖 ∈ 𝐽) → ((𝐽 mVar 𝑈)‘𝑖) ∈ (Base‘𝑇))
61	48	ad2antrr 728	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ ¬ 𝑖 ∈ 𝐽) → 𝐶:(Base‘𝑈)⟶(Base‘𝑇))
62		eqid 2736	. . . . . . . . 9 ⊢ ((𝐼 ∖ 𝐽) mVar 𝑅) = ((𝐼 ∖ 𝐽) mVar 𝑅)
63	28	ad2antrr 728	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ ¬ 𝑖 ∈ 𝐽) → (𝐼 ∖ 𝐽) ∈ V)
64	31	ad2antrr 728	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ ¬ 𝑖 ∈ 𝐽) → 𝑅 ∈ Ring)
65		simplr 770	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ ¬ 𝑖 ∈ 𝐽) → 𝑖 ∈ 𝐼)
66		simpr 485	. . . . . . . . . 10 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ ¬ 𝑖 ∈ 𝐽) → ¬ 𝑖 ∈ 𝐽)
67	65, 66	eldifd 3897	. . . . . . . . 9 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ ¬ 𝑖 ∈ 𝐽) → 𝑖 ∈ (𝐼 ∖ 𝐽))
68	6, 62, 21, 63, 64, 67	mvrcl 21969	. . . . . . . 8 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ ¬ 𝑖 ∈ 𝐽) → (((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑖) ∈ (Base‘𝑈))
69	61, 68	ffvelcdmd 7029	. . . . . . 7 ⊢ (((𝜑 ∧ 𝑖 ∈ 𝐼) ∧ ¬ 𝑖 ∈ 𝐽) → (𝐶‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑖)) ∈ (Base‘𝑇))
70	60, 69	ifclda 4493	. . . . . 6 ⊢ ((𝜑 ∧ 𝑖 ∈ 𝐼) → if(𝑖 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑖), (𝐶‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑖))) ∈ (Base‘𝑇))
71	70	fmpttd 7059	. . . . 5 ⊢ (𝜑 → (𝑖 ∈ 𝐼 ↦ if(𝑖 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑖), (𝐶‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑖)))):𝐼⟶(Base‘𝑇))
72	55, 14, 71	elmapdd 8781	. . . 4 ⊢ (𝜑 → (𝑖 ∈ 𝐼 ↦ if(𝑖 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑖), (𝐶‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑖)))) ∈ ((Base‘𝑇) ↑m 𝐼))
73		fvex 6843	. . . . 5 ⊢ (𝐶‘((algSc‘𝑈)‘𝑋)) ∈ V
74	73	fvconst2 7151	. . . 4 ⊢ ((𝑖 ∈ 𝐼 ↦ if(𝑖 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑖), (𝐶‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑖)))) ∈ ((Base‘𝑇) ↑m 𝐼) → ((((Base‘𝑇) ↑m 𝐼) × {(𝐶‘((algSc‘𝑈)‘𝑋))})‘(𝑖 ∈ 𝐼 ↦ if(𝑖 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑖), (𝐶‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑖))))) = (𝐶‘((algSc‘𝑈)‘𝑋)))
75	72, 74	syl 17	. . 3 ⊢ (𝜑 → ((((Base‘𝑇) ↑m 𝐼) × {(𝐶‘((algSc‘𝑈)‘𝑋))})‘(𝑖 ∈ 𝐼 ↦ if(𝑖 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑖), (𝐶‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑖))))) = (𝐶‘((algSc‘𝑈)‘𝑋)))
76	52, 75	eqtrd 2771	. 2 ⊢ (𝜑 → (((𝐼 eval 𝑇)‘(𝐷 ∘ (𝐴‘𝑋)))‘(𝑖 ∈ 𝐼 ↦ if(𝑖 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑖), (𝐶‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑖))))) = (𝐶‘((algSc‘𝑈)‘𝑋)))
77		eqid 2736	. . 3 ⊢ (Base‘𝑃) = (Base‘𝑃)
78		eqid 2736	. . . . 5 ⊢ (Scalar‘𝑃) = (Scalar‘𝑃)
79	7, 14, 31	mplringd 22000	. . . . 5 ⊢ (𝜑 → 𝑃 ∈ Ring)
80	7, 14, 31	mpllmodd 22002	. . . . 5 ⊢ (𝜑 → 𝑃 ∈ LMod)
81		eqid 2736	. . . . 5 ⊢ (Base‘(Scalar‘𝑃)) = (Base‘(Scalar‘𝑃))
82	10, 78, 79, 80, 81, 77	asclf 21859	. . . 4 ⊢ (𝜑 → 𝐴:(Base‘(Scalar‘𝑃))⟶(Base‘𝑃))
83	7, 14, 31	mplsca 21990	. . . . . . 7 ⊢ (𝜑 → 𝑅 = (Scalar‘𝑃))
84	83	fveq2d 6834	. . . . . 6 ⊢ (𝜑 → (Base‘𝑅) = (Base‘(Scalar‘𝑃)))
85	5, 84	eqtr2id 2784	. . . . 5 ⊢ (𝜑 → (Base‘(Scalar‘𝑃)) = 𝐵)
86	17, 85	eleqtrrd 2839	. . . 4 ⊢ (𝜑 → 𝑋 ∈ (Base‘(Scalar‘𝑃)))
87	82, 86	ffvelcdmd 7029	. . 3 ⊢ (𝜑 → (𝐴‘𝑋) ∈ (Base‘𝑃))
88	7, 77, 6, 22, 24, 1, 16, 27, 87	selvval2 22120	. 2 ⊢ (𝜑 → (((𝐼 selectVars 𝑅)‘𝐽)‘(𝐴‘𝑋)) = (((𝐼 eval 𝑇)‘(𝐷 ∘ (𝐴‘𝑋)))‘(𝑖 ∈ 𝐼 ↦ if(𝑖 ∈ 𝐽, ((𝐽 mVar 𝑈)‘𝑖), (𝐶‘(((𝐼 ∖ 𝐽) mVar 𝑅)‘𝑖))))))
89	35	ffund 6662	. . 3 ⊢ (𝜑 → Fun (algSc‘𝑈))
90	35	fdmd 6668	. . . 4 ⊢ (𝜑 → dom (algSc‘𝑈) = (Base‘(Scalar‘𝑈)))
91	39, 90	eleqtrrd 2839	. . 3 ⊢ (𝜑 → 𝑋 ∈ dom (algSc‘𝑈))
92	89, 91, 1	fvcod 6929	. 2 ⊢ (𝜑 → (𝐷‘𝑋) = (𝐶‘((algSc‘𝑈)‘𝑋)))
93	76, 88, 92	3eqtr4d 2781	1 ⊢ (𝜑 → (((𝐼 selectVars 𝑅)‘𝐽)‘(𝐴‘𝑋)) = (𝐷‘𝑋))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 396   = wceq 1543   ∈ wcel 2115  {crab 3388  Vcvv 3428   ∖ cdif 3883   ⊆ wss 3886  ifcif 4457  {csn 4558   ↦ cmpt 5156   × cxp 5619  ^◡ccnv 5620  dom cdm 5621   “ cima 5624   ∘ ccom 5625  ⟶wf 6484  ‘cfv 6488  (class class class)co 7359   ↑_m cmap 8766  Fincfn 8886  ℕcn 12168  ℕ₀cn0 12431  Basecbs 17173  Scalarcsca 17217  Ringcrg 20208  CRingccrg 20209  SubRingcsubrg 20544  algSccascl 21830   mVar cmvr 21883   mPoly cmpl 21884   eval cevl 22052   selectVars cslv 22095

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1970  ax-7 2011  ax-8 2117  ax-9 2125  ax-10 2148  ax-11 2164  ax-12 2185  ax-ext 2708  ax-rep 5202  ax-sep 5221  ax-nul 5231  ax-pow 5297  ax-pr 5365  ax-un 7681  ax-cnex 11088  ax-resscn 11089  ax-1cn 11090  ax-icn 11091  ax-addcl 11092  ax-addrcl 11093  ax-mulcl 11094  ax-mulrcl 11095  ax-mulcom 11096  ax-addass 11097  ax-mulass 11098  ax-distr 11099  ax-i2m1 11100  ax-1ne0 11101  ax-1rid 11102  ax-rnegex 11103  ax-rrecex 11104  ax-cnre 11105  ax-pre-lttri 11106  ax-pre-lttrn 11107  ax-pre-ltadd 11108  ax-pre-mulgt0 11109

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 850  df-3or 1089  df-3an 1090  df-tru 1546  df-fal 1556  df-ex 1783  df-nf 1787  df-sb 2070  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2932  df-nel 3036  df-ral 3051  df-rex 3061  df-rmo 3341  df-reu 3342  df-rab 3389  df-v 3430  df-sbc 3727  df-csb 3835  df-dif 3889  df-un 3891  df-in 3893  df-ss 3903  df-pss 3906  df-nul 4265  df-if 4458  df-pw 4534  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4842  df-int 4881  df-iun 4926  df-iin 4927  df-br 5076  df-opab 5138  df-mpt 5157  df-tr 5183  df-id 5516  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-se 5575  df-we 5576  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6255  df-ord 6316  df-on 6317  df-lim 6318  df-suc 6319  df-iota 6444  df-fun 6490  df-fn 6491  df-f 6492  df-f1 6493  df-fo 6494  df-f1o 6495  df-fv 6496  df-isom 6497  df-riota 7316  df-ov 7362  df-oprab 7363  df-mpo 7364  df-of 7623  df-ofr 7624  df-om 7810  df-1st 7934  df-2nd 7935  df-supp 8104  df-frecs 8224  df-wrecs 8255  df-recs 8304  df-rdg 8342  df-1o 8398  df-2o 8399  df-er 8636  df-map 8768  df-pm 8769  df-ixp 8839  df-en 8887  df-dom 8888  df-sdom 8889  df-fin 8890  df-fsupp 9268  df-sup 9348  df-oi 9418  df-card 9857  df-pnf 11175  df-mnf 11176  df-xr 11177  df-ltxr 11178  df-le 11179  df-sub 11373  df-neg 11374  df-nn 12169  df-2 12238  df-3 12239  df-4 12240  df-5 12241  df-6 12242  df-7 12243  df-8 12244  df-9 12245  df-n0 12432  df-z 12519  df-dec 12639  df-uz 12783  df-fz 13456  df-fzo 13603  df-seq 13958  df-hash 14287  df-struct 17111  df-sets 17128  df-slot 17146  df-ndx 17158  df-base 17174  df-ress 17195  df-plusg 17227  df-mulr 17228  df-sca 17230  df-vsca 17231  df-ip 17232  df-tset 17233  df-ple 17234  df-ds 17236  df-hom 17238  df-cco 17239  df-0g 17398  df-gsum 17399  df-prds 17404  df-pws 17406  df-mre 17542  df-mrc 17543  df-acs 17545  df-mgm 18602  df-sgrp 18681  df-mnd 18697  df-mhm 18745  df-submnd 18746  df-grp 18906  df-minusg 18907  df-sbg 18908  df-mulg 19038  df-subg 19093  df-ghm 19182  df-cntz 19286  df-cmn 19751  df-abl 19752  df-mgp 20116  df-rng 20128  df-ur 20157  df-srg 20162  df-ring 20210  df-cring 20211  df-rhm 20446  df-subrng 20521  df-subrg 20545  df-lmod 20855  df-lss 20925  df-lsp 20965  df-assa 21831  df-asp 21832  df-ascl 21833  df-psr 21887  df-mvr 21888  df-mpl 21889  df-evls 22053  df-evl 22054  df-selv 22096

This theorem is referenced by:  selvply1rhmlem2  33708