mplind - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > mplind		Structured version Visualization version GIF version

Theorem mplind 21993

Description: Prove a property of polynomials by "structural" induction, under a simplified model of structure which loses the sum of products structure. The commutativity condition is stronger than strictly needed. (Contributed by Stefan O'Rear, 11-Mar-2015.)

**Hypotheses**
Ref	Expression
mplind.sk	⊢ 𝐾 = (Base‘𝑅)
mplind.sv	⊢ 𝑉 = (𝐼 mVar 𝑅)
mplind.sy	⊢ 𝑌 = (𝐼 mPoly 𝑅)
mplind.sp	⊢ + = (+_g‘𝑌)
mplind.st	⊢ · = (._r‘𝑌)
mplind.sc	⊢ 𝐶 = (algSc‘𝑌)
mplind.sb	⊢ 𝐵 = (Base‘𝑌)
mplind.p	⊢ ((𝜑 ∧ (𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻)) → (𝑥 + 𝑦) ∈ 𝐻)
mplind.t	⊢ ((𝜑 ∧ (𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻)) → (𝑥 · 𝑦) ∈ 𝐻)
mplind.s	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → (𝐶‘𝑥) ∈ 𝐻)
mplind.v	⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑉‘𝑥) ∈ 𝐻)
mplind.x	⊢ (𝜑 → 𝑋 ∈ 𝐵)
mplind.i	⊢ (𝜑 → 𝐼 ∈ 𝑊)
mplind.r	⊢ (𝜑 → 𝑅 ∈ CRing)

**Assertion**
Ref	Expression
mplind	⊢ (𝜑 → 𝑋 ∈ 𝐻)

Distinct variable groups: 𝑥,𝑦, + 𝑥,𝐵,𝑦 𝑥,𝐶,𝑦 𝑥,𝐼 𝜑,𝑥,𝑦 𝑥,𝐻,𝑦 𝑥,𝐾 𝑥, · ,𝑦 𝑥,𝑉 𝑥,𝑌,𝑦 Allowed substitution hints: 𝑅(𝑥,𝑦) 𝐼(𝑦) 𝐾(𝑦) 𝑉(𝑦) 𝑊(𝑥,𝑦) 𝑋(𝑥,𝑦)

