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 22094

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 2737	. . . . . 6 ⊢ (𝐼 mPwSer 𝑅) = (𝐼 mPwSer 𝑅)
2		mplind.i	. . . . . 6 ⊢ (𝜑 → 𝐼 ∈ 𝑊)
3		mplind.r	. . . . . 6 ⊢ (𝜑 → 𝑅 ∈ CRing)
4	1, 2, 3	psrassa 21993	. . . . 5 ⊢ (𝜑 → (𝐼 mPwSer 𝑅) ∈ AssAlg)
5		inss2 4238	. . . . . 6 ⊢ (𝐻 ∩ 𝐵) ⊆ 𝐵
6		mplind.sy	. . . . . . . 8 ⊢ 𝑌 = (𝐼 mPoly 𝑅)
7		mplind.sb	. . . . . . . 8 ⊢ 𝐵 = (Base‘𝑌)
8		crngring 20242	. . . . . . . . 9 ⊢ (𝑅 ∈ CRing → 𝑅 ∈ Ring)
9	3, 8	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑅 ∈ Ring)
10	1, 6, 7, 2, 9	mplsubrg 22025	. . . . . . 7 ⊢ (𝜑 → 𝐵 ∈ (SubRing‘(𝐼 mPwSer 𝑅)))
11		eqid 2737	. . . . . . . 8 ⊢ (Base‘(𝐼 mPwSer 𝑅)) = (Base‘(𝐼 mPwSer 𝑅))
12	11	subrgss 20572	. . . . . . 7 ⊢ (𝐵 ∈ (SubRing‘(𝐼 mPwSer 𝑅)) → 𝐵 ⊆ (Base‘(𝐼 mPwSer 𝑅)))
13	10, 12	syl 17	. . . . . 6 ⊢ (𝜑 → 𝐵 ⊆ (Base‘(𝐼 mPwSer 𝑅)))
14	5, 13	sstrid 3995	. . . . 5 ⊢ (𝜑 → (𝐻 ∩ 𝐵) ⊆ (Base‘(𝐼 mPwSer 𝑅)))
15		mplind.sv	. . . . . . . . 9 ⊢ 𝑉 = (𝐼 mVar 𝑅)
16	6, 15, 7, 2, 9	mvrf2 22013	. . . . . . . 8 ⊢ (𝜑 → 𝑉:𝐼⟶𝐵)
17	16	ffnd 6737	. . . . . . 7 ⊢ (𝜑 → 𝑉 Fn 𝐼)
18		mplind.v	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → (𝑉‘𝑥) ∈ 𝐻)
19	18	ralrimiva 3146	. . . . . . 7 ⊢ (𝜑 → ∀𝑥 ∈ 𝐼 (𝑉‘𝑥) ∈ 𝐻)
20		fnfvrnss 7141	. . . . . . 7 ⊢ ((𝑉 Fn 𝐼 ∧ ∀𝑥 ∈ 𝐼 (𝑉‘𝑥) ∈ 𝐻) → ran 𝑉 ⊆ 𝐻)
21	17, 19, 20	syl2anc 584	. . . . . 6 ⊢ (𝜑 → ran 𝑉 ⊆ 𝐻)
22	16	frnd 6744	. . . . . 6 ⊢ (𝜑 → ran 𝑉 ⊆ 𝐵)
23	21, 22	ssind 4241	. . . . 5 ⊢ (𝜑 → ran 𝑉 ⊆ (𝐻 ∩ 𝐵))
24		eqid 2737	. . . . . 6 ⊢ (AlgSpan‘(𝐼 mPwSer 𝑅)) = (AlgSpan‘(𝐼 mPwSer 𝑅))
25	24, 11	aspss 21897	. . . . 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 22060	. . . . 5 ⊢ (𝜑 → ((AlgSpan‘(𝐼 mPwSer 𝑅))‘ran 𝑉) = (Base‘𝑌))
28	27, 7	eqtr4di 2795	. . . 4 ⊢ (𝜑 → ((AlgSpan‘(𝐼 mPwSer 𝑅))‘ran 𝑉) = 𝐵)
29	5	a1i 11	. . . . . . . 8 ⊢ (𝜑 → (𝐻 ∩ 𝐵) ⊆ 𝐵)
30	6	mplassa 22042	. . . . . . . . . . . . . 14 ⊢ ((𝐼 ∈ 𝑊 ∧ 𝑅 ∈ CRing) → 𝑌 ∈ AssAlg)
31	2, 3, 30	syl2anc 584	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝑌 ∈ AssAlg)
32		mplind.sc	. . . . . . . . . . . . . 14 ⊢ 𝐶 = (algSc‘𝑌)
33		eqid 2737	. . . . . . . . . . . . . 14 ⊢ (Scalar‘𝑌) = (Scalar‘𝑌)
34	32, 33	asclrhm 21910	. . . . . . . . . . . . 13 ⊢ (𝑌 ∈ AssAlg → 𝐶 ∈ ((Scalar‘𝑌) RingHom 𝑌))
35	31, 34	syl 17	. . . . . . . . . . . 12 ⊢ (𝜑 → 𝐶 ∈ ((Scalar‘𝑌) RingHom 𝑌))
36		eqid 2737	. . . . . . . . . . . . 13 ⊢ (1_r‘(Scalar‘𝑌)) = (1_r‘(Scalar‘𝑌))
37		eqid 2737	. . . . . . . . . . . . 13 ⊢ (1_r‘𝑌) = (1_r‘𝑌)
38	36, 37	rhm1 20489	. . . . . . . . . . . 12 ⊢ (𝐶 ∈ ((Scalar‘𝑌) RingHom 𝑌) → (𝐶‘(1_r‘(Scalar‘𝑌))) = (1_r‘𝑌))
39	35, 38	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶‘(1_r‘(Scalar‘𝑌))) = (1_r‘𝑌))
40		fveq2 6906	. . . . . . . . . . . . 13 ⊢ (𝑥 = (1_r‘(Scalar‘𝑌)) → (𝐶‘𝑥) = (𝐶‘(1_r‘(Scalar‘𝑌))))
41	40	eleq1d 2826	. . . . . . . . . . . 12 ⊢ (𝑥 = (1_r‘(Scalar‘𝑌)) → ((𝐶‘𝑥) ∈ 𝐻 ↔ (𝐶‘(1_r‘(Scalar‘𝑌))) ∈ 𝐻))
42		mplind.s	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐾) → (𝐶‘𝑥) ∈ 𝐻)
43	42	ralrimiva 3146	. . . . . . . . . . . 12 ⊢ (𝜑 → ∀𝑥 ∈ 𝐾 (𝐶‘𝑥) ∈ 𝐻)
44	6, 2, 3	mplsca 22033	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑅 = (Scalar‘𝑌))
45	44, 9	eqeltrrd 2842	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (Scalar‘𝑌) ∈ Ring)
46		eqid 2737	. . . . . . . . . . . . . . 15 ⊢ (Base‘(Scalar‘𝑌)) = (Base‘(Scalar‘𝑌))
47	46, 36	ringidcl 20262	. . . . . . . . . . . . . 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 6910	. . . . . . . . . . . . . 14 ⊢ (𝜑 → (Base‘𝑅) = (Base‘(Scalar‘𝑌)))
51	49, 50	eqtrid 2789	. . . . . . . . . . . . 13 ⊢ (𝜑 → 𝐾 = (Base‘(Scalar‘𝑌)))
52	48, 51	eleqtrrd 2844	. . . . . . . . . . . 12 ⊢ (𝜑 → (1_r‘(Scalar‘𝑌)) ∈ 𝐾)
53	41, 43, 52	rspcdva 3623	. . . . . . . . . . 11 ⊢ (𝜑 → (𝐶‘(1_r‘(Scalar‘𝑌))) ∈ 𝐻)
54	39, 53	eqeltrrd 2842	. . . . . . . . . 10 ⊢ (𝜑 → (1_r‘𝑌) ∈ 𝐻)
55		assaring 21881	. . . . . . . . . . . 12 ⊢ (𝑌 ∈ AssAlg → 𝑌 ∈ Ring)
56	31, 55	syl 17	. . . . . . . . . . 11 ⊢ (𝜑 → 𝑌 ∈ Ring)
57	7, 37	ringidcl 20262	. . . . . . . . . . 11 ⊢ (𝑌 ∈ Ring → (1_r‘𝑌) ∈ 𝐵)
58	56, 57	syl 17	. . . . . . . . . 10 ⊢ (𝜑 → (1_r‘𝑌) ∈ 𝐵)
59	54, 58	elind 4200	. . . . . . . . 9 ⊢ (𝜑 → (1_r‘𝑌) ∈ (𝐻 ∩ 𝐵))
60	59	ne0d 4342	. . . . . . . 8 ⊢ (𝜑 → (𝐻 ∩ 𝐵) ≠ ∅)
61		elinel1 4201	. . . . . . . . . . . . . . 15 ⊢ (𝑧 ∈ (𝐻 ∩ 𝐵) → 𝑧 ∈ 𝐻)
62		elinel1 4201	. . . . . . . . . . . . . . 15 ⊢ (𝑤 ∈ (𝐻 ∩ 𝐵) → 𝑤 ∈ 𝐻)
63	61, 62	anim12i 613	. . . . . . . . . . . . . 14 ⊢ ((𝑧 ∈ (𝐻 ∩ 𝐵) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵)) → (𝑧 ∈ 𝐻 ∧ 𝑤 ∈ 𝐻))
64		mplind.p	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻)) → (𝑥 + 𝑦) ∈ 𝐻)
65	64	caovclg 7625	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑧 ∈ 𝐻 ∧ 𝑤 ∈ 𝐻)) → (𝑧 + 𝑤) ∈ 𝐻)
66	63, 65	sylan2 593	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐻 ∩ 𝐵) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → (𝑧 + 𝑤) ∈ 𝐻)
67		assalmod 21880	. . . . . . . . . . . . . . . . 17 ⊢ (𝑌 ∈ AssAlg → 𝑌 ∈ LMod)
68	31, 67	syl 17	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → 𝑌 ∈ LMod)
69		lmodgrp 20865	. . . . . . . . . . . . . . . 16 ⊢ (𝑌 ∈ LMod → 𝑌 ∈ Grp)
70	68, 69	syl 17	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → 𝑌 ∈ Grp)
71	70	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐻 ∩ 𝐵) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → 𝑌 ∈ Grp)
72		simprl 771	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐻 ∩ 𝐵) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → 𝑧 ∈ (𝐻 ∩ 𝐵))
73	72	elin2d 4205	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐻 ∩ 𝐵) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → 𝑧 ∈ 𝐵)
74		simprr 773	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐻 ∩ 𝐵) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → 𝑤 ∈ (𝐻 ∩ 𝐵))
75	74	elin2d 4205	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐻 ∩ 𝐵) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → 𝑤 ∈ 𝐵)
76		mplind.sp	. . . . . . . . . . . . . . 15 ⊢ + = (+_g‘𝑌)
77	7, 76	grpcl 18959	. . . . . . . . . . . . . 14 ⊢ ((𝑌 ∈ Grp ∧ 𝑧 ∈ 𝐵 ∧ 𝑤 ∈ 𝐵) → (𝑧 + 𝑤) ∈ 𝐵)
78	71, 73, 75, 77	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐻 ∩ 𝐵) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → (𝑧 + 𝑤) ∈ 𝐵)
79	66, 78	elind 4200	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑧 ∈ (𝐻 ∩ 𝐵) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → (𝑧 + 𝑤) ∈ (𝐻 ∩ 𝐵))
80	79	anassrs 467	. . . . . . . . . . 11 ⊢ (((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵)) → (𝑧 + 𝑤) ∈ (𝐻 ∩ 𝐵))
81	80	ralrimiva 3146	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) → ∀𝑤 ∈ (𝐻 ∩ 𝐵)(𝑧 + 𝑤) ∈ (𝐻 ∩ 𝐵))
82		mplind.st	. . . . . . . . . . . . 13 ⊢ · = (._r‘𝑌)
83		eqid 2737	. . . . . . . . . . . . 13 ⊢ (inv_g‘𝑌) = (inv_g‘𝑌)
84	56	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) → 𝑌 ∈ Ring)
85		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) → 𝑧 ∈ (𝐻 ∩ 𝐵))
86	85	elin2d 4205	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) → 𝑧 ∈ 𝐵)
87	7, 82, 37, 83, 84, 86	ringnegl 20299	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) → (((inv_g‘𝑌)‘(1_r‘𝑌)) · 𝑧) = ((inv_g‘𝑌)‘𝑧))
88		simpl 482	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) → 𝜑)
89		rhmghm 20484	. . . . . . . . . . . . . . . . . 18 ⊢ (𝐶 ∈ ((Scalar‘𝑌) RingHom 𝑌) → 𝐶 ∈ ((Scalar‘𝑌) GrpHom 𝑌))
90	35, 89	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (𝜑 → 𝐶 ∈ ((Scalar‘𝑌) GrpHom 𝑌))
91		eqid 2737	. . . . . . . . . . . . . . . . . 18 ⊢ (inv_g‘(Scalar‘𝑌)) = (inv_g‘(Scalar‘𝑌))
92	46, 91, 83	ghminv 19241	. . . . . . . . . . . . . . . . 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 6910	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((inv_g‘𝑌)‘(𝐶‘(1_r‘(Scalar‘𝑌)))) = ((inv_g‘𝑌)‘(1_r‘𝑌)))
95	93, 94	eqtrd 2777	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐶‘((inv_g‘(Scalar‘𝑌))‘(1_r‘(Scalar‘𝑌)))) = ((inv_g‘𝑌)‘(1_r‘𝑌)))
96		fveq2 6906	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = ((inv_g‘(Scalar‘𝑌))‘(1_r‘(Scalar‘𝑌))) → (𝐶‘𝑥) = (𝐶‘((inv_g‘(Scalar‘𝑌))‘(1_r‘(Scalar‘𝑌)))))
97	96	eleq1d 2826	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = ((inv_g‘(Scalar‘𝑌))‘(1_r‘(Scalar‘𝑌))) → ((𝐶‘𝑥) ∈ 𝐻 ↔ (𝐶‘((inv_g‘(Scalar‘𝑌))‘(1_r‘(Scalar‘𝑌)))) ∈ 𝐻))
98		ringgrp 20235	. . . . . . . . . . . . . . . . . . 19 ⊢ ((Scalar‘𝑌) ∈ Ring → (Scalar‘𝑌) ∈ Grp)
99	45, 98	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ (𝜑 → (Scalar‘𝑌) ∈ Grp)
100	46, 91	grpinvcl 19005	. . . . . . . . . . . . . . . . . 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 2844	. . . . . . . . . . . . . . . 16 ⊢ (𝜑 → ((inv_g‘(Scalar‘𝑌))‘(1_r‘(Scalar‘𝑌))) ∈ 𝐾)
103	97, 43, 102	rspcdva 3623	. . . . . . . . . . . . . . 15 ⊢ (𝜑 → (𝐶‘((inv_g‘(Scalar‘𝑌))‘(1_r‘(Scalar‘𝑌)))) ∈ 𝐻)
104	95, 103	eqeltrrd 2842	. . . . . . . . . . . . . 14 ⊢ (𝜑 → ((inv_g‘𝑌)‘(1_r‘𝑌)) ∈ 𝐻)
105	104	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) → ((inv_g‘𝑌)‘(1_r‘𝑌)) ∈ 𝐻)
106	85	elin1d 4204	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) → 𝑧 ∈ 𝐻)
107		mplind.t	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻)) → (𝑥 · 𝑦) ∈ 𝐻)
108	107	caovclg 7625	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (((inv_g‘𝑌)‘(1_r‘𝑌)) ∈ 𝐻 ∧ 𝑧 ∈ 𝐻)) → (((inv_g‘𝑌)‘(1_r‘𝑌)) · 𝑧) ∈ 𝐻)
109	88, 105, 106, 108	syl12anc 837	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) → (((inv_g‘𝑌)‘(1_r‘𝑌)) · 𝑧) ∈ 𝐻)
110	87, 109	eqeltrrd 2842	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) → ((inv_g‘𝑌)‘𝑧) ∈ 𝐻)
111	70	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) → 𝑌 ∈ Grp)
112	7, 83	grpinvcl 19005	. . . . . . . . . . . 12 ⊢ ((𝑌 ∈ Grp ∧ 𝑧 ∈ 𝐵) → ((inv_g‘𝑌)‘𝑧) ∈ 𝐵)
113	111, 86, 112	syl2anc 584	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) → ((inv_g‘𝑌)‘𝑧) ∈ 𝐵)
114	110, 113	elind 4200	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) → ((inv_g‘𝑌)‘𝑧) ∈ (𝐻 ∩ 𝐵))
115	81, 114	jca 511	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑧 ∈ (𝐻 ∩ 𝐵)) → (∀𝑤 ∈ (𝐻 ∩ 𝐵)(𝑧 + 𝑤) ∈ (𝐻 ∩ 𝐵) ∧ ((inv_g‘𝑌)‘𝑧) ∈ (𝐻 ∩ 𝐵)))
116	115	ralrimiva 3146	. . . . . . . 8 ⊢ (𝜑 → ∀𝑧 ∈ (𝐻 ∩ 𝐵)(∀𝑤 ∈ (𝐻 ∩ 𝐵)(𝑧 + 𝑤) ∈ (𝐻 ∩ 𝐵) ∧ ((inv_g‘𝑌)‘𝑧) ∈ (𝐻 ∩ 𝐵)))
117	7, 76, 83	issubg2 19159	. . . . . . . . 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 4201	. . . . . . . . . . 11 ⊢ (𝑥 ∈ (𝐻 ∩ 𝐵) → 𝑥 ∈ 𝐻)
121		elinel1 4201	. . . . . . . . . . 11 ⊢ (𝑦 ∈ (𝐻 ∩ 𝐵) → 𝑦 ∈ 𝐻)
122	120, 121	anim12i 613	. . . . . . . . . 10 ⊢ ((𝑥 ∈ (𝐻 ∩ 𝐵) ∧ 𝑦 ∈ (𝐻 ∩ 𝐵)) → (𝑥 ∈ 𝐻 ∧ 𝑦 ∈ 𝐻))
123	122, 107	sylan2 593	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (𝐻 ∩ 𝐵) ∧ 𝑦 ∈ (𝐻 ∩ 𝐵))) → (𝑥 · 𝑦) ∈ 𝐻)
124	56	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (𝐻 ∩ 𝐵) ∧ 𝑦 ∈ (𝐻 ∩ 𝐵))) → 𝑌 ∈ Ring)
125		simprl 771	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (𝐻 ∩ 𝐵) ∧ 𝑦 ∈ (𝐻 ∩ 𝐵))) → 𝑥 ∈ (𝐻 ∩ 𝐵))
126	125	elin2d 4205	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (𝐻 ∩ 𝐵) ∧ 𝑦 ∈ (𝐻 ∩ 𝐵))) → 𝑥 ∈ 𝐵)
127		simprr 773	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑥 ∈ (𝐻 ∩ 𝐵) ∧ 𝑦 ∈ (𝐻 ∩ 𝐵))) → 𝑦 ∈ (𝐻 ∩ 𝐵))
128	127	elin2d 4205	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑥 ∈ (𝐻 ∩ 𝐵) ∧ 𝑦 ∈ (𝐻 ∩ 𝐵))) → 𝑦 ∈ 𝐵)
129	7, 82	ringcl 20247	. . . . . . . . . 10 ⊢ ((𝑌 ∈ Ring ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 · 𝑦) ∈ 𝐵)
130	124, 126, 128, 129	syl3anc 1373	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑥 ∈ (𝐻 ∩ 𝐵) ∧ 𝑦 ∈ (𝐻 ∩ 𝐵))) → (𝑥 · 𝑦) ∈ 𝐵)
131	123, 130	elind 4200	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑥 ∈ (𝐻 ∩ 𝐵) ∧ 𝑦 ∈ (𝐻 ∩ 𝐵))) → (𝑥 · 𝑦) ∈ (𝐻 ∩ 𝐵))
132	131	ralrimivva 3202	. . . . . . 7 ⊢ (𝜑 → ∀𝑥 ∈ (𝐻 ∩ 𝐵)∀𝑦 ∈ (𝐻 ∩ 𝐵)(𝑥 · 𝑦) ∈ (𝐻 ∩ 𝐵))
133	7, 37, 82	issubrg2 20592	. . . . . . . 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 22016	. . . . . . . 8 ⊢ 𝑌 = ((𝐼 mPwSer 𝑅) ↾_s 𝐵)
137	136	subsubrg 20598	. . . . . . 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 21880	. . . . . . 7 ⊢ ((𝐼 mPwSer 𝑅) ∈ AssAlg → (𝐼 mPwSer 𝑅) ∈ LMod)
141	4, 140	syl 17	. . . . . 6 ⊢ (𝜑 → (𝐼 mPwSer 𝑅) ∈ LMod)
142	1, 6, 7, 2, 9	mpllss 22023	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ (LSubSp‘(𝐼 mPwSer 𝑅)))
143	31	adantr 480	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → 𝑌 ∈ AssAlg)
144		simprl 771	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → 𝑧 ∈ (Base‘(Scalar‘𝑌)))
145		simprr 773	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → 𝑤 ∈ (𝐻 ∩ 𝐵))
146	145	elin2d 4205	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → 𝑤 ∈ 𝐵)
147		eqid 2737	. . . . . . . . . . . 12 ⊢ ( ·_𝑠 ‘𝑌) = ( ·_𝑠 ‘𝑌)
148	32, 33, 46, 7, 82, 147	asclmul1 21906	. . . . . . . . . . 11 ⊢ ((𝑌 ∈ AssAlg ∧ 𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ 𝐵) → ((𝐶‘𝑧) · 𝑤) = (𝑧( ·_𝑠 ‘𝑌)𝑤))
149	143, 144, 146, 148	syl3anc 1373	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → ((𝐶‘𝑧) · 𝑤) = (𝑧( ·_𝑠 ‘𝑌)𝑤))
150		fveq2 6906	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑧 → (𝐶‘𝑥) = (𝐶‘𝑧))
151	150	eleq1d 2826	. . . . . . . . . . . . 13 ⊢ (𝑥 = 𝑧 → ((𝐶‘𝑥) ∈ 𝐻 ↔ (𝐶‘𝑧) ∈ 𝐻))
152	43	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → ∀𝑥 ∈ 𝐾 (𝐶‘𝑥) ∈ 𝐻)
153	51	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → 𝐾 = (Base‘(Scalar‘𝑌)))
154	144, 153	eleqtrrd 2844	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → 𝑧 ∈ 𝐾)
155	151, 152, 154	rspcdva 3623	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → (𝐶‘𝑧) ∈ 𝐻)
156	145	elin1d 4204	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → 𝑤 ∈ 𝐻)
157	155, 156	jca 511	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → ((𝐶‘𝑧) ∈ 𝐻 ∧ 𝑤 ∈ 𝐻))
158	107	caovclg 7625	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ ((𝐶‘𝑧) ∈ 𝐻 ∧ 𝑤 ∈ 𝐻)) → ((𝐶‘𝑧) · 𝑤) ∈ 𝐻)
159	157, 158	syldan 591	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → ((𝐶‘𝑧) · 𝑤) ∈ 𝐻)
160	149, 159	eqeltrrd 2842	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → (𝑧( ·_𝑠 ‘𝑌)𝑤) ∈ 𝐻)
161	68	adantr 480	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → 𝑌 ∈ LMod)
162	7, 33, 147, 46	lmodvscl 20876	. . . . . . . . . 10 ⊢ ((𝑌 ∈ LMod ∧ 𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ 𝐵) → (𝑧( ·_𝑠 ‘𝑌)𝑤) ∈ 𝐵)
163	161, 144, 146, 162	syl3anc 1373	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → (𝑧( ·_𝑠 ‘𝑌)𝑤) ∈ 𝐵)
164	160, 163	elind 4200	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑧 ∈ (Base‘(Scalar‘𝑌)) ∧ 𝑤 ∈ (𝐻 ∩ 𝐵))) → (𝑧( ·_𝑠 ‘𝑌)𝑤) ∈ (𝐻 ∩ 𝐵))
165	164	ralrimivva 3202	. . . . . . 7 ⊢ (𝜑 → ∀𝑧 ∈ (Base‘(Scalar‘𝑌))∀𝑤 ∈ (𝐻 ∩ 𝐵)(𝑧( ·_𝑠 ‘𝑌)𝑤) ∈ (𝐻 ∩ 𝐵))
166		eqid 2737	. . . . . . . . 9 ⊢ (LSubSp‘𝑌) = (LSubSp‘𝑌)
167	33, 46, 7, 147, 166	islss4 20960	. . . . . . . 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 2737	. . . . . . . 8 ⊢ (LSubSp‘(𝐼 mPwSer 𝑅)) = (LSubSp‘(𝐼 mPwSer 𝑅))
171	136, 170, 166	lsslss 20959	. . . . . . 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 838	. . . . 5 ⊢ (𝜑 → (𝐻 ∩ 𝐵) ∈ (LSubSp‘(𝐼 mPwSer 𝑅)))
174	24, 11, 170	aspid 21895	. . . . 5 ⊢ (((𝐼 mPwSer 𝑅) ∈ AssAlg ∧ (𝐻 ∩ 𝐵) ∈ (SubRing‘(𝐼 mPwSer 𝑅)) ∧ (𝐻 ∩ 𝐵) ∈ (LSubSp‘(𝐼 mPwSer 𝑅))) → ((AlgSpan‘(𝐼 mPwSer 𝑅))‘(𝐻 ∩ 𝐵)) = (𝐻 ∩ 𝐵))
175	4, 139, 173, 174	syl3anc 1373	. . . 4 ⊢ (𝜑 → ((AlgSpan‘(𝐼 mPwSer 𝑅))‘(𝐻 ∩ 𝐵)) = (𝐻 ∩ 𝐵))
176	26, 28, 175	3sstr3d 4038	. . 3 ⊢ (𝜑 → 𝐵 ⊆ (𝐻 ∩ 𝐵))
177		mplind.x	. . 3 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
178	176, 177	sseldd 3984	. 2 ⊢ (𝜑 → 𝑋 ∈ (𝐻 ∩ 𝐵))
179	178	elin1d 4204	1 ⊢ (𝜑 → 𝑋 ∈ 𝐻)

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∧ w3a 1087 = wceq 1540 ∈ wcel 2108 ≠ wne 2940 ∀wral 3061 ∩ cin 3950 ⊆ wss 3951 ∅c0 4333 ran crn 5686 Fn wfn 6556 ‘cfv 6561 (class class class)co 7431 Basecbs 17247 +_gcplusg 17297 ._rcmulr 17298 Scalarcsca 17300 ·_𝑠 cvsca 17301 Grpcgrp 18951 inv_gcminusg 18952 SubGrpcsubg 19138 GrpHom cghm 19230 1_rcur 20178 Ringcrg 20230 CRingccrg 20231 RingHom crh 20469 SubRingcsubrg 20569 LModclmod 20858 LSubSpclss 20929 AssAlgcasa 21870 AlgSpancasp 21871 algSccascl 21872 mPwSer cmps 21924 mVar cmvr 21925 mPoly cmpl 21926

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 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-rep 5279 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755 ax-cnex 11211 ax-resscn 11212 ax-1cn 11213 ax-icn 11214 ax-addcl 11215 ax-addrcl 11216 ax-mulcl 11217 ax-mulrcl 11218 ax-mulcom 11219 ax-addass 11220 ax-mulass 11221 ax-distr 11222 ax-i2m1 11223 ax-1ne0 11224 ax-1rid 11225 ax-rnegex 11226 ax-rrecex 11227 ax-cnre 11228 ax-pre-lttri 11229 ax-pre-lttrn 11230 ax-pre-ltadd 11231 ax-pre-mulgt0 11232

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-nel 3047 df-ral 3062 df-rex 3071 df-rmo 3380 df-reu 3381 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-pss 3971 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-tp 4631 df-op 4633 df-uni 4908 df-int 4947 df-iun 4993 df-iin 4994 df-br 5144 df-opab 5206 df-mpt 5226 df-tr 5260 df-id 5578 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5637 df-se 5638 df-we 5639 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-pred 6321 df-ord 6387 df-on 6388 df-lim 6389 df-suc 6390 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-isom 6570 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-of 7697 df-ofr 7698 df-om 7888 df-1st 8014 df-2nd 8015 df-supp 8186 df-frecs 8306 df-wrecs 8337 df-recs 8411 df-rdg 8450 df-1o 8506 df-2o 8507 df-er 8745 df-map 8868 df-pm 8869 df-ixp 8938 df-en 8986 df-dom 8987 df-sdom 8988 df-fin 8989 df-fsupp 9402 df-sup 9482 df-oi 9550 df-card 9979 df-pnf 11297 df-mnf 11298 df-xr 11299 df-ltxr 11300 df-le 11301 df-sub 11494 df-neg 11495 df-nn 12267 df-2 12329 df-3 12330 df-4 12331 df-5 12332 df-6 12333 df-7 12334 df-8 12335 df-9 12336 df-n0 12527 df-z 12614 df-dec 12734 df-uz 12879 df-fz 13548 df-fzo 13695 df-seq 14043 df-hash 14370 df-struct 17184 df-sets 17201 df-slot 17219 df-ndx 17231 df-base 17248 df-ress 17275 df-plusg 17310 df-mulr 17311 df-sca 17313 df-vsca 17314 df-ip 17315 df-tset 17316 df-ple 17317 df-ds 17319 df-hom 17321 df-cco 17322 df-0g 17486 df-gsum 17487 df-prds 17492 df-pws 17494 df-mre 17629 df-mrc 17630 df-acs 17632 df-mgm 18653 df-sgrp 18732 df-mnd 18748 df-mhm 18796 df-submnd 18797 df-grp 18954 df-minusg 18955 df-sbg 18956 df-mulg 19086 df-subg 19141 df-ghm 19231 df-cntz 19335 df-cmn 19800 df-abl 19801 df-mgp 20138 df-rng 20150 df-ur 20179 df-srg 20184 df-ring 20232 df-cring 20233 df-rhm 20472 df-subrng 20546 df-subrg 20570 df-lmod 20860 df-lss 20930 df-assa 21873 df-asp 21874 df-ascl 21875 df-psr 21929 df-mvr 21930 df-mpl 21931

This theorem is referenced by: mpfind 22131

W3C validator