mplind

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)

	Ref	Expression
Hypotheses	mplind.sk	$⊢ K = {Base}_{R}$
	mplind.sv	$⊢ V = I mVar R$
	mplind.sy	$⊢ Y = I mPoly R$
	mplind.sp	$⊢ \underset{˙}{+} = +_{Y}$
	mplind.st	$⊢ \underset{˙}{\cdot} = \cdot_{Y}$
	mplind.sc	$⊢ C = algSc (Y)$
	mplind.sb	$⊢ B = {Base}_{Y}$
	mplind.p	$⊢ (φ \land (x \in H \land y \in H)) \to x \underset{˙}{+} y \in H$
	mplind.t	$⊢ (φ \land (x \in H \land y \in H)) \to x \underset{˙}{\cdot} y \in H$
	mplind.s	$⊢ (φ \land x \in K) \to C (x) \in H$
	mplind.v	$⊢ (φ \land x \in I) \to V (x) \in H$
	mplind.x	$⊢ φ \to X \in B$
	mplind.i	$⊢ φ \to I \in W$
	mplind.r	$⊢ φ \to R \in CRing$
Assertion	mplind	$⊢ φ \to X \in H$

Proof

Step	Hyp	Ref	Expression
1		mplind.sk	$⊢ K = {Base}_{R}$
2		mplind.sv	$⊢ V = I mVar R$
3		mplind.sy	$⊢ Y = I mPoly R$
4		mplind.sp	$⊢ \underset{˙}{+} = +_{Y}$
5		mplind.st	$⊢ \underset{˙}{\cdot} = \cdot_{Y}$
6		mplind.sc	$⊢ C = algSc (Y)$
7		mplind.sb	$⊢ B = {Base}_{Y}$
8		mplind.p	$⊢ (φ \land (x \in H \land y \in H)) \to x \underset{˙}{+} y \in H$
9		mplind.t	$⊢ (φ \land (x \in H \land y \in H)) \to x \underset{˙}{\cdot} y \in H$
10		mplind.s	$⊢ (φ \land x \in K) \to C (x) \in H$
11		mplind.v	$⊢ (φ \land x \in I) \to V (x) \in H$
12		mplind.x	$⊢ φ \to X \in B$
13		mplind.i	$⊢ φ \to I \in W$
14		mplind.r	$⊢ φ \to R \in CRing$
15		eqid	$⊢ I mPwSer R = I mPwSer R$
16	15 13 14	psrassa	$⊢ φ \to I mPwSer R \in AssAlg$
17		inss2	$⊢ H \cap B \subseteq B$
18		crngring	$⊢ R \in CRing \to R \in Ring$
19	14 18	syl	$⊢ φ \to R \in Ring$
20	15 3 7 13 19	mplsubrg	$⊢ φ \to B \in SubRing (I mPwSer R)$
21		eqid	$⊢ {Base}_{(I mPwSer R)} = {Base}_{(I mPwSer R)}$
22	21	subrgss	$⊢ B \in SubRing (I mPwSer R) \to B \subseteq {Base}_{(I mPwSer R)}$
23	20 22	syl	$⊢ φ \to B \subseteq {Base}_{(I mPwSer R)}$
24	17 23	sstrid	$⊢ φ \to H \cap B \subseteq {Base}_{(I mPwSer R)}$
25	3 2 7 13 19	mvrf2	$⊢ φ \to V : I ⟶ B$
26	25	ffnd	$⊢ φ \to V Fn I$
27	11	ralrimiva	$⊢ φ \to \forall x \in I V (x) \in H$
28		fnfvrnss	$⊢ (V Fn I \land \forall x \in I V (x) \in H) \to ran V \subseteq H$
29	26 27 28	syl2anc	$⊢ φ \to ran V \subseteq H$
30	25	frnd	$⊢ φ \to ran V \subseteq B$
31	29 30	ssind	$⊢ φ \to ran V \subseteq H \cap B$
32		eqid	$⊢ AlgSpan (I mPwSer R) = AlgSpan (I mPwSer R)$
33	32 21	aspss	$⊢ (I mPwSer R \in AssAlg \land H \cap B \subseteq {Base}_{(I mPwSer R)} \land ran V \subseteq H \cap B) \to AlgSpan (I mPwSer R) (ran V) \subseteq AlgSpan (I mPwSer R) (H \cap B)$
34	16 24 31 33	syl3anc	$⊢ φ \to AlgSpan (I mPwSer R) (ran V) \subseteq AlgSpan (I mPwSer R) (H \cap B)$
35	3 15 2 32 13 14	mplbas2	$⊢ φ \to AlgSpan (I mPwSer R) (ran V) = {Base}_{Y}$
36	35 7	eqtr4di	$⊢ φ \to AlgSpan (I mPwSer R) (ran V) = B$
37	17	a1i	$⊢ φ \to H \cap B \subseteq B$
38	3	mplassa	$⊢ (I \in W \land R \in CRing) \to Y \in AssAlg$
39	13 14 38	syl2anc	$⊢ φ \to Y \in AssAlg$
40		eqid	$⊢ Scalar (Y) = Scalar (Y)$
41	6 40	asclrhm	$⊢ Y \in AssAlg \to C \in (Scalar (Y) RingHom Y)$
42	39 41	syl	$⊢ φ \to C \in (Scalar (Y) RingHom Y)$
43		eqid	$⊢ 1_{Scalar (Y)} = 1_{Scalar (Y)}$
44		eqid	$⊢ 1_{Y} = 1_{Y}$
45	43 44	rhm1	$⊢ C \in (Scalar (Y) RingHom Y) \to C (1_{Scalar (Y)}) = 1_{Y}$
46	42 45	syl	$⊢ φ \to C (1_{Scalar (Y)}) = 1_{Y}$
47		fveq2	$⊢ x = 1_{Scalar (Y)} \to C (x) = C (1_{Scalar (Y)})$
48	47	eleq1d	$⊢ x = 1_{Scalar (Y)} \to (C (x) \in H \leftrightarrow C (1_{Scalar (Y)}) \in H)$
49	10	ralrimiva	$⊢ φ \to \forall x \in K C (x) \in H$
50	3 13 14	mplsca	$⊢ φ \to R = Scalar (Y)$
51	50 19	eqeltrrd	$⊢ φ \to Scalar (Y) \in Ring$
52		eqid	$⊢ {Base}_{Scalar (Y)} = {Base}_{Scalar (Y)}$
53	52 43	ringidcl	$⊢ Scalar (Y) \in Ring \to 1_{Scalar (Y)} \in {Base}_{Scalar (Y)}$
54	51 53	syl	$⊢ φ \to 1_{Scalar (Y)} \in {Base}_{Scalar (Y)}$
55	50	fveq2d	$⊢ φ \to {Base}_{R} = {Base}_{Scalar (Y)}$
56	1 55	eqtrid	$⊢ φ \to K = {Base}_{Scalar (Y)}$
57	54 56	eleqtrrd	$⊢ φ \to 1_{Scalar (Y)} \in K$
58	48 49 57	rspcdva	$⊢ φ \to C (1_{Scalar (Y)}) \in H$
59	46 58	eqeltrrd	$⊢ φ \to 1_{Y} \in H$
60		assaring	$⊢ Y \in AssAlg \to Y \in Ring$
61	39 60	syl	$⊢ φ \to Y \in Ring$
62	7 44	ringidcl	$⊢ Y \in Ring \to 1_{Y} \in B$
63	61 62	syl	$⊢ φ \to 1_{Y} \in B$
64	59 63	elind	$⊢ φ \to 1_{Y} \in (H \cap B)$
65	64	ne0d	$⊢ φ \to H \cap B \neq \emptyset$
66		elinel1	$⊢ z \in (H \cap B) \to z \in H$
67		elinel1	$⊢ w \in (H \cap B) \to w \in H$
68	66 67	anim12i	$⊢ (z \in (H \cap B) \land w \in (H \cap B)) \to (z \in H \land w \in H)$
69	8	caovclg	$⊢ (φ \land (z \in H \land w \in H)) \to z \underset{˙}{+} w \in H$
70	68 69	sylan2	$⊢ (φ \land (z \in (H \cap B) \land w \in (H \cap B))) \to z \underset{˙}{+} w \in H$
71		assalmod	$⊢ Y \in AssAlg \to Y \in LMod$
72	39 71	syl	$⊢ φ \to Y \in LMod$
73		lmodgrp	$⊢ Y \in LMod \to Y \in Grp$
74	72 73	syl	$⊢ φ \to Y \in Grp$
75	74	adantr	$⊢ (φ \land (z \in (H \cap B) \land w \in (H \cap B))) \to Y \in Grp$
76		simprl	$⊢ (φ \land (z \in (H \cap B) \land w \in (H \cap B))) \to z \in (H \cap B)$
77	76	elin2d	$⊢ (φ \land (z \in (H \cap B) \land w \in (H \cap B))) \to z \in B$
78		simprr	$⊢ (φ \land (z \in (H \cap B) \land w \in (H \cap B))) \to w \in (H \cap B)$
79	78	elin2d	$⊢ (φ \land (z \in (H \cap B) \land w \in (H \cap B))) \to w \in B$
80	7 4	grpcl	$⊢ (Y \in Grp \land z \in B \land w \in B) \to z \underset{˙}{+} w \in B$
81	75 77 79 80	syl3anc	$⊢ (φ \land (z \in (H \cap B) \land w \in (H \cap B))) \to z \underset{˙}{+} w \in B$
82	70 81	elind	$⊢ (φ \land (z \in (H \cap B) \land w \in (H \cap B))) \to z \underset{˙}{+} w \in (H \cap B)$
83	82	anassrs	$⊢ ((φ \land z \in (H \cap B)) \land w \in (H \cap B)) \to z \underset{˙}{+} w \in (H \cap B)$
84	83	ralrimiva	$⊢ (φ \land z \in (H \cap B)) \to \forall w \in (H \cap B) z \underset{˙}{+} w \in (H \cap B)$
85		eqid	$⊢ {inv}_{g} (Y) = {inv}_{g} (Y)$
86	61	adantr	$⊢ (φ \land z \in (H \cap B)) \to Y \in Ring$
87		simpr	$⊢ (φ \land z \in (H \cap B)) \to z \in (H \cap B)$
88	87	elin2d	$⊢ (φ \land z \in (H \cap B)) \to z \in B$
89	7 5 44 85 86 88	ringnegl	$⊢ (φ \land z \in (H \cap B)) \to {inv}_{g} (Y) (1_{Y}) \underset{˙}{\cdot} z = {inv}_{g} (Y) (z)$
90		simpl	$⊢ (φ \land z \in (H \cap B)) \to φ$
91		rhmghm	$⊢ C \in (Scalar (Y) RingHom Y) \to C \in (Scalar (Y) GrpHom Y)$
92	42 91	syl	$⊢ φ \to C \in (Scalar (Y) GrpHom Y)$
93		eqid	$⊢ {inv}_{g} (Scalar (Y)) = {inv}_{g} (Scalar (Y))$
94	52 93 85	ghminv	$⊢ (C \in (Scalar (Y) GrpHom Y) \land 1_{Scalar (Y)} \in {Base}_{Scalar (Y)}) \to C ({inv}_{g} (Scalar (Y)) (1_{Scalar (Y)})) = {inv}_{g} (Y) (C (1_{Scalar (Y)}))$
95	92 54 94	syl2anc	$⊢ φ \to C ({inv}_{g} (Scalar (Y)) (1_{Scalar (Y)})) = {inv}_{g} (Y) (C (1_{Scalar (Y)}))$
96	46	fveq2d	$⊢ φ \to {inv}_{g} (Y) (C (1_{Scalar (Y)})) = {inv}_{g} (Y) (1_{Y})$
97	95 96	eqtrd	$⊢ φ \to C ({inv}_{g} (Scalar (Y)) (1_{Scalar (Y)})) = {inv}_{g} (Y) (1_{Y})$
98		fveq2	$⊢ x = {inv}_{g} (Scalar (Y)) (1_{Scalar (Y)}) \to C (x) = C ({inv}_{g} (Scalar (Y)) (1_{Scalar (Y)}))$
99	98	eleq1d	$⊢ x = {inv}_{g} (Scalar (Y)) (1_{Scalar (Y)}) \to (C (x) \in H \leftrightarrow C ({inv}_{g} (Scalar (Y)) (1_{Scalar (Y)})) \in H)$
100		ringgrp	$⊢ Scalar (Y) \in Ring \to Scalar (Y) \in Grp$
101	51 100	syl	$⊢ φ \to Scalar (Y) \in Grp$
102	52 93	grpinvcl	$⊢ (Scalar (Y) \in Grp \land 1_{Scalar (Y)} \in {Base}_{Scalar (Y)}) \to {inv}_{g} (Scalar (Y)) (1_{Scalar (Y)}) \in {Base}_{Scalar (Y)}$
103	101 54 102	syl2anc	$⊢ φ \to {inv}_{g} (Scalar (Y)) (1_{Scalar (Y)}) \in {Base}_{Scalar (Y)}$
104	103 56	eleqtrrd	$⊢ φ \to {inv}_{g} (Scalar (Y)) (1_{Scalar (Y)}) \in K$
105	99 49 104	rspcdva	$⊢ φ \to C ({inv}_{g} (Scalar (Y)) (1_{Scalar (Y)})) \in H$
106	97 105	eqeltrrd	$⊢ φ \to {inv}_{g} (Y) (1_{Y}) \in H$
107	106	adantr	$⊢ (φ \land z \in (H \cap B)) \to {inv}_{g} (Y) (1_{Y}) \in H$
108	87	elin1d	$⊢ (φ \land z \in (H \cap B)) \to z \in H$
109	9	caovclg	$⊢ (φ \land ({inv}_{g} (Y) (1_{Y}) \in H \land z \in H)) \to {inv}_{g} (Y) (1_{Y}) \underset{˙}{\cdot} z \in H$
110	90 107 108 109	syl12anc	$⊢ (φ \land z \in (H \cap B)) \to {inv}_{g} (Y) (1_{Y}) \underset{˙}{\cdot} z \in H$
111	89 110	eqeltrrd	$⊢ (φ \land z \in (H \cap B)) \to {inv}_{g} (Y) (z) \in H$
112	74	adantr	$⊢ (φ \land z \in (H \cap B)) \to Y \in Grp$
113	7 85	grpinvcl	$⊢ (Y \in Grp \land z \in B) \to {inv}_{g} (Y) (z) \in B$
114	112 88 113	syl2anc	$⊢ (φ \land z \in (H \cap B)) \to {inv}_{g} (Y) (z) \in B$
115	111 114	elind	$⊢ (φ \land z \in (H \cap B)) \to {inv}_{g} (Y) (z) \in (H \cap B)$
116	84 115	jca	$⊢ (φ \land z \in (H \cap B)) \to (\forall w \in (H \cap B) z \underset{˙}{+} w \in (H \cap B) \land {inv}_{g} (Y) (z) \in (H \cap B))$
117	116	ralrimiva	$⊢ φ \to \forall z \in (H \cap B) (\forall w \in (H \cap B) z \underset{˙}{+} w \in (H \cap B) \land {inv}_{g} (Y) (z) \in (H \cap B))$
118	7 4 85	issubg2	$⊢ Y \in Grp \to (H \cap B \in SubGrp (Y) \leftrightarrow (H \cap B \subseteq B \land H \cap B \neq \emptyset \land \forall z \in (H \cap B) (\forall w \in (H \cap B) z \underset{˙}{+} w \in (H \cap B) \land {inv}_{g} (Y) (z) \in (H \cap B))))$
119	74 118	syl	$⊢ φ \to (H \cap B \in SubGrp (Y) \leftrightarrow (H \cap B \subseteq B \land H \cap B \neq \emptyset \land \forall z \in (H \cap B) (\forall w \in (H \cap B) z \underset{˙}{+} w \in (H \cap B) \land {inv}_{g} (Y) (z) \in (H \cap B))))$
120	37 65 117 119	mpbir3and	$⊢ φ \to H \cap B \in SubGrp (Y)$
121		elinel1	$⊢ x \in (H \cap B) \to x \in H$
122		elinel1	$⊢ y \in (H \cap B) \to y \in H$
123	121 122	anim12i	$⊢ (x \in (H \cap B) \land y \in (H \cap B)) \to (x \in H \land y \in H)$
124	123 9	sylan2	$⊢ (φ \land (x \in (H \cap B) \land y \in (H \cap B))) \to x \underset{˙}{\cdot} y \in H$
125	61	adantr	$⊢ (φ \land (x \in (H \cap B) \land y \in (H \cap B))) \to Y \in Ring$
126		simprl	$⊢ (φ \land (x \in (H \cap B) \land y \in (H \cap B))) \to x \in (H \cap B)$
127	126	elin2d	$⊢ (φ \land (x \in (H \cap B) \land y \in (H \cap B))) \to x \in B$
128		simprr	$⊢ (φ \land (x \in (H \cap B) \land y \in (H \cap B))) \to y \in (H \cap B)$
129	128	elin2d	$⊢ (φ \land (x \in (H \cap B) \land y \in (H \cap B))) \to y \in B$
130	7 5	ringcl	$⊢ (Y \in Ring \land x \in B \land y \in B) \to x \underset{˙}{\cdot} y \in B$
131	125 127 129 130	syl3anc	$⊢ (φ \land (x \in (H \cap B) \land y \in (H \cap B))) \to x \underset{˙}{\cdot} y \in B$
132	124 131	elind	$⊢ (φ \land (x \in (H \cap B) \land y \in (H \cap B))) \to x \underset{˙}{\cdot} y \in (H \cap B)$
133	132	ralrimivva	$⊢ φ \to \forall x \in (H \cap B) \forall y \in (H \cap B) x \underset{˙}{\cdot} y \in (H \cap B)$
134	7 44 5	issubrg2	$⊢ Y \in Ring \to (H \cap B \in SubRing (Y) \leftrightarrow (H \cap B \in SubGrp (Y) \land 1_{Y} \in (H \cap B) \land \forall x \in (H \cap B) \forall y \in (H \cap B) x \underset{˙}{\cdot} y \in (H \cap B)))$
135	61 134	syl	$⊢ φ \to (H \cap B \in SubRing (Y) \leftrightarrow (H \cap B \in SubGrp (Y) \land 1_{Y} \in (H \cap B) \land \forall x \in (H \cap B) \forall y \in (H \cap B) x \underset{˙}{\cdot} y \in (H \cap B)))$
136	120 64 133 135	mpbir3and	$⊢ φ \to H \cap B \in SubRing (Y)$
137	3 15 7	mplval2	$⊢ Y = (I mPwSer R) ↾_{𝑠} B$
138	137	subsubrg	$⊢ B \in SubRing (I mPwSer R) \to (H \cap B \in SubRing (Y) \leftrightarrow (H \cap B \in SubRing (I mPwSer R) \land H \cap B \subseteq B))$
139	138	simprbda	$⊢ (B \in SubRing (I mPwSer R) \land H \cap B \in SubRing (Y)) \to H \cap B \in SubRing (I mPwSer R)$
140	20 136 139	syl2anc	$⊢ φ \to H \cap B \in SubRing (I mPwSer R)$
141		assalmod	$⊢ I mPwSer R \in AssAlg \to I mPwSer R \in LMod$
142	16 141	syl	$⊢ φ \to I mPwSer R \in LMod$
143	15 3 7 13 19	mpllss	$⊢ φ \to B \in LSubSp (I mPwSer R)$
144	39	adantr	$⊢ (φ \land (z \in {Base}_{Scalar (Y)} \land w \in (H \cap B))) \to Y \in AssAlg$
145		simprl	$⊢ (φ \land (z \in {Base}_{Scalar (Y)} \land w \in (H \cap B))) \to z \in {Base}_{Scalar (Y)}$
146		simprr	$⊢ (φ \land (z \in {Base}_{Scalar (Y)} \land w \in (H \cap B))) \to w \in (H \cap B)$
147	146	elin2d	$⊢ (φ \land (z \in {Base}_{Scalar (Y)} \land w \in (H \cap B))) \to w \in B$
148		eqid	$⊢ \cdot_{Y} = \cdot_{Y}$
149	6 40 52 7 5 148	asclmul1	$⊢ (Y \in AssAlg \land z \in {Base}_{Scalar (Y)} \land w \in B) \to C (z) \underset{˙}{\cdot} w = z \cdot_{Y} w$
150	144 145 147 149	syl3anc	$⊢ (φ \land (z \in {Base}_{Scalar (Y)} \land w \in (H \cap B))) \to C (z) \underset{˙}{\cdot} w = z \cdot_{Y} w$
151		fveq2	$⊢ x = z \to C (x) = C (z)$
152	151	eleq1d	$⊢ x = z \to (C (x) \in H \leftrightarrow C (z) \in H)$
153	49	adantr	$⊢ (φ \land (z \in {Base}_{Scalar (Y)} \land w \in (H \cap B))) \to \forall x \in K C (x) \in H$
154	56	adantr	$⊢ (φ \land (z \in {Base}_{Scalar (Y)} \land w \in (H \cap B))) \to K = {Base}_{Scalar (Y)}$
155	145 154	eleqtrrd	$⊢ (φ \land (z \in {Base}_{Scalar (Y)} \land w \in (H \cap B))) \to z \in K$
156	152 153 155	rspcdva	$⊢ (φ \land (z \in {Base}_{Scalar (Y)} \land w \in (H \cap B))) \to C (z) \in H$
157	146	elin1d	$⊢ (φ \land (z \in {Base}_{Scalar (Y)} \land w \in (H \cap B))) \to w \in H$
158	156 157	jca	$⊢ (φ \land (z \in {Base}_{Scalar (Y)} \land w \in (H \cap B))) \to (C (z) \in H \land w \in H)$
159	9	caovclg	$⊢ (φ \land (C (z) \in H \land w \in H)) \to C (z) \underset{˙}{\cdot} w \in H$
160	158 159	syldan	$⊢ (φ \land (z \in {Base}_{Scalar (Y)} \land w \in (H \cap B))) \to C (z) \underset{˙}{\cdot} w \in H$
161	150 160	eqeltrrd	$⊢ (φ \land (z \in {Base}_{Scalar (Y)} \land w \in (H \cap B))) \to z \cdot_{Y} w \in H$
162	72	adantr	$⊢ (φ \land (z \in {Base}_{Scalar (Y)} \land w \in (H \cap B))) \to Y \in LMod$
163	7 40 148 52	lmodvscl	$⊢ (Y \in LMod \land z \in {Base}_{Scalar (Y)} \land w \in B) \to z \cdot_{Y} w \in B$
164	162 145 147 163	syl3anc	$⊢ (φ \land (z \in {Base}_{Scalar (Y)} \land w \in (H \cap B))) \to z \cdot_{Y} w \in B$
165	161 164	elind	$⊢ (φ \land (z \in {Base}_{Scalar (Y)} \land w \in (H \cap B))) \to z \cdot_{Y} w \in (H \cap B)$
166	165	ralrimivva	$⊢ φ \to \forall z \in {Base}_{Scalar (Y)} \forall w \in (H \cap B) z \cdot_{Y} w \in (H \cap B)$
167		eqid	$⊢ LSubSp (Y) = LSubSp (Y)$
168	40 52 7 148 167	islss4	$⊢ Y \in LMod \to (H \cap B \in LSubSp (Y) \leftrightarrow (H \cap B \in SubGrp (Y) \land \forall z \in {Base}_{Scalar (Y)} \forall w \in (H \cap B) z \cdot_{Y} w \in (H \cap B)))$
169	72 168	syl	$⊢ φ \to (H \cap B \in LSubSp (Y) \leftrightarrow (H \cap B \in SubGrp (Y) \land \forall z \in {Base}_{Scalar (Y)} \forall w \in (H \cap B) z \cdot_{Y} w \in (H \cap B)))$
170	120 166 169	mpbir2and	$⊢ φ \to H \cap B \in LSubSp (Y)$
171		eqid	$⊢ LSubSp (I mPwSer R) = LSubSp (I mPwSer R)$
172	137 171 167	lsslss	$⊢ (I mPwSer R \in LMod \land B \in LSubSp (I mPwSer R)) \to (H \cap B \in LSubSp (Y) \leftrightarrow (H \cap B \in LSubSp (I mPwSer R) \land H \cap B \subseteq B))$
173	172	simprbda	$⊢ ((I mPwSer R \in LMod \land B \in LSubSp (I mPwSer R)) \land H \cap B \in LSubSp (Y)) \to H \cap B \in LSubSp (I mPwSer R)$
174	142 143 170 173	syl21anc	$⊢ φ \to H \cap B \in LSubSp (I mPwSer R)$
175	32 21 171	aspid	$⊢ (I mPwSer R \in AssAlg \land H \cap B \in SubRing (I mPwSer R) \land H \cap B \in LSubSp (I mPwSer R)) \to AlgSpan (I mPwSer R) (H \cap B) = H \cap B$
176	16 140 174 175	syl3anc	$⊢ φ \to AlgSpan (I mPwSer R) (H \cap B) = H \cap B$
177	34 36 176	3sstr3d	$⊢ φ \to B \subseteq H \cap B$
178	177 12	sseldd	$⊢ φ \to X \in (H \cap B)$
179	178	elin1d	$⊢ φ \to X \in H$

Metamath Proof Explorer

Theorem mplind

Proof