Proof of Theorem mplind Dummy variables 𝑤 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2729	. . . . . 6 ⊢ (𝐼 mPwSer 𝑅) = (𝐼 mPwSer 𝑅)
2		mplind.i	. . . . . 6 ⊢ (𝜑 → 𝐼 ∈ 𝑊)
3		mplind.r	. . . . . 6 ⊢ (𝜑 → 𝑅 ∈ CRing)
4	1, 2, 3	psrassa 21898	. . . . 5 ⊢ (𝜑 → (𝐼 mPwSer 𝑅) ∈ AssAlg)
5		inss2 4191	. . . . . 6 ⊢ (𝐻 ∩ 𝐵) ⊆ 𝐵
6		mplind.sy	. . . . . . . 8 ⊢ 𝑌 = (𝐼 mPoly 𝑅)
7		mplind.sb	. . . . . . . 8 ⊢ 𝐵 = (Base‘𝑌)
8		crngring 20148	. . . . . . . . 9 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)
9	3, 8	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ Ring)
10	1, 6, 7, 2, 9	mplsubrg 21930	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ (SubRing‘(𝐼 mPwSer 𝑅)))
11		eqid 2729	. . . . . . . 8 ⊢ (Base‘(𝐼 mPwSer 𝑅)) = (Base‘(𝐼 mPwSer 𝑅))
12	11	subrgss 20475	. . . . . . 7 ⊢ (𝐵 ∈ (SubRing‘(𝐼 mPwSer 𝑅)) → 𝐵 ⊆ (Base‘(𝐼 mPwSer 𝑅)))
13	10, 12	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐵 ⊆ (Base‘(𝐼 mPwSer 𝑅)))
14	5, 13	sstrid 3949	. . . . 5 ⊢ (𝜑 → (𝐻 ∩ 𝐵) ⊆ (Base‘(𝐼 mPwSer 𝑅)))
15		mplind.sv	. . . . . . . . 9 ⊢ 𝑉 = (𝐼 mVar 𝑅)
16	6, 15, 7, 2, 9	mvrf2 21918	. . . . . . . 8 ⊢ (𝜑 → 𝑉:𝐼⟶𝐵)
17	16	ffnd 6657	. . . . . . 7 ⊢ (𝜑 → 𝑉 Fn 𝐼)
18		mplind.v	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑉‘𝑥) ∈ 𝐻)
19	18	ralrimiva 3121	. . . . . . 7 ⊢ (𝜑 → ∀𝑥 ∈ 𝐼 (𝑉‘𝑥) ∈ 𝐻)
20		fnfvrnss 7059	. . . . . . 7 ⊢ ((𝑉 Fn 𝐼 ∧ ∀𝑥 ∈ 𝐼 (𝑉‘𝑥) ∈ 𝐻) → ran 𝑉 ⊆ 𝐻)
21	17, 19, 20	syl2anc 584	. . . . . 6 ⊢ (𝜑 → ran 𝑉 ⊆ 𝐻)
22	16	frnd 6664	. . . . . 6 ⊢ (𝜑 → ran 𝑉 ⊆ 𝐵)
23	21, 22	ssind 4194	. . . . 5 ⊢ (𝜑 → ran 𝑉 ⊆ (𝐻 ∩ 𝐵))
24		eqid 2729	. . . . . 6 ⊢ (AlgSpan‘(𝐼 mPwSer 𝑅)) = (AlgSpan‘(𝐼 mPwSer 𝑅))
25	24, 11	aspss 21802	. . . . 5 ⊢ (((𝐼 mPwSer 𝑅) ∈ AssAlg ∧ (𝐻 ∩ 𝐵) ⊆ (Base‘(𝐼 mPwSer 𝑅)) ∧ ran 𝑉 ⊆ (𝐻 ∩ 𝐵)) → ((AlgSpan‘(𝐼 mPwSer 𝑅))‘ran 𝑉) ⊆ ((AlgSpan‘(𝐼 mPwSer 𝑅))‘(𝐻 ∩ 𝐵)))
26	4, 14, 23, 25	syl3anc 1373	. . . 4 ⊢ (𝜑 → ((AlgSpan‘(𝐼 mPwSer 𝑅))‘ran 𝑉) ⊆ ((AlgSpan‘(𝐼 mPwSer 𝑅))‘(𝐻 ∩ 𝐵)))
27	6, 1, 15, 24, 2, 3	mplbas2 21965	. . . . 5 ⊢ (𝜑 → ((AlgSpan‘(𝐼 mPwSer 𝑅))‘ran 𝑉) = (Base‘𝑌))
28	27, 7	eqtr4di 2782	. . . 4 ⊢ (𝜑 → ((AlgSpan‘(𝐼 mPwSer 𝑅))‘ran 𝑉) = 𝐵)
29	5	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (𝐻 ∩ 𝐵) ⊆ 𝐵)
30	6	mplassa 21947	. . . . . . . . . . . . . 14 ⊢ ((𝐼 ∈ 𝑊 ∧ 𝑅 ∈ CRing) → 𝑌 ∈ AssAlg)
31	2, 3, 30	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑌 ∈ AssAlg)
32		mplind.sc	. . . . . . . . . . . . . 14 ⊢ 𝐶 = (algSc‘𝑌)
33		eqid 2729	. . . . . . . . . . . . . 14 ⊢ (Scalar‘𝑌) = (Scalar‘𝑌)
34	32, 33	asclrhm 21815	. . . . . . . . . . . . 13 ⊢ (𝑌 ∈ AssAlg → 𝐶 ∈ ((Scalar‘𝑌) RingHom 𝑌))
35	31, 34	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ∈ ((Scalar‘𝑌) RingHom 𝑌))
36		eqid 2729	. . . . . . . . . . . . 13 ⊢ (1_r‘(Scalar‘𝑌)) = (1_r‘(Scalar‘𝑌))
37		eqid 2729	. . . . . . . . . . . . 13 ⊢ (1_r‘𝑌) = (1_r‘𝑌)
38	36, 37	rhm1 20392	. . . . . . . . . . . 12 ⊢ (𝐶 ∈ ((Scalar‘𝑌) RingHom 𝑌) → (𝐶‘(1_r‘(Scalar‘𝑌))) = (1_r‘𝑌))
39	35, 38	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶‘(1_r‘(Scalar‘𝑌))) = (1_r‘𝑌))
40		fveq2 6826	. . . . . . . . . . . . 13 ⊢ (𝑥 = (1_r‘(Scalar‘𝑌)) → (𝐶‘𝑥) = (𝐶‘(1_r‘(Scalar‘𝑌))))
41	40	eleq1d 2813	. . . . . . . . . . . 12 ⊢ (𝑥 = (1_r‘(Scalar‘𝑌)) → ((𝐶‘𝑥) ∈ 𝐻 ↔ (𝐶‘(1_r‘(Scalar‘𝑌))) ∈ 𝐻))
42		mplind.s	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → (𝐶‘𝑥) ∈ 𝐻)
43	42	ralrimiva 3121	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑥 ∈ 𝐾 (𝐶‘𝑥) ∈ 𝐻)
44	6, 2, 3	mplsca 21938	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑅 = (Scalar‘𝑌))
45	44, 9	eqeltrrd 2829	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (Scalar‘𝑌) ∈ Ring)
46		eqid 2729	. . . . . . . . . . . . . . 15 ⊢ (Base‘(Scalar‘𝑌)) = (Base‘(Scalar‘𝑌))
47	46, 36	ringidcl 20168	. . . . . . . . . . . . . 14 ⊢ ((Scalar‘𝑌) ∈ Ring → (1_r‘(Scalar‘𝑌)) ∈ (Base‘(Scalar‘𝑌)))
48	45, 47	syl 17	. . . . . . . . . . . . 13 ⊢ (𝜑 → (1_r‘(Scalar‘𝑌)) ∈ (Base‘(Scalar‘𝑌)))
49		mplind.sk	. . . . . . . . . . . . . 14 ⊢ 𝐾 = (Base‘𝑅)
50	44	fveq2d 6830	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (Base‘𝑅) = (Base‘(Scalar‘𝑌)))
51	49, 50	eqtrid 2776	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐾 = (Base‘(Scalar‘𝑌)))
52	48, 51	eleqtrrd 2831	. . . . . . . . . . . 12 ⊢ (𝜑 → (1_r‘(Scalar‘𝑌)) ∈ 𝐾)
53	41, 43, 52	rspcdva 3580	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶‘(1_r‘(Scalar‘𝑌))) ∈ 𝐻)
54	39, 53	eqeltrrd 2829	. . . . . . . . . 10 ⊢ (𝜑 → (1_r‘𝑌) ∈ 𝐻)
55		assaring 21786	. . . . . . . . . . . 12 ⊢ (𝑌 ∈ AssAlg → 𝑌 ∈ Ring)
56	31, 55	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑌 ∈ Ring)
57	7, 37	ringidcl 20168	. . . . . . . . . . 11 ⊢ (𝑌 ∈ Ring → (1_r‘𝑌) ∈ 𝐵)
58	56, 57	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (1_r‘𝑌) ∈ 𝐵)
59	54, 58	elind 4153	. . . . . . . . 9 ⊢ (𝜑 → (1_r‘𝑌) ∈ (𝐻 ∩ 𝐵))
60	59	ne0d 4295	. . . . . . . 8 ⊢ (𝜑 → (𝐻 ∩ 𝐵) ≠ ∅)
61		elinel1 4154	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ (𝐻 ∩ 𝐵) → 𝑧 ∈ 𝐻)
62		elinel1 4154	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ (𝐻 ∩ 𝐵) → 𝑤 ∈ 𝐻)
63	61, 62	anim12i 613	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ (𝐻 ∩ 𝐵) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵)) → (𝑧 ∈ 𝐻 ∧ 𝑤 ∈ 𝐻))
64		mplind.p	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻)) → (𝑥 + 𝑦) ∈ 𝐻)
65	64	caovclg 7545	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐻 ∧ 𝑤 ∈ 𝐻)) → (𝑧 + 𝑤) ∈ 𝐻)
66	63, 65	sylan2 593	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐻 ∩ 𝐵) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → (𝑧 + 𝑤) ∈ 𝐻)
67		assalmod 21785	. . . . . . . . . . . . . . . . 17 ⊢ (𝑌 ∈ AssAlg → 𝑌 ∈ LMod)
68	31, 67	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑌 ∈ LMod)
69		lmodgrp 20788	. . . . . . . . . . . . . . . 16 ⊢ (𝑌 ∈ LMod → 𝑌 ∈ Grp)
70	68, 69	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑌 ∈ Grp)
71	70	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐻 ∩ 𝐵) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → 𝑌 ∈ Grp)
72		simprl 770	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐻 ∩ 𝐵) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → 𝑧 ∈ (𝐻 ∩ 𝐵))
73	72	elin2d 4158	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐻 ∩ 𝐵) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → 𝑧 ∈ 𝐵)
74		simprr 772	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐻 ∩ 𝐵) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → 𝑤 ∈ (𝐻 ∩ 𝐵))
75	74	elin2d 4158	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐻 ∩ 𝐵) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → 𝑤 ∈ 𝐵)
76		mplind.sp	. . . . . . . . . . . . . . 15 ⊢ + = (+_g‘𝑌)
77	7, 76	grpcl 18838	. . . . . . . . . . . . . 14 ⊢ ((𝑌 ∈ Grp ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) → (𝑧 + 𝑤) ∈ 𝐵)
78	71, 73, 75, 77	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐻 ∩ 𝐵) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → (𝑧 + 𝑤) ∈ 𝐵)
79	66, 78	elind 4153	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐻 ∩ 𝐵) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → (𝑧 + 𝑤) ∈ (𝐻 ∩ 𝐵))
80	79	anassrs 467	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵)) → (𝑧 + 𝑤) ∈ (𝐻 ∩ 𝐵))
81	80	ralrimiva 3121	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) → ∀𝑤 ∈ (𝐻 ∩ 𝐵)(𝑧 + 𝑤) ∈ (𝐻 ∩ 𝐵))
82		mplind.st	. . . . . . . . . . . . 13 ⊢ · = (._r‘𝑌)
83		eqid 2729	. . . . . . . . . . . . 13 ⊢ (inv_g‘𝑌) = (inv_g‘𝑌)
84	56	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) → 𝑌 ∈ Ring)
85		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) → 𝑧 ∈ (𝐻 ∩ 𝐵))
86	85	elin2d 4158	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) → 𝑧 ∈ 𝐵)
87	7, 82, 37, 83, 84, 86	ringnegl 20205	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) → (((inv_g‘𝑌)‘(1_r‘𝑌)) · 𝑧) = ((inv_g‘𝑌)‘𝑧))
88		simpl 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) → 𝜑)
89		rhmghm 20387	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐶 ∈ ((Scalar‘𝑌) RingHom 𝑌) → 𝐶 ∈ ((Scalar‘𝑌) GrpHom 𝑌))
90	35, 89	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐶 ∈ ((Scalar‘𝑌) GrpHom 𝑌))
91		eqid 2729	. . . . . . . . . . . . . . . . . 18 ⊢ (inv_g‘(Scalar‘𝑌)) = (inv_g‘(Scalar‘𝑌))
92	46, 91, 83	ghminv 19120	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐶 ∈ ((Scalar‘𝑌) GrpHom 𝑌) ∧ (1_r‘(Scalar‘𝑌)) ∈ (Base‘(Scalar‘𝑌))) → (𝐶‘((inv_g‘(Scalar‘𝑌))‘(1_r‘(Scalar‘𝑌)))) = ((inv_g‘𝑌)‘(𝐶‘(1_r‘(Scalar‘𝑌)))))
93	90, 48, 92	syl2anc 584	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → (𝐶‘((inv_g‘(Scalar‘𝑌))‘(1_r‘(Scalar‘𝑌)))) = ((inv_g‘𝑌)‘(𝐶‘(1_r‘(Scalar‘𝑌)))))
94	39	fveq2d 6830	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((inv_g‘𝑌)‘(𝐶‘(1_r‘(Scalar‘𝑌)))) = ((inv_g‘𝑌)‘(1_r‘𝑌)))
95	93, 94	eqtrd 2764	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐶‘((inv_g‘(Scalar‘𝑌))‘(1_r‘(Scalar‘𝑌)))) = ((inv_g‘𝑌)‘(1_r‘𝑌)))
96		fveq2 6826	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = ((inv_g‘(Scalar‘𝑌))‘(1_r‘(Scalar‘𝑌))) → (𝐶‘𝑥) = (𝐶‘((inv_g‘(Scalar‘𝑌))‘(1_r‘(Scalar‘𝑌)))))
97	96	eleq1d 2813	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = ((inv_g‘(Scalar‘𝑌))‘(1_r‘(Scalar‘𝑌))) → ((𝐶‘𝑥) ∈ 𝐻 ↔ (𝐶‘((inv_g‘(Scalar‘𝑌))‘(1_r‘(Scalar‘𝑌)))) ∈ 𝐻))
98		ringgrp 20141	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Scalar‘𝑌) ∈ Ring → (Scalar‘𝑌) ∈ Grp)
99	45, 98	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (Scalar‘𝑌) ∈ Grp)
100	46, 91	grpinvcl 18884	. . . . . . . . . . . . . . . . . 18 ⊢ (((Scalar‘𝑌) ∈ Grp ∧ (1_r‘(Scalar‘𝑌)) ∈ (Base‘(Scalar‘𝑌))) → ((inv_g‘(Scalar‘𝑌))‘(1_r‘(Scalar‘𝑌))) ∈ (Base‘(Scalar‘𝑌)))
101	99, 48, 100	syl2anc 584	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → ((inv_g‘(Scalar‘𝑌))‘(1_r‘(Scalar‘𝑌))) ∈ (Base‘(Scalar‘𝑌)))
102	101, 51	eleqtrrd 2831	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((inv_g‘(Scalar‘𝑌))‘(1_r‘(Scalar‘𝑌))) ∈ 𝐾)
103	97, 43, 102	rspcdva 3580	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐶‘((inv_g‘(Scalar‘𝑌))‘(1_r‘(Scalar‘𝑌)))) ∈ 𝐻)
104	95, 103	eqeltrrd 2829	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((inv_g‘𝑌)‘(1_r‘𝑌)) ∈ 𝐻)
105	104	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) → ((inv_g‘𝑌)‘(1_r‘𝑌)) ∈ 𝐻)
106	85	elin1d 4157	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) → 𝑧 ∈ 𝐻)
107		mplind.t	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻)) → (𝑥 · 𝑦) ∈ 𝐻)
108	107	caovclg 7545	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (((inv_g‘𝑌)‘(1_r‘𝑌)) ∈ 𝐻 ∧ 𝑧 ∈ 𝐻)) → (((inv_g‘𝑌)‘(1_r‘𝑌)) · 𝑧) ∈ 𝐻)
109	88, 105, 106, 108	syl12anc 836	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) → (((inv_g‘𝑌)‘(1_r‘𝑌)) · 𝑧) ∈ 𝐻)
110	87, 109	eqeltrrd 2829	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) → ((inv_g‘𝑌)‘𝑧) ∈ 𝐻)
111	70	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) → 𝑌 ∈ Grp)
112	7, 83	grpinvcl 18884	. . . . . . . . . . . 12 ⊢ ((𝑌 ∈ Grp ∧ 𝑧 ∈ 𝐵) → ((inv_g‘𝑌)‘𝑧) ∈ 𝐵)
113	111, 86, 112	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) → ((inv_g‘𝑌)‘𝑧) ∈ 𝐵)
114	110, 113	elind 4153	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) → ((inv_g‘𝑌)‘𝑧) ∈ (𝐻 ∩ 𝐵))
115	81, 114	jca 511	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) → (∀𝑤 ∈ (𝐻 ∩ 𝐵)(𝑧 + 𝑤) ∈ (𝐻 ∩ 𝐵) ∧ ((inv_g‘𝑌)‘𝑧) ∈ (𝐻 ∩ 𝐵)))
116	115	ralrimiva 3121	. . . . . . . 8 ⊢ (𝜑 → ∀𝑧 ∈ (𝐻 ∩ 𝐵)(∀𝑤 ∈ (𝐻 ∩ 𝐵)(𝑧 + 𝑤) ∈ (𝐻 ∩ 𝐵) ∧ ((inv_g‘𝑌)‘𝑧) ∈ (𝐻 ∩ 𝐵)))
117	7, 76, 83	issubg2 19038	. . . . . . . . 9 ⊢ (𝑌 ∈ Grp → ((𝐻 ∩ 𝐵) ∈ (SubGrp‘𝑌) ↔ ((𝐻 ∩ 𝐵) ⊆ 𝐵 ∧ (𝐻 ∩ 𝐵) ≠ ∅ ∧ ∀𝑧 ∈ (𝐻 ∩ 𝐵)(∀𝑤 ∈ (𝐻 ∩ 𝐵)(𝑧 + 𝑤) ∈ (𝐻 ∩ 𝐵) ∧ ((inv_g‘𝑌)‘𝑧) ∈ (𝐻 ∩ 𝐵)))))
118	70, 117	syl 17	. . . . . . . 8 ⊢ (𝜑 → ((𝐻 ∩ 𝐵) ∈ (SubGrp‘𝑌) ↔ ((𝐻 ∩ 𝐵) ⊆ 𝐵 ∧ (𝐻 ∩ 𝐵) ≠ ∅ ∧ ∀𝑧 ∈ (𝐻 ∩ 𝐵)(∀𝑤 ∈ (𝐻 ∩ 𝐵)(𝑧 + 𝑤) ∈ (𝐻 ∩ 𝐵) ∧ ((inv_g‘𝑌)‘𝑧) ∈ (𝐻 ∩ 𝐵)))))
119	29, 60, 116, 118	mpbir3and 1343	. . . . . . 7 ⊢ (𝜑 → (𝐻 ∩ 𝐵) ∈ (SubGrp‘𝑌))
120		elinel1 4154	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (𝐻 ∩ 𝐵) → 𝑥 ∈ 𝐻)
121		elinel1 4154	. . . . . . . . . . 11 ⊢ (𝑦 ∈ (𝐻 ∩ 𝐵) → 𝑦 ∈ 𝐻)
122	120, 121	anim12i 613	. . . . . . . . . 10 ⊢ ((𝑥 ∈ (𝐻 ∩ 𝐵) ∧ 𝑦 ∈ (𝐻 ∩ 𝐵)) → (𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻))
123	122, 107	sylan2 593	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (𝐻 ∩ 𝐵) ∧ 𝑦 ∈ (𝐻 ∩ 𝐵))) → (𝑥 · 𝑦) ∈ 𝐻)
124	56	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (𝐻 ∩ 𝐵) ∧ 𝑦 ∈ (𝐻 ∩ 𝐵))) → 𝑌 ∈ Ring)
125		simprl 770	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (𝐻 ∩ 𝐵) ∧ 𝑦 ∈ (𝐻 ∩ 𝐵))) → 𝑥 ∈ (𝐻 ∩ 𝐵))
126	125	elin2d 4158	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (𝐻 ∩ 𝐵) ∧ 𝑦 ∈ (𝐻 ∩ 𝐵))) → 𝑥 ∈ 𝐵)
127		simprr 772	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (𝐻 ∩ 𝐵) ∧ 𝑦 ∈ (𝐻 ∩ 𝐵))) → 𝑦 ∈ (𝐻 ∩ 𝐵))
128	127	elin2d 4158	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (𝐻 ∩ 𝐵) ∧ 𝑦 ∈ (𝐻 ∩ 𝐵))) → 𝑦 ∈ 𝐵)
129	7, 82	ringcl 20153	. . . . . . . . . 10 ⊢ ((𝑌 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 · 𝑦) ∈ 𝐵)
130	124, 126, 128, 129	syl3anc 1373	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (𝐻 ∩ 𝐵) ∧ 𝑦 ∈ (𝐻 ∩ 𝐵))) → (𝑥 · 𝑦) ∈ 𝐵)
131	123, 130	elind 4153	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (𝐻 ∩ 𝐵) ∧ 𝑦 ∈ (𝐻 ∩ 𝐵))) → (𝑥 · 𝑦) ∈ (𝐻 ∩ 𝐵))
132	131	ralrimivva 3172	. . . . . . 7 ⊢ (𝜑 → ∀𝑥 ∈ (𝐻 ∩ 𝐵)∀𝑦 ∈ (𝐻 ∩ 𝐵)(𝑥 · 𝑦) ∈ (𝐻 ∩ 𝐵))
133	7, 37, 82	issubrg2 20495	. . . . . . . 8 ⊢ (𝑌 ∈ Ring → ((𝐻 ∩ 𝐵) ∈ (SubRing‘𝑌) ↔ ((𝐻 ∩ 𝐵) ∈ (SubGrp‘𝑌) ∧ (1_r‘𝑌) ∈ (𝐻 ∩ 𝐵) ∧ ∀𝑥 ∈ (𝐻 ∩ 𝐵)∀𝑦 ∈ (𝐻 ∩ 𝐵)(𝑥 · 𝑦) ∈ (𝐻 ∩ 𝐵))))
134	56, 133	syl 17	. . . . . . 7 ⊢ (𝜑 → ((𝐻 ∩ 𝐵) ∈ (SubRing‘𝑌) ↔ ((𝐻 ∩ 𝐵) ∈ (SubGrp‘𝑌) ∧ (1_r‘𝑌) ∈ (𝐻 ∩ 𝐵) ∧ ∀𝑥 ∈ (𝐻 ∩ 𝐵)∀𝑦 ∈ (𝐻 ∩ 𝐵)(𝑥 · 𝑦) ∈ (𝐻 ∩ 𝐵))))
135	119, 59, 132, 134	mpbir3and 1343	. . . . . 6 ⊢ (𝜑 → (𝐻 ∩ 𝐵) ∈ (SubRing‘𝑌))
136	6, 1, 7	mplval2 21921	. . . . . . . 8 ⊢ 𝑌 = ((𝐼 mPwSer 𝑅) ↾_s 𝐵)
137	136	subsubrg 20501	. . . . . . 7 ⊢ (𝐵 ∈ (SubRing‘(𝐼 mPwSer 𝑅)) → ((𝐻 ∩ 𝐵) ∈ (SubRing‘𝑌) ↔ ((𝐻 ∩ 𝐵) ∈ (SubRing‘(𝐼 mPwSer 𝑅)) ∧ (𝐻 ∩ 𝐵) ⊆ 𝐵)))
138	137	simprbda 498	. . . . . 6 ⊢ ((𝐵 ∈ (SubRing‘(𝐼 mPwSer 𝑅)) ∧ (𝐻 ∩ 𝐵) ∈ (SubRing‘𝑌)) → (𝐻 ∩ 𝐵) ∈ (SubRing‘(𝐼 mPwSer 𝑅)))
139	10, 135, 138	syl2anc 584	. . . . 5 ⊢ (𝜑 → (𝐻 ∩ 𝐵) ∈ (SubRing‘(𝐼 mPwSer 𝑅)))
140		assalmod 21785	. . . . . . 7 ⊢ ((𝐼 mPwSer 𝑅) ∈ AssAlg → (𝐼 mPwSer 𝑅) ∈ LMod)
141	4, 140	syl 17	. . . . . 6 ⊢ (𝜑 → (𝐼 mPwSer 𝑅) ∈ LMod)
142	1, 6, 7, 2, 9	mpllss 21928	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ (LSubSp‘(𝐼 mPwSer 𝑅)))
143	31	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → 𝑌 ∈ AssAlg)
144		simprl 770	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → 𝑧 ∈ (Base‘(Scalar‘𝑌)))
145		simprr 772	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → 𝑤 ∈ (𝐻 ∩ 𝐵))
146	145	elin2d 4158	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → 𝑤 ∈ 𝐵)
147		eqid 2729	. . . . . . . . . . . 12 ⊢ ( ·_𝑠 ‘𝑌) = ( ·_𝑠 ‘𝑌)
148	32, 33, 46, 7, 82, 147	asclmul1 21811	. . . . . . . . . . 11 ⊢ ((𝑌 ∈ AssAlg ∧ 𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ 𝐵) → ((𝐶‘𝑧) · 𝑤) = (𝑧( ·_𝑠 ‘𝑌)𝑤))
149	143, 144, 146, 148	syl3anc 1373	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → ((𝐶‘𝑧) · 𝑤) = (𝑧( ·_𝑠 ‘𝑌)𝑤))
150		fveq2 6826	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑧 → (𝐶‘𝑥) = (𝐶‘𝑧))
151	150	eleq1d 2813	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → ((𝐶‘𝑥) ∈ 𝐻 ↔ (𝐶‘𝑧) ∈ 𝐻))
152	43	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → ∀𝑥 ∈ 𝐾 (𝐶‘𝑥) ∈ 𝐻)
153	51	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → 𝐾 = (Base‘(Scalar‘𝑌)))
154	144, 153	eleqtrrd 2831	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → 𝑧 ∈ 𝐾)
155	151, 152, 154	rspcdva 3580	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → (𝐶‘𝑧) ∈ 𝐻)
156	145	elin1d 4157	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → 𝑤 ∈ 𝐻)
157	155, 156	jca 511	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → ((𝐶‘𝑧) ∈ 𝐻 ∧ 𝑤 ∈ 𝐻))
158	107	caovclg 7545	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝐶‘𝑧) ∈ 𝐻 ∧ 𝑤 ∈ 𝐻)) → ((𝐶‘𝑧) · 𝑤) ∈ 𝐻)
159	157, 158	syldan 591	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → ((𝐶‘𝑧) · 𝑤) ∈ 𝐻)
160	149, 159	eqeltrrd 2829	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → (𝑧( ·_𝑠 ‘𝑌)𝑤) ∈ 𝐻)
161	68	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → 𝑌 ∈ LMod)
162	7, 33, 147, 46	lmodvscl 20799	. . . . . . . . . 10 ⊢ ((𝑌 ∈ LMod ∧ 𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ 𝐵) → (𝑧( ·_𝑠 ‘𝑌)𝑤) ∈ 𝐵)
163	161, 144, 146, 162	syl3anc 1373	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → (𝑧( ·_𝑠 ‘𝑌)𝑤) ∈ 𝐵)
164	160, 163	elind 4153	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → (𝑧( ·_𝑠 ‘𝑌)𝑤) ∈ (𝐻 ∩ 𝐵))
165	164	ralrimivva 3172	. . . . . . 7 ⊢ (𝜑 → ∀𝑧 ∈ (Base‘(Scalar‘𝑌))∀𝑤 ∈ (𝐻 ∩ 𝐵)(𝑧( ·_𝑠 ‘𝑌)𝑤) ∈ (𝐻 ∩ 𝐵))
166		eqid 2729	. . . . . . . . 9 ⊢ (LSubSp‘𝑌) = (LSubSp‘𝑌)
167	33, 46, 7, 147, 166	islss4 20883	. . . . . . . 8 ⊢ (𝑌 ∈ LMod → ((𝐻 ∩ 𝐵) ∈ (LSubSp‘𝑌) ↔ ((𝐻 ∩ 𝐵) ∈ (SubGrp‘𝑌) ∧ ∀𝑧 ∈ (Base‘(Scalar‘𝑌))∀𝑤 ∈ (𝐻 ∩ 𝐵)(𝑧( ·_𝑠 ‘𝑌)𝑤) ∈ (𝐻 ∩ 𝐵))))
168	68, 167	syl 17	. . . . . . 7 ⊢ (𝜑 → ((𝐻 ∩ 𝐵) ∈ (LSubSp‘𝑌) ↔ ((𝐻 ∩ 𝐵) ∈ (SubGrp‘𝑌) ∧ ∀𝑧 ∈ (Base‘(Scalar‘𝑌))∀𝑤 ∈ (𝐻 ∩ 𝐵)(𝑧( ·_𝑠 ‘𝑌)𝑤) ∈ (𝐻 ∩ 𝐵))))
169	119, 165, 168	mpbir2and 713	. . . . . 6 ⊢ (𝜑 → (𝐻 ∩ 𝐵) ∈ (LSubSp‘𝑌))
170		eqid 2729	. . . . . . . 8 ⊢ (LSubSp‘(𝐼 mPwSer 𝑅)) = (LSubSp‘(𝐼 mPwSer 𝑅))
171	136, 170, 166	lsslss 20882	. . . . . . 7 ⊢ (((𝐼 mPwSer 𝑅) ∈ LMod ∧ 𝐵 ∈ (LSubSp‘(𝐼 mPwSer 𝑅))) → ((𝐻 ∩ 𝐵) ∈ (LSubSp‘𝑌) ↔ ((𝐻 ∩ 𝐵) ∈ (LSubSp‘(𝐼 mPwSer 𝑅)) ∧ (𝐻 ∩ 𝐵) ⊆ 𝐵)))
172	171	simprbda 498	. . . . . 6 ⊢ ((((𝐼 mPwSer 𝑅) ∈ LMod ∧ 𝐵 ∈ (LSubSp‘(𝐼 mPwSer 𝑅))) ∧ (𝐻 ∩ 𝐵) ∈ (LSubSp‘𝑌)) → (𝐻 ∩ 𝐵) ∈ (LSubSp‘(𝐼 mPwSer 𝑅)))
173	141, 142, 169, 172	syl21anc 837	. . . . 5 ⊢ (𝜑 → (𝐻 ∩ 𝐵) ∈ (LSubSp‘(𝐼 mPwSer 𝑅)))
174	24, 11, 170	aspid 21800	. . . . 5 ⊢ (((𝐼 mPwSer 𝑅) ∈ AssAlg ∧ (𝐻 ∩ 𝐵) ∈ (SubRing‘(𝐼 mPwSer 𝑅)) ∧ (𝐻 ∩ 𝐵) ∈ (LSubSp‘(𝐼 mPwSer 𝑅))) → ((AlgSpan‘(𝐼 mPwSer 𝑅))‘(𝐻 ∩ 𝐵)) = (𝐻 ∩ 𝐵))
175	4, 139, 173, 174	syl3anc 1373	. . . 4 ⊢ (𝜑 → ((AlgSpan‘(𝐼 mPwSer 𝑅))‘(𝐻 ∩ 𝐵)) = (𝐻 ∩ 𝐵))
176	26, 28, 175	3sstr3d 3992	. . 3 ⊢ (𝜑 → 𝐵 ⊆ (𝐻 ∩ 𝐵))
177		mplind.x	. . 3 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
178	176, 177	sseldd 3938	. 2 ⊢ (𝜑 → 𝑋 ∈ (𝐻 ∩ 𝐵))
179	178	elin1d 4157	1 ⊢ (𝜑 → 𝑋 ∈ 𝐻)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1086 = wceq 1540 ∈ wcel 2109 ≠ wne 2925 ∀wral 3044 ∩ cin 3904 ⊆ wss 3905 ∅c0 4286 ran crn 5624 Fn wfn 6481 ‘cfv 6486 (class class class)co 7353 Basecbs 17138 +_gcplusg 17179 ._rcmulr 17180 Scalarcsca 17182 ·_𝑠 cvsca 17183 Grpcgrp 18830 inv_gcminusg 18831 SubGrpcsubg 19017 GrpHom cghm 19109 1_rcur 20084 Ringcrg 20136 CRingccrg 20137 RingHom crh 20372 SubRingcsubrg 20472 LModclmod 20781 LSubSpclss 20852 AssAlgcasa 21775 AlgSpancasp 21776 algSccascl 21777 mPwSer cmps 21829 mVar cmvr 21830 mPoly cmpl 21831

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2008 ax-8 2111 ax-9 2119 ax-10 2142 ax-11 2158 ax-12 2178 ax-ext 2701 ax-rep 5221 ax-sep 5238 ax-nul 5248 ax-pow 5307 ax-pr 5374 ax-un 7675 ax-cnex 11084 ax-resscn 11085 ax-1cn 11086 ax-icn 11087 ax-addcl 11088 ax-addrcl 11089 ax-mulcl 11090 ax-mulrcl 11091 ax-mulcom 11092 ax-addass 11093 ax-mulass 11094 ax-distr 11095 ax-i2m1 11096 ax-1ne0 11097 ax-1rid 11098 ax-rnegex 11099 ax-rrecex 11100 ax-cnre 11101 ax-pre-lttri 11102 ax-pre-lttrn 11103 ax-pre-ltadd 11104 ax-pre-mulgt0 11105

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2533 df-eu 2562 df-clab 2708 df-cleq 2721 df-clel 2803 df-nfc 2878 df-ne 2926 df-nel 3030 df-ral 3045 df-rex 3054 df-rmo 3345 df-reu 3346 df-rab 3397 df-v 3440 df-sbc 3745 df-csb 3854 df-dif 3908 df-un 3910 df-in 3912 df-ss 3922 df-pss 3925 df-nul 4287 df-if 4479 df-pw 4555 df-sn 4580 df-pr 4582 df-tp 4584 df-op 4586 df-uni 4862 df-int 4900 df-iun 4946 df-iin 4947 df-br 5096 df-opab 5158 df-mpt 5177 df-tr 5203 df-id 5518 df-eprel 5523 df-po 5531 df-so 5532 df-fr 5576 df-se 5577 df-we 5578 df-xp 5629 df-rel 5630 df-cnv 5631 df-co 5632 df-dm 5633 df-rn 5634 df-res 5635 df-ima 5636 df-pred 6253 df-ord 6314 df-on 6315 df-lim 6316 df-suc 6317 df-iota 6442 df-fun 6488 df-fn 6489 df-f 6490 df-f1 6491 df-fo 6492 df-f1o 6493 df-fv 6494 df-isom 6495 df-riota 7310 df-ov 7356 df-oprab 7357 df-mpo 7358 df-of 7617 df-ofr 7618 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 8632 df-map 8762 df-pm 8763 df-ixp 8832 df-en 8880 df-dom 8881 df-sdom 8882 df-fin 8883 df-fsupp 9271 df-sup 9351 df-oi 9421 df-card 9854 df-pnf 11170 df-mnf 11171 df-xr 11172 df-ltxr 11173 df-le 11174 df-sub 11367 df-neg 11368 df-nn 12147 df-2 12209 df-3 12210 df-4 12211 df-5 12212 df-6 12213 df-7 12214 df-8 12215 df-9 12216 df-n0 12403 df-z 12490 df-dec 12610 df-uz 12754 df-fz 13429 df-fzo 13576 df-seq 13927 df-hash 14256 df-struct 17076 df-sets 17093 df-slot 17111 df-ndx 17123 df-base 17139 df-ress 17160 df-plusg 17192 df-mulr 17193 df-sca 17195 df-vsca 17196 df-ip 17197 df-tset 17198 df-ple 17199 df-ds 17201 df-hom 17203 df-cco 17204 df-0g 17363 df-gsum 17364 df-prds 17369 df-pws 17371 df-mre 17506 df-mrc 17507 df-acs 17509 df-mgm 18532 df-sgrp 18611 df-mnd 18627 df-mhm 18675 df-submnd 18676 df-grp 18833 df-minusg 18834 df-sbg 18835 df-mulg 18965 df-subg 19020 df-ghm 19110 df-cntz 19214 df-cmn 19679 df-abl 19680 df-mgp 20044 df-rng 20056 df-ur 20085 df-srg 20090 df-ring 20138 df-cring 20139 df-rhm 20375 df-subrng 20449 df-subrg 20473 df-lmod 20783 df-lss 20853 df-assa 21778 df-asp 21779 df-ascl 21780 df-psr 21834 df-mvr 21835 df-mpl 21836

This theorem is referenced by: mpfind 22030

W3C validator