Theorem evlseu 22059

Description: For a given interpretation of the variables 𝐺 and of the scalars 𝐹, this extends to a homomorphic interpretation of the polynomial ring in exactly one way. (Contributed by Stefan O'Rear, 9-Mar-2015.) (Revised by AV, 11-Apr-2024.)

Hypotheses

Ref	Expression
evlseu.p	⊢ 𝑃 = (𝐼 mPoly 𝑅)
evlseu.c	⊢ 𝐶 = (Base‘𝑆)
evlseu.a	⊢ 𝐴 = (algSc‘𝑃)
evlseu.v	⊢ 𝑉 = (𝐼 mVar 𝑅)
evlseu.i	⊢ (𝜑 → 𝐼 ∈ 𝑊)
evlseu.r	⊢ (𝜑 → 𝑅 ∈ CRing)
evlseu.s	⊢ (𝜑 → 𝑆 ∈ CRing)
evlseu.f	⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆))
evlseu.g	⊢ (𝜑 → 𝐺:𝐼⟶𝐶)

Assertion

Ref	Expression
evlseu	⊢ (𝜑 → ∃!𝑚 ∈ (𝑃 RingHom 𝑆)((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺))

Distinct variable groups:   𝐴,𝑚   𝑚,𝐹   𝑚,𝐺   𝑚,𝐼   𝑃,𝑚   𝜑,𝑚   𝑆,𝑚   𝑚,𝑉

Allowed substitution hints:   𝐶(𝑚)   𝑅(𝑚)   𝑊(𝑚)

Proof of Theorem evlseu

Dummy variables 𝑛 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		evlseu.p	. . . 4 ⊢ 𝑃 = (𝐼 mPoly 𝑅)
2		eqid 2739	. . . 4 ⊢ (Base‘𝑃) = (Base‘𝑃)
3		evlseu.c	. . . 4 ⊢ 𝐶 = (Base‘𝑆)
4		eqid 2739	. . . 4 ⊢ {𝑧 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑧 “ ℕ) ∈ Fin} = {𝑧 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑧 “ ℕ) ∈ Fin}
5		eqid 2739	. . . 4 ⊢ (mulGrp‘𝑆) = (mulGrp‘𝑆)
6		eqid 2739	. . . 4 ⊢ (.g‘(mulGrp‘𝑆)) = (.g‘(mulGrp‘𝑆))
7		eqid 2739	. . . 4 ⊢ (.r‘𝑆) = (.r‘𝑆)
8		evlseu.v	. . . 4 ⊢ 𝑉 = (𝐼 mVar 𝑅)
9		eqid 2739	. . . 4 ⊢ (𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘f (.g‘(mulGrp‘𝑆))𝐺)))))) = (𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘f (.g‘(mulGrp‘𝑆))𝐺))))))
10		evlseu.i	. . . 4 ⊢ (𝜑 → 𝐼 ∈ 𝑊)
11		evlseu.r	. . . 4 ⊢ (𝜑 → 𝑅 ∈ CRing)
12		evlseu.s	. . . 4 ⊢ (𝜑 → 𝑆 ∈ CRing)
13		evlseu.f	. . . 4 ⊢ (𝜑 → 𝐹 ∈ (𝑅 RingHom 𝑆))
14		evlseu.g	. . . 4 ⊢ (𝜑 → 𝐺:𝐼⟶𝐶)
15		evlseu.a	. . . 4 ⊢ 𝐴 = (algSc‘𝑃)
16	1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15	evlslem1 22058	. . 3 ⊢ (𝜑 → ((𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘f (.g‘(mulGrp‘𝑆))𝐺)))))) ∈ (𝑃 RingHom 𝑆) ∧ ((𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘f (.g‘(mulGrp‘𝑆))𝐺)))))) ∘ 𝐴) = 𝐹 ∧ ((𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘f (.g‘(mulGrp‘𝑆))𝐺)))))) ∘ 𝑉) = 𝐺))
17		coeq1 5799	. . . . . . 7 ⊢ (𝑚 = (𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘f (.g‘(mulGrp‘𝑆))𝐺)))))) → (𝑚 ∘ 𝐴) = ((𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘f (.g‘(mulGrp‘𝑆))𝐺)))))) ∘ 𝐴))
18	17	eqeq1d 2741	. . . . . 6 ⊢ (𝑚 = (𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘f (.g‘(mulGrp‘𝑆))𝐺)))))) → ((𝑚 ∘ 𝐴) = 𝐹 ↔ ((𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘f (.g‘(mulGrp‘𝑆))𝐺)))))) ∘ 𝐴) = 𝐹))
19		coeq1 5799	. . . . . . 7 ⊢ (𝑚 = (𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘f (.g‘(mulGrp‘𝑆))𝐺)))))) → (𝑚 ∘ 𝑉) = ((𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘f (.g‘(mulGrp‘𝑆))𝐺)))))) ∘ 𝑉))
20	19	eqeq1d 2741	. . . . . 6 ⊢ (𝑚 = (𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘f (.g‘(mulGrp‘𝑆))𝐺)))))) → ((𝑚 ∘ 𝑉) = 𝐺 ↔ ((𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘f (.g‘(mulGrp‘𝑆))𝐺)))))) ∘ 𝑉) = 𝐺))
21	18, 20	anbi12d 638	. . . . 5 ⊢ (𝑚 = (𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘f (.g‘(mulGrp‘𝑆))𝐺)))))) → (((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺) ↔ (((𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘f (.g‘(mulGrp‘𝑆))𝐺)))))) ∘ 𝐴) = 𝐹 ∧ ((𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘f (.g‘(mulGrp‘𝑆))𝐺)))))) ∘ 𝑉) = 𝐺)))
22	21	rspcev 3560	. . . 4 ⊢ (((𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘f (.g‘(mulGrp‘𝑆))𝐺)))))) ∈ (𝑃 RingHom 𝑆) ∧ (((𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘f (.g‘(mulGrp‘𝑆))𝐺)))))) ∘ 𝐴) = 𝐹 ∧ ((𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘f (.g‘(mulGrp‘𝑆))𝐺)))))) ∘ 𝑉) = 𝐺)) → ∃𝑚 ∈ (𝑃 RingHom 𝑆)((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺))
23	22	3impb 1120	. . 3 ⊢ (((𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘f (.g‘(mulGrp‘𝑆))𝐺)))))) ∈ (𝑃 RingHom 𝑆) ∧ ((𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘f (.g‘(mulGrp‘𝑆))𝐺)))))) ∘ 𝐴) = 𝐹 ∧ ((𝑥 ∈ (Base‘𝑃) ↦ (𝑆 Σg (𝑦 ∈ {𝑧 ∈ (ℕ0 ↑m 𝐼) ∣ (◡𝑧 “ ℕ) ∈ Fin} ↦ ((𝐹‘(𝑥‘𝑦))(.r‘𝑆)((mulGrp‘𝑆) Σg (𝑦 ∘f (.g‘(mulGrp‘𝑆))𝐺)))))) ∘ 𝑉) = 𝐺) → ∃𝑚 ∈ (𝑃 RingHom 𝑆)((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺))
24	16, 23	syl 17	. 2 ⊢ (𝜑 → ∃𝑚 ∈ (𝑃 RingHom 𝑆)((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺))
25		eqid 2739	. . . . . . . . . 10 ⊢ (Base‘𝑅) = (Base‘𝑅)
26		crngring 20217	. . . . . . . . . . 11 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)
27	11, 26	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → 𝑅 ∈ Ring)
28	1, 2, 25, 15, 10, 27	mplasclf 22041	. . . . . . . . 9 ⊢ (𝜑 → 𝐴:(Base‘𝑅)⟶(Base‘𝑃))
29	28	ffund 6659	. . . . . . . 8 ⊢ (𝜑 → Fun 𝐴)
30		funcoeqres 6798	. . . . . . . 8 ⊢ ((Fun 𝐴 ∧ (𝑚 ∘ 𝐴) = 𝐹) → (𝑚 ↾ ran 𝐴) = (𝐹 ∘ ◡𝐴))
31	29, 30	sylan 586	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∘ 𝐴) = 𝐹) → (𝑚 ↾ ran 𝐴) = (𝐹 ∘ ◡𝐴))
32	1, 8, 2, 10, 27	mvrf2 21967	. . . . . . . . 9 ⊢ (𝜑 → 𝑉:𝐼⟶(Base‘𝑃))
33	32	ffund 6659	. . . . . . . 8 ⊢ (𝜑 → Fun 𝑉)
34		funcoeqres 6798	. . . . . . . 8 ⊢ ((Fun 𝑉 ∧ (𝑚 ∘ 𝑉) = 𝐺) → (𝑚 ↾ ran 𝑉) = (𝐺 ∘ ◡𝑉))
35	33, 34	sylan 586	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∘ 𝑉) = 𝐺) → (𝑚 ↾ ran 𝑉) = (𝐺 ∘ ◡𝑉))
36	31, 35	anim12dan 625	. . . . . 6 ⊢ ((𝜑 ∧ ((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺)) → ((𝑚 ↾ ran 𝐴) = (𝐹 ∘ ◡𝐴) ∧ (𝑚 ↾ ran 𝑉) = (𝐺 ∘ ◡𝑉)))
37	36	ex 413	. . . . 5 ⊢ (𝜑 → (((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺) → ((𝑚 ↾ ran 𝐴) = (𝐹 ∘ ◡𝐴) ∧ (𝑚 ↾ ran 𝑉) = (𝐺 ∘ ◡𝑉))))
38		resundi 5945	. . . . . 6 ⊢ (𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝑚 ↾ ran 𝐴) ∪ (𝑚 ↾ ran 𝑉))
39		uneq12 4093	. . . . . 6 ⊢ (((𝑚 ↾ ran 𝐴) = (𝐹 ∘ ◡𝐴) ∧ (𝑚 ↾ ran 𝑉) = (𝐺 ∘ ◡𝑉)) → ((𝑚 ↾ ran 𝐴) ∪ (𝑚 ↾ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉)))
40	38, 39	eqtrid 2786	. . . . 5 ⊢ (((𝑚 ↾ ran 𝐴) = (𝐹 ∘ ◡𝐴) ∧ (𝑚 ↾ ran 𝑉) = (𝐺 ∘ ◡𝑉)) → (𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉)))
41	37, 40	syl6 35	. . . 4 ⊢ (𝜑 → (((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺) → (𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉))))
42	41	ralrimivw 3135	. . 3 ⊢ (𝜑 → ∀𝑚 ∈ (𝑃 RingHom 𝑆)(((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺) → (𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉))))
43		eqtr3 2761	. . . . . 6 ⊢ (((𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉)) ∧ (𝑛 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉))) → (𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = (𝑛 ↾ (ran 𝐴 ∪ ran 𝑉)))
44		eqid 2739	. . . . . . . . . . . . 13 ⊢ (𝐼 mPwSer 𝑅) = (𝐼 mPwSer 𝑅)
45	44, 10, 11	psrassa 21947	. . . . . . . . . . . 12 ⊢ (𝜑 → (𝐼 mPwSer 𝑅) ∈ AssAlg)
46		eqid 2739	. . . . . . . . . . . . . 14 ⊢ (Base‘(𝐼 mPwSer 𝑅)) = (Base‘(𝐼 mPwSer 𝑅))
47	44, 8, 46, 10, 27	mvrf 21959	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑉:𝐼⟶(Base‘(𝐼 mPwSer 𝑅)))
48	47	frnd 6663	. . . . . . . . . . . 12 ⊢ (𝜑 → ran 𝑉 ⊆ (Base‘(𝐼 mPwSer 𝑅)))
49		eqid 2739	. . . . . . . . . . . . 13 ⊢ (AlgSpan‘(𝐼 mPwSer 𝑅)) = (AlgSpan‘(𝐼 mPwSer 𝑅))
50		eqid 2739	. . . . . . . . . . . . 13 ⊢ (algSc‘(𝐼 mPwSer 𝑅)) = (algSc‘(𝐼 mPwSer 𝑅))
51		eqid 2739	. . . . . . . . . . . . 13 ⊢ (mrCls‘(SubRing‘(𝐼 mPwSer 𝑅))) = (mrCls‘(SubRing‘(𝐼 mPwSer 𝑅)))
52	49, 50, 51, 46	aspval2 21873	. . . . . . . . . . . 12 ⊢ (((𝐼 mPwSer 𝑅) ∈ AssAlg ∧ ran 𝑉 ⊆ (Base‘(𝐼 mPwSer 𝑅))) → ((AlgSpan‘(𝐼 mPwSer 𝑅))‘ran 𝑉) = ((mrCls‘(SubRing‘(𝐼 mPwSer 𝑅)))‘(ran (algSc‘(𝐼 mPwSer 𝑅)) ∪ ran 𝑉)))
53	45, 48, 52	syl2anc 590	. . . . . . . . . . 11 ⊢ (𝜑 → ((AlgSpan‘(𝐼 mPwSer 𝑅))‘ran 𝑉) = ((mrCls‘(SubRing‘(𝐼 mPwSer 𝑅)))‘(ran (algSc‘(𝐼 mPwSer 𝑅)) ∪ ran 𝑉)))
54	1, 44, 8, 49, 10, 11	mplbas2 22018	. . . . . . . . . . 11 ⊢ (𝜑 → ((AlgSpan‘(𝐼 mPwSer 𝑅))‘ran 𝑉) = (Base‘𝑃))
55	44, 1, 2, 10, 27	mplsubrg 21979	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (Base‘𝑃) ∈ (SubRing‘(𝐼 mPwSer 𝑅)))
56	1, 44, 2	mplval2 21970	. . . . . . . . . . . . . . . 16 ⊢ 𝑃 = ((𝐼 mPwSer 𝑅) ↾s (Base‘𝑃))
57	56	subsubrg2 20571	. . . . . . . . . . . . . . 15 ⊢ ((Base‘𝑃) ∈ (SubRing‘(𝐼 mPwSer 𝑅)) → (SubRing‘𝑃) = ((SubRing‘(𝐼 mPwSer 𝑅)) ∩ 𝒫 (Base‘𝑃)))
58	55, 57	syl 17	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (SubRing‘𝑃) = ((SubRing‘(𝐼 mPwSer 𝑅)) ∩ 𝒫 (Base‘𝑃)))
59	58	fveq2d 6831	. . . . . . . . . . . . 13 ⊢ (𝜑 → (mrCls‘(SubRing‘𝑃)) = (mrCls‘((SubRing‘(𝐼 mPwSer 𝑅)) ∩ 𝒫 (Base‘𝑃))))
60	50, 56	ressascl 21871	. . . . . . . . . . . . . . . . 17 ⊢ ((Base‘𝑃) ∈ (SubRing‘(𝐼 mPwSer 𝑅)) → (algSc‘(𝐼 mPwSer 𝑅)) = (algSc‘𝑃))
61	55, 60	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (algSc‘(𝐼 mPwSer 𝑅)) = (algSc‘𝑃))
62	15, 61	eqtr4id 2793	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝐴 = (algSc‘(𝐼 mPwSer 𝑅)))
63	62	rneqd 5880	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ran 𝐴 = ran (algSc‘(𝐼 mPwSer 𝑅)))
64	63	uneq1d 4097	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ran 𝐴 ∪ ran 𝑉) = (ran (algSc‘(𝐼 mPwSer 𝑅)) ∪ ran 𝑉))
65	59, 64	fveq12d 6834	. . . . . . . . . . . 12 ⊢ (𝜑 → ((mrCls‘(SubRing‘𝑃))‘(ran 𝐴 ∪ ran 𝑉)) = ((mrCls‘((SubRing‘(𝐼 mPwSer 𝑅)) ∩ 𝒫 (Base‘𝑃)))‘(ran (algSc‘(𝐼 mPwSer 𝑅)) ∪ ran 𝑉)))
66		assaring 21836	. . . . . . . . . . . . . 14 ⊢ ((𝐼 mPwSer 𝑅) ∈ AssAlg → (𝐼 mPwSer 𝑅) ∈ Ring)
67	46	subrgmre 20569	. . . . . . . . . . . . . 14 ⊢ ((𝐼 mPwSer 𝑅) ∈ Ring → (SubRing‘(𝐼 mPwSer 𝑅)) ∈ (Moore‘(Base‘(𝐼 mPwSer 𝑅))))
68	45, 66, 67	3syl 18	. . . . . . . . . . . . 13 ⊢ (𝜑 → (SubRing‘(𝐼 mPwSer 𝑅)) ∈ (Moore‘(Base‘(𝐼 mPwSer 𝑅))))
69	28	frnd 6663	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → ran 𝐴 ⊆ (Base‘𝑃))
70	63, 69	eqsstrrd 3950	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ran (algSc‘(𝐼 mPwSer 𝑅)) ⊆ (Base‘𝑃))
71	32	frnd 6663	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ran 𝑉 ⊆ (Base‘𝑃))
72	70, 71	unssd 4121	. . . . . . . . . . . . 13 ⊢ (𝜑 → (ran (algSc‘(𝐼 mPwSer 𝑅)) ∪ ran 𝑉) ⊆ (Base‘𝑃))
73		eqid 2739	. . . . . . . . . . . . . 14 ⊢ (mrCls‘((SubRing‘(𝐼 mPwSer 𝑅)) ∩ 𝒫 (Base‘𝑃))) = (mrCls‘((SubRing‘(𝐼 mPwSer 𝑅)) ∩ 𝒫 (Base‘𝑃)))
74	51, 73	submrc 17585	. . . . . . . . . . . . 13 ⊢ (((SubRing‘(𝐼 mPwSer 𝑅)) ∈ (Moore‘(Base‘(𝐼 mPwSer 𝑅))) ∧ (Base‘𝑃) ∈ (SubRing‘(𝐼 mPwSer 𝑅)) ∧ (ran (algSc‘(𝐼 mPwSer 𝑅)) ∪ ran 𝑉) ⊆ (Base‘𝑃)) → ((mrCls‘((SubRing‘(𝐼 mPwSer 𝑅)) ∩ 𝒫 (Base‘𝑃)))‘(ran (algSc‘(𝐼 mPwSer 𝑅)) ∪ ran 𝑉)) = ((mrCls‘(SubRing‘(𝐼 mPwSer 𝑅)))‘(ran (algSc‘(𝐼 mPwSer 𝑅)) ∪ ran 𝑉)))
75	68, 55, 72, 74	syl3anc 1379	. . . . . . . . . . . 12 ⊢ (𝜑 → ((mrCls‘((SubRing‘(𝐼 mPwSer 𝑅)) ∩ 𝒫 (Base‘𝑃)))‘(ran (algSc‘(𝐼 mPwSer 𝑅)) ∪ ran 𝑉)) = ((mrCls‘(SubRing‘(𝐼 mPwSer 𝑅)))‘(ran (algSc‘(𝐼 mPwSer 𝑅)) ∪ ran 𝑉)))
76	65, 75	eqtr2d 2775	. . . . . . . . . . 11 ⊢ (𝜑 → ((mrCls‘(SubRing‘(𝐼 mPwSer 𝑅)))‘(ran (algSc‘(𝐼 mPwSer 𝑅)) ∪ ran 𝑉)) = ((mrCls‘(SubRing‘𝑃))‘(ran 𝐴 ∪ ran 𝑉)))
77	53, 54, 76	3eqtr3d 2782	. . . . . . . . . 10 ⊢ (𝜑 → (Base‘𝑃) = ((mrCls‘(SubRing‘𝑃))‘(ran 𝐴 ∪ ran 𝑉)))
78	77	ad2antrr 732	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) ∧ (ran 𝐴 ∪ ran 𝑉) ⊆ dom (𝑚 ∩ 𝑛)) → (Base‘𝑃) = ((mrCls‘(SubRing‘𝑃))‘(ran 𝐴 ∪ ran 𝑉)))
79	1, 10, 27	mplringd 21997	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝑃 ∈ Ring)
80	2	subrgmre 20569	. . . . . . . . . . . 12 ⊢ (𝑃 ∈ Ring → (SubRing‘𝑃) ∈ (Moore‘(Base‘𝑃)))
81	79, 80	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (SubRing‘𝑃) ∈ (Moore‘(Base‘𝑃)))
82	81	ad2antrr 732	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) ∧ (ran 𝐴 ∪ ran 𝑉) ⊆ dom (𝑚 ∩ 𝑛)) → (SubRing‘𝑃) ∈ (Moore‘(Base‘𝑃)))
83		simpr 485	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) ∧ (ran 𝐴 ∪ ran 𝑉) ⊆ dom (𝑚 ∩ 𝑛)) → (ran 𝐴 ∪ ran 𝑉) ⊆ dom (𝑚 ∩ 𝑛))
84		rhmeql 20575	. . . . . . . . . . 11 ⊢ ((𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆)) → dom (𝑚 ∩ 𝑛) ∈ (SubRing‘𝑃))
85	84	ad2antlr 733	. . . . . . . . . 10 ⊢ (((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) ∧ (ran 𝐴 ∪ ran 𝑉) ⊆ dom (𝑚 ∩ 𝑛)) → dom (𝑚 ∩ 𝑛) ∈ (SubRing‘𝑃))
86		eqid 2739	. . . . . . . . . . 11 ⊢ (mrCls‘(SubRing‘𝑃)) = (mrCls‘(SubRing‘𝑃))
87	86	mrcsscl 17577	. . . . . . . . . 10 ⊢ (((SubRing‘𝑃) ∈ (Moore‘(Base‘𝑃)) ∧ (ran 𝐴 ∪ ran 𝑉) ⊆ dom (𝑚 ∩ 𝑛) ∧ dom (𝑚 ∩ 𝑛) ∈ (SubRing‘𝑃)) → ((mrCls‘(SubRing‘𝑃))‘(ran 𝐴 ∪ ran 𝑉)) ⊆ dom (𝑚 ∩ 𝑛))
88	82, 83, 85, 87	syl3anc 1379	. . . . . . . . 9 ⊢ (((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) ∧ (ran 𝐴 ∪ ran 𝑉) ⊆ dom (𝑚 ∩ 𝑛)) → ((mrCls‘(SubRing‘𝑃))‘(ran 𝐴 ∪ ran 𝑉)) ⊆ dom (𝑚 ∩ 𝑛))
89	78, 88	eqsstrd 3949	. . . . . . . 8 ⊢ (((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) ∧ (ran 𝐴 ∪ ran 𝑉) ⊆ dom (𝑚 ∩ 𝑛)) → (Base‘𝑃) ⊆ dom (𝑚 ∩ 𝑛))
90	89	ex 413	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) → ((ran 𝐴 ∪ ran 𝑉) ⊆ dom (𝑚 ∩ 𝑛) → (Base‘𝑃) ⊆ dom (𝑚 ∩ 𝑛)))
91		simprl 776	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) → 𝑚 ∈ (𝑃 RingHom 𝑆))
92	2, 3	rhmf 20455	. . . . . . . . 9 ⊢ (𝑚 ∈ (𝑃 RingHom 𝑆) → 𝑚:(Base‘𝑃)⟶𝐶)
93		ffn 6655	. . . . . . . . 9 ⊢ (𝑚:(Base‘𝑃)⟶𝐶 → 𝑚 Fn (Base‘𝑃))
94	91, 92, 93	3syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) → 𝑚 Fn (Base‘𝑃))
95		simprr 778	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) → 𝑛 ∈ (𝑃 RingHom 𝑆))
96	2, 3	rhmf 20455	. . . . . . . . 9 ⊢ (𝑛 ∈ (𝑃 RingHom 𝑆) → 𝑛:(Base‘𝑃)⟶𝐶)
97		ffn 6655	. . . . . . . . 9 ⊢ (𝑛:(Base‘𝑃)⟶𝐶 → 𝑛 Fn (Base‘𝑃))
98	95, 96, 97	3syl 18	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) → 𝑛 Fn (Base‘𝑃))
99	69	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) → ran 𝐴 ⊆ (Base‘𝑃))
100	71	adantr 481	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) → ran 𝑉 ⊆ (Base‘𝑃))
101	99, 100	unssd 4121	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) → (ran 𝐴 ∪ ran 𝑉) ⊆ (Base‘𝑃))
102		fnreseql 6989	. . . . . . . 8 ⊢ ((𝑚 Fn (Base‘𝑃) ∧ 𝑛 Fn (Base‘𝑃) ∧ (ran 𝐴 ∪ ran 𝑉) ⊆ (Base‘𝑃)) → ((𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = (𝑛 ↾ (ran 𝐴 ∪ ran 𝑉)) ↔ (ran 𝐴 ∪ ran 𝑉) ⊆ dom (𝑚 ∩ 𝑛)))
103	94, 98, 101, 102	syl3anc 1379	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) → ((𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = (𝑛 ↾ (ran 𝐴 ∪ ran 𝑉)) ↔ (ran 𝐴 ∪ ran 𝑉) ⊆ dom (𝑚 ∩ 𝑛)))
104		fneqeql2 6988	. . . . . . . 8 ⊢ ((𝑚 Fn (Base‘𝑃) ∧ 𝑛 Fn (Base‘𝑃)) → (𝑚 = 𝑛 ↔ (Base‘𝑃) ⊆ dom (𝑚 ∩ 𝑛)))
105	94, 98, 104	syl2anc 590	. . . . . . 7 ⊢ ((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) → (𝑚 = 𝑛 ↔ (Base‘𝑃) ⊆ dom (𝑚 ∩ 𝑛)))
106	90, 103, 105	3imtr4d 295	. . . . . 6 ⊢ ((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) → ((𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = (𝑛 ↾ (ran 𝐴 ∪ ran 𝑉)) → 𝑚 = 𝑛))
107	43, 106	syl5 34	. . . . 5 ⊢ ((𝜑 ∧ (𝑚 ∈ (𝑃 RingHom 𝑆) ∧ 𝑛 ∈ (𝑃 RingHom 𝑆))) → (((𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉)) ∧ (𝑛 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉))) → 𝑚 = 𝑛))
108	107	ralrimivva 3182	. . . 4 ⊢ (𝜑 → ∀𝑚 ∈ (𝑃 RingHom 𝑆)∀𝑛 ∈ (𝑃 RingHom 𝑆)(((𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉)) ∧ (𝑛 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉))) → 𝑚 = 𝑛))
109		reseq1 5925	. . . . . 6 ⊢ (𝑚 = 𝑛 → (𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = (𝑛 ↾ (ran 𝐴 ∪ ran 𝑉)))
110	109	eqeq1d 2741	. . . . 5 ⊢ (𝑚 = 𝑛 → ((𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉)) ↔ (𝑛 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉))))
111	110	rmo4 3671	. . . 4 ⊢ (∃*𝑚 ∈ (𝑃 RingHom 𝑆)(𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉)) ↔ ∀𝑚 ∈ (𝑃 RingHom 𝑆)∀𝑛 ∈ (𝑃 RingHom 𝑆)(((𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉)) ∧ (𝑛 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉))) → 𝑚 = 𝑛))
112	108, 111	sylibr 235	. . 3 ⊢ (𝜑 → ∃*𝑚 ∈ (𝑃 RingHom 𝑆)(𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉)))
113		rmoim 3681	. . 3 ⊢ (∀𝑚 ∈ (𝑃 RingHom 𝑆)(((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺) → (𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉))) → (∃*𝑚 ∈ (𝑃 RingHom 𝑆)(𝑚 ↾ (ran 𝐴 ∪ ran 𝑉)) = ((𝐹 ∘ ◡𝐴) ∪ (𝐺 ∘ ◡𝑉)) → ∃*𝑚 ∈ (𝑃 RingHom 𝑆)((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺)))
114	42, 112, 113	sylc 65	. 2 ⊢ (𝜑 → ∃*𝑚 ∈ (𝑃 RingHom 𝑆)((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺))
115		reu5 3346	. 2 ⊢ (∃!𝑚 ∈ (𝑃 RingHom 𝑆)((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺) ↔ (∃𝑚 ∈ (𝑃 RingHom 𝑆)((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺) ∧ ∃*𝑚 ∈ (𝑃 RingHom 𝑆)((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺)))
116	24, 114, 115	sylanbrc 589	1 ⊢ (𝜑 → ∃!𝑚 ∈ (𝑃 RingHom 𝑆)((𝑚 ∘ 𝐴) = 𝐹 ∧ (𝑚 ∘ 𝑉) = 𝐺))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   ∧ w3a 1092   = wceq 1547   ∈ wcel 2119  ∀wral 3053  ∃wrex 3063  ∃!wreu 3342  ∃*wrmo 3343  {crab 3391   ∪ cun 3881   ∩ cin 3882   ⊆ wss 3883  𝒫 cpw 4529   ↦ cmpt 5153  ^◡ccnv 5617  dom cdm 5618  ran crn 5619   ↾ cres 5620   “ cima 5621   ∘ ccom 5622  Fun wfun 6479   Fn wfn 6480  ⟶wf 6481  ‘cfv 6485  (class class class)co 7356   ∘_f cof 7618   ↑_m cmap 8763  Fincfn 8883  ℕcn 12165  ℕ₀cn0 12428  Basecbs 17170  ._rcmulr 17212   Σ_g cgsu 17394  Moorecmre 17535  mrClscmrc 17536  ._gcmg 19034  mulGrpcmgp 20112  Ringcrg 20205  CRingccrg 20206   RingHom crh 20440  SubRingcsubrg 20541  AssAlgcasa 21825  AlgSpancasp 21826  algSccascl 21827   mPwSer cmps 21879   mVar cmvr 21880   mPoly cmpl 21881

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2711  ax-rep 5199  ax-sep 5218  ax-nul 5228  ax-pow 5294  ax-pr 5362  ax-un 7678  ax-cnex 11085  ax-resscn 11086  ax-1cn 11087  ax-icn 11088  ax-addcl 11089  ax-addrcl 11090  ax-mulcl 11091  ax-mulrcl 11092  ax-mulcom 11093  ax-addass 11094  ax-mulass 11095  ax-distr 11096  ax-i2m1 11097  ax-1ne0 11098  ax-1rid 11099  ax-rnegex 11100  ax-rrecex 11101  ax-cnre 11102  ax-pre-lttri 11103  ax-pre-lttrn 11104  ax-pre-ltadd 11105  ax-pre-mulgt0 11106

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3or 1093  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2718  df-cleq 2731  df-clel 2814  df-nfc 2888  df-ne 2935  df-nel 3039  df-ral 3054  df-rex 3064  df-rmo 3344  df-reu 3345  df-rab 3392  df-v 3433  df-sbc 3724  df-csb 3832  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-pss 3903  df-nul 4262  df-if 4455  df-pw 4531  df-sn 4556  df-pr 4558  df-tp 4560  df-op 4562  df-uni 4839  df-int 4878  df-iun 4923  df-iin 4924  df-br 5073  df-opab 5135  df-mpt 5154  df-tr 5180  df-id 5513  df-eprel 5518  df-po 5526  df-so 5527  df-fr 5571  df-se 5572  df-we 5573  df-xp 5624  df-rel 5625  df-cnv 5626  df-co 5627  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631  df-pred 6252  df-ord 6313  df-on 6314  df-lim 6315  df-suc 6316  df-iota 6441  df-fun 6487  df-fn 6488  df-f 6489  df-f1 6490  df-fo 6491  df-f1o 6492  df-fv 6493  df-isom 6494  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-of 7620  df-ofr 7621  df-om 7807  df-1st 7931  df-2nd 7932  df-supp 8101  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-1o 8395  df-2o 8396  df-er 8633  df-map 8765  df-pm 8766  df-ixp 8836  df-en 8884  df-dom 8885  df-sdom 8886  df-fin 8887  df-fsupp 9265  df-sup 9345  df-oi 9415  df-card 9854  df-pnf 11172  df-mnf 11173  df-xr 11174  df-ltxr 11175  df-le 11176  df-sub 11370  df-neg 11371  df-nn 12166  df-2 12235  df-3 12236  df-4 12237  df-5 12238  df-6 12239  df-7 12240  df-8 12241  df-9 12242  df-n0 12429  df-z 12516  df-dec 12636  df-uz 12780  df-fz 13453  df-fzo 13600  df-seq 13955  df-hash 14284  df-struct 17108  df-sets 17125  df-slot 17143  df-ndx 17155  df-base 17171  df-ress 17192  df-plusg 17224  df-mulr 17225  df-sca 17227  df-vsca 17228  df-ip 17229  df-tset 17230  df-ple 17231  df-ds 17233  df-hom 17235  df-cco 17236  df-0g 17395  df-gsum 17396  df-prds 17401  df-pws 17403  df-mre 17539  df-mrc 17540  df-acs 17542  df-mgm 18599  df-sgrp 18678  df-mnd 18694  df-mhm 18742  df-submnd 18743  df-grp 18903  df-minusg 18904  df-sbg 18905  df-mulg 19035  df-subg 19090  df-ghm 19179  df-cntz 19283  df-cmn 19748  df-abl 19749  df-mgp 20113  df-rng 20125  df-ur 20154  df-srg 20159  df-ring 20207  df-cring 20208  df-rhm 20443  df-subrng 20518  df-subrg 20542  df-lmod 20852  df-lss 20922  df-lsp 20962  df-assa 21828  df-asp 21829  df-ascl 21830  df-psr 21884  df-mvr 21885  df-mpl 21886

This theorem is referenced by:  evlsval2  22063  evlsval3  22